English
Let x ∈ M, f ∈ Dual_R M, y ∈ M, g ∈ Dual_R M with f(x) = 2. Then the equality of endomorphisms holds: preReflection (preReflection x f y) (preReflection f (Dual.eval x) g) = (preReflection x f) ∘ (preReflection y g) ∘ (preReflection x f).
Русский
Пусть x ∈ M, f ∈ Dual_R M, y ∈ M, g ∈ Dual_R M и f(x) = 2. Тогда выполняется равенство тождественной фигуры: предотражение(предотражение x f y)(предотражение f (Dual.eval x) g) = (предотражение x f) ∘ (предотражение y g) ∘ (предотражение x f).
LaTeX
$$$\\text{Let }R,M\\text{ with }f\\in M^*,\\ x,y\\in M\\text{ and }g\\in M^*\\text{ with }f(x)=2.\\\\\n\\text{Then }\\mathrm{preReflection}(\\mathrm{preReflection}(x,f,y))\\big(\\mathrm{preReflection}(f,\\mathrm{Dual.eval}(x),g)\\big)=(\\mathrm{preReflection}(x,f))\\circ(\\mathrm{preReflection}(y,g))\\circ(\\mathrm{preReflection}(x,f)).$$$
Lean4
theorem preReflection_preReflection (g : Dual R M) (h : f x = 2) :
preReflection (preReflection x f y) (preReflection f (Dual.eval R M x) g) =
(preReflection x f) ∘ₗ (preReflection y g) ∘ₗ (preReflection x f) :=
by
ext m
simp only [h, preReflection_apply, mul_comm (g x) (f m), mul_two, mul_assoc, Dual.eval_apply, LinearMap.sub_apply,
LinearMap.coe_comp, LinearMap.smul_apply, smul_eq_mul, smul_sub, sub_smul, smul_smul, sub_mul, comp_apply, map_sub,
map_smul, add_smul]
abel
