English
The extension respects multiplication: (I * J).extended = I.extended * J.extended.
Русский
Расширение сохраняет умножение: (I*J).extended = I.extended * J.extended.
LaTeX
$$$ (I \cdot J).extended L hf = (I.extended L hf) \cdot (J.extended L hf) $$$
Lean4
theorem extended_mul : (I * J).extended L hf = (I.extended L hf) * (J.extended L hf) :=
by
apply coeToSubmodule_injective
simp only [coe_extended_eq_span, coe_mul, span_mul_span]
refine Submodule.span_eq_span (fun _ h ↦ ?_) (fun _ h ↦ ?_)
· rcases h with ⟨x, hx, rfl⟩
replace hx : x ∈ (I : Submodule A K) * (J : Submodule A K) := coe_mul I J ▸ hx
rw [Submodule.mul_eq_span_mul_set] at hx
refine span_induction (fun y hy ↦ ?_) (by simp) (fun y z _ _ hy hz ↦ ?_) (fun a y _ hy ↦ ?_) hx
· rcases Set.mem_mul.mp hy with ⟨i, hi, j, hj, rfl⟩
exact subset_span <| Set.mem_mul.mpr ⟨map_f i, ⟨i, hi, by simp⟩, map_f j, ⟨j, hj, by simp⟩, by simp⟩
· exact map_add map_f y z ▸ Submodule.add_mem _ hy hz
· rw [Algebra.smul_def, map_mul, map_eq, ← Algebra.smul_def]
exact smul_mem _ (f a) hy
· rcases Set.mem_mul.mp h with ⟨y, ⟨i, hi, rfl⟩, z, ⟨j, hj, rfl⟩, rfl⟩
exact Submodule.subset_span ⟨i * j, mul_mem_mul hi hj, by simp⟩
