Theorem cmodscmulexp

Description: The scalar product of a vector with powers of _i belongs to the base set of a subcomplex module if the scalar subring of th subcomplex module contains _i . (Contributed by AV, 18-Oct-2021)

	Ref	Expression
Hypotheses	cmodscexp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cmodscexp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	cmodscmulexp.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
	cmodscmulexp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion	cmodscmulexp	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) ) → ( ( i ↑ 𝑁 ) · 𝐵 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		cmodscexp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		cmodscexp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		cmodscmulexp.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
4		cmodscmulexp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		clmlmod	⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
6	5	adantr	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) ) → 𝑊 ∈ LMod )
7		simp1	⊢ ( ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) → i ∈ 𝐾 )
8	7	anim2i	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) ) → ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) )
9		simpr3	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℕ )
10	1 2	cmodscexp	⊢ ( ( ( 𝑊 ∈ ℂMod ∧ i ∈ 𝐾 ) ∧ 𝑁 ∈ ℕ ) → ( i ↑ 𝑁 ) ∈ 𝐾 )
11	8 9 10	syl2anc	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) ) → ( i ↑ 𝑁 ) ∈ 𝐾 )
12		simpr2	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) ) → 𝐵 ∈ 𝑋 )
13	3 1 4 2	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ ( i ↑ 𝑁 ) ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ) → ( ( i ↑ 𝑁 ) · 𝐵 ) ∈ 𝑋 )
14	6 11 12 13	syl3anc	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( i ∈ 𝐾 ∧ 𝐵 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ) ) → ( ( i ↑ 𝑁 ) · 𝐵 ) ∈ 𝑋 )