Metamath Proof Explorer

Theorem lincsumscmcl

Description: The sum of a linear combination and a multiplication of a linear combination with a scalar is a linear combination. (Contributed by AV, 11-Apr-2019)

Ref Expression
Hypotheses lincscmcl.s ⊢ · ˙ = ⋅ M
lincscmcl.r ⊢ R = Base Scalar ⁡ M
lincsumscmcl.b ⊢ + ˙ = + M
Assertion lincsumscmcl ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ C ∈ R ∧ D ∈ M LinCo V ∧ B ∈ M LinCo V → C · ˙ D + ˙ B ∈ M LinCo V

Proof

Step Hyp Ref Expression
1 lincscmcl.s ⊢ · ˙ = ⋅ M
2 lincscmcl.r ⊢ R = Base Scalar ⁡ M
3 lincsumscmcl.b ⊢ + ˙ = + M
4 1 2 lincscmcl ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ C ∈ R ∧ D ∈ M LinCo V → C · ˙ D ∈ M LinCo V
5 4 3adant3r3 ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ C ∈ R ∧ D ∈ M LinCo V ∧ B ∈ M LinCo V → C · ˙ D ∈ M LinCo V
6 simpr3 ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ C ∈ R ∧ D ∈ M LinCo V ∧ B ∈ M LinCo V → B ∈ M LinCo V
7 5 6 jca ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ C ∈ R ∧ D ∈ M LinCo V ∧ B ∈ M LinCo V → C · ˙ D ∈ M LinCo V ∧ B ∈ M LinCo V
8 3 lincsumcl ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ C · ˙ D ∈ M LinCo V ∧ B ∈ M LinCo V → C · ˙ D + ˙ B ∈ M LinCo V
9 7 8 syldan ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ C ∈ R ∧ D ∈ M LinCo V ∧ B ∈ M LinCo V → C · ˙ D + ˙ B ∈ M LinCo V