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 \in CMod \land i \in K) \land N \in ℕ) \to i^{N} \in K$

Proof

Step	Hyp	Ref	Expression
1		cmodscexp.f	$⊢ F = Scalar (W)$
2		cmodscexp.k	$⊢ K = {Base}_{F}$
3		ax-icn	$⊢ i \in ℂ$
4	3	a1i	$⊢ (W \in CMod \land i \in K) \to i \in ℂ$
5		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
6		cnfldexp	$⊢ (i \in ℂ \land N \in ℕ_{0}) \to N \cdot_{{mulGrp}_{ℂ_{fld}}} i = i^{N}$
7	4 5 6	syl2an	$⊢ ((W \in CMod \land i \in K) \land N \in ℕ) \to N \cdot_{{mulGrp}_{ℂ_{fld}}} i = i^{N}$
8	1 2	clmsubrg	$⊢ W \in CMod \to K \in SubRing (ℂ_{fld})$
9		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
10	9	subrgsubm	$⊢ K \in SubRing (ℂ_{fld}) \to K \in SubMnd ({mulGrp}_{ℂ_{fld}})$
11	8 10	syl	$⊢ W \in CMod \to K \in SubMnd ({mulGrp}_{ℂ_{fld}})$
12	11	ad2antrr	$⊢ ((W \in CMod \land i \in K) \land N \in ℕ) \to K \in SubMnd ({mulGrp}_{ℂ_{fld}})$
13	5	adantl	$⊢ ((W \in CMod \land i \in K) \land N \in ℕ) \to N \in ℕ_{0}$
14		simplr	$⊢ ((W \in CMod \land i \in K) \land N \in ℕ) \to i \in K$
15		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
16	15	submmulgcl	$⊢ (K \in SubMnd ({mulGrp}_{ℂ_{fld}}) \land N \in ℕ_{0} \land i \in K) \to N \cdot_{{mulGrp}_{ℂ_{fld}}} i \in K$
17	12 13 14 16	syl3anc	$⊢ ((W \in CMod \land i \in K) \land N \in ℕ) \to N \cdot_{{mulGrp}_{ℂ_{fld}}} i \in K$
18	7 17	eqeltrrd	$⊢ ((W \in CMod \land i \in K) \land N \in ℕ) \to i^{N} \in K$