English
If z lies in the span generated by elements hI.dpow n x with x ∈ S, then for any k ≠ 0, hI.dpow k z also lies in the same span.
Русский
Если z ∈ span{ y | ∃ n ≠ 0, ∃ x ∈ S, y = hI.dpow n x }, то для любого k ≠ 0, hI.dpow k z ∈ тот же span.
LaTeX
$$If z ∈ span {y : A | ∃ (n ≠ 0) (x ∈ S), y = hI.dpow n x}, then hI.dpow k z ∈ span {y : A | ∃ (n ≠ 0) (x ∈ S), y = hI.dpow n x}$$
Lean4
theorem dpow_mem_span_of_mem_span {S : Set A} (hS : S ⊆ I) {k : ℕ} (hk : k ≠ 0) {z : A}
(hz : z ∈ span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) :
hI.dpow k z ∈ span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} :=
by
let J := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
have hSI := hI.dpow_span_isSubideal hS
have haux : ∀ (n : ℕ) (_ : n ≠ 0), hI.dpow n z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} :=
by
refine Submodule.span_induction ?_ ?_ ?_ ?_ hz
· -- Elements of S
rintro y ⟨m, hm, x, hxS, hxy⟩ n hn
rw [hxy, hI.dpow_comp hm (hS hxS)]
exact mul_mem_left _ _ (subset_span ⟨n * m, mul_ne_zero hn hm, x, hxS, rfl⟩)
· -- Zero
exact fun _ hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem]
· intro x y hx hy hx_pow hy_pow n hn
rw [hI.dpow_add' (hSI hx) (hSI hy)]
apply Submodule.sum_mem (span _)
intro m _
by_cases hm0 : m = 0
· rw [hm0]; exact (span _).mul_mem_left _ (hy_pow n hn)
· exact (span _).mul_mem_right _ (hx_pow m hm0)
· intro a x hx hx_pow n hn
rw [smul_eq_mul, hI.dpow_mul (hSI hx)]
exact mul_mem_left (span _) (a ^ n) (hx_pow n hn)
exact haux _ hk
