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

Metamath Proof Explorer

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 ↑ 𝑁 ) · 𝐵 ) ∈ 𝑋 )