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 ↑ 𝑁 ) ∈ 𝐾 )