This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cmodscexp.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cmodscexp ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → ( i ↑ 𝑁 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 cmodscexp.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cmodscexp.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 ax-icn ⊢ i ∈ ℂ
4 3 a1i ⊢ ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) → i ∈ ℂ )
5 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
6 cnfldexp ⊢ ( ( i ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ ℂfld ) ) i ) = ( i ↑ 𝑁 ) )
7 4 5 6 syl2an ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ ℂfld ) ) i ) = ( i ↑ 𝑁 ) )
8 1 2 clmsubrg ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
9 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
10 9 subrgsubm ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
11 8 10 syl ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
12 11 ad2antrr ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
13 5 adantl ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
14 simplr ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → i ∈ 𝐾 )
15 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
16 15 submmulgcl ⊢ ( ( 𝐾 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ 𝑁 ∈ ℕ0 ∧ i ∈ 𝐾 ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ ℂfld ) ) i ) ∈ 𝐾 )
17 12 13 14 16 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ( .g ‘ ( mulGrp ‘ ℂfld ) ) i ) ∈ 𝐾 )
18 7 17 eqeltrrd ⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → ( i ↑ 𝑁 ) ∈ 𝐾 )