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 ⊢ F = Scalar ⁡ W
cmodscexp.k ⊢ K = Base F
cmodscmulexp.x ⊢ X = Base W
cmodscmulexp.s ⊢ · ˙ = ⋅ W
Assertion cmodscmulexp ⊢ W ∈ CMod ∧ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → i N · ˙ B ∈ X

Proof

Step Hyp Ref Expression
1 cmodscexp.f ⊢ F = Scalar ⁡ W
2 cmodscexp.k ⊢ K = Base F
3 cmodscmulexp.x ⊢ X = Base W
4 cmodscmulexp.s ⊢ · ˙ = ⋅ W
5 clmlmod ⊢ W ∈ CMod → W ∈ LMod
6 5 adantr ⊢ W ∈ CMod ∧ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → W ∈ LMod
7 simp1 ⊢ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → i ∈ K
8 7 anim2i ⊢ W ∈ CMod ∧ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → W ∈ CMod ∧ i ∈ K
9 simpr3 ⊢ W ∈ CMod ∧ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → N ∈ ℕ
10 1 2 cmodscexp ⊢ W ∈ CMod ∧ i ∈ K ∧ N ∈ ℕ → i N ∈ K
11 8 9 10 syl2anc ⊢ W ∈ CMod ∧ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → i N ∈ K
12 simpr2 ⊢ W ∈ CMod ∧ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → B ∈ X
13 3 1 4 2 lmodvscl ⊢ W ∈ LMod ∧ i N ∈ K ∧ B ∈ X → i N · ˙ B ∈ X
14 6 11 12 13 syl3anc ⊢ W ∈ CMod ∧ i ∈ K ∧ B ∈ X ∧ N ∈ ℕ → i N · ˙ B ∈ X