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	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
		lincscmcl.r	$⊢ R = {Base}_{Scalar (M)}$
		lincsumscmcl.b	$⊢ \underset{˙}{+} = +_{M}$
	Assertion	lincsumscmcl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \in R \land D \in (M LinCo V) \land B \in (M LinCo V))) \to (C \underset{˙}{\cdot} D) \underset{˙}{+} B \in (M LinCo V)$

Proof

Step	Hyp	Ref	Expression
1		lincscmcl.s	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
2		lincscmcl.r	$⊢ R = {Base}_{Scalar (M)}$
3		lincsumscmcl.b	$⊢ \underset{˙}{+} = +_{M}$
4	1 2	lincscmcl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R \land D \in (M LinCo V)) \to C \underset{˙}{\cdot} D \in (M LinCo V)$
5	4	3adant3r3	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \in R \land D \in (M LinCo V) \land B \in (M LinCo V))) \to C \underset{˙}{\cdot} D \in (M LinCo V)$
6		simpr3	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \in R \land D \in (M LinCo V) \land B \in (M LinCo V))) \to B \in (M LinCo V)$
7	5 6	jca	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \in R \land D \in (M LinCo V) \land B \in (M LinCo V))) \to (C \underset{˙}{\cdot} D \in (M LinCo V) \land B \in (M LinCo V))$
8	3	lincsumcl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \underset{˙}{\cdot} D \in (M LinCo V) \land B \in (M LinCo V))) \to (C \underset{˙}{\cdot} D) \underset{˙}{+} B \in (M LinCo V)$
9	7 8	syldan	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \in R \land D \in (M LinCo V) \land B \in (M LinCo V))) \to (C \underset{˙}{\cdot} D) \underset{˙}{+} B \in (M LinCo V)$