dist_inversion_mul_dist_center_eq

English

For x ≠ c and y ≠ c, the product dist(inversion(c,R,x), y) · dist(x,c) equals dist(x, inversion(c,R,y)) · dist(y,c).

Русский

При x ≠ c и y ≠ c произведение dist(inversion(c,R,x), y) на dist(x,c) равно произведению dist(x, inversion(c,R,y)) на dist(y,c).

LaTeX

$$$x \ne c \land y \ne c \Rightarrow dist(inversion(c,R,x),y) \cdot dist(x,c) = dist(x, inversion(c,R,y)) \cdot dist(y,c)$$$

Lean4

theorem dist_inversion_mul_dist_center_eq (hx : x ≠ c) (hy : y ≠ c) :
    dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c :=
  by
  rcases eq_or_ne R 0 with rfl | hR; · simp [dist_comm, mul_comm]
  have hy' : inversion c R y ≠ c := by simp [*]
  conv in dist _ y => rw [← inversion_inversion c hR y]
  rw [dist_inversion_inversion hx hy', dist_inversion_center]
  have : dist x c ≠ 0 := dist_ne_zero.2 hx
  field_simp

Похожие утверждения