Metamath Proof Explorer

Theorem cmodscexp

Description: The powers of _i belong to the scalar subring of a subcomplex module if _i belongs to the scalar subring . (Contributed by AV, 18-Oct-2021)

Ref Expression
Hypotheses cmodscexp.f ⊢ F = Scalar ⁡ W
cmodscexp.k ⊢ K = Base F
Assertion cmodscexp ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → i N ∈ K

Proof

Step Hyp Ref Expression
1 cmodscexp.f ⊢ F = Scalar ⁡ W
2 cmodscexp.k ⊢ K = Base F
3 ax-icn ⊢ i ∈ ℂ
4 3 a1i ⊢ W ∈ CMod ∧ i ∈ K → i ∈ ℂ
5 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
6 cnfldexp ⊢ i ∈ ℂ ∧ N ∈ ℕ 0 → N ⋅ mulGrp ℂ fld i = i N
7 4 5 6 syl2an ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → N ⋅ mulGrp ℂ fld i = i N
8 1 2 clmsubrg ⊢ W ∈ CMod → K ∈ SubRing ⁡ ℂ fld
9 eqid ⊢ mulGrp ℂ fld = mulGrp ℂ fld
10 9 subrgsubm ⊢ K ∈ SubRing ⁡ ℂ fld → K ∈ SubMnd ⁡ mulGrp ℂ fld
11 8 10 syl ⊢ W ∈ CMod → K ∈ SubMnd ⁡ mulGrp ℂ fld
12 11 ad2antrr ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → K ∈ SubMnd ⁡ mulGrp ℂ fld
13 5 adantl ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → N ∈ ℕ 0
14 simplr ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → i ∈ K
15 eqid ⊢ ⋅ mulGrp ℂ fld = ⋅ mulGrp ℂ fld
16 15 submmulgcl ⊢ K ∈ SubMnd ⁡ mulGrp ℂ fld ∧ N ∈ ℕ 0 ∧ i ∈ K → N ⋅ mulGrp ℂ fld i ∈ K
17 12 13 14 16 syl3anc ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → N ⋅ mulGrp ℂ fld i ∈ K
18 7 17 eqeltrrd ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → i N ∈ K