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	|- .x. = ( .s ` M )
	lincscmcl.r	|- R = ( Base ` ( Scalar ` M ) )
	lincsumscmcl.b	|- .+ = ( +g ` M )
Assertion	lincsumscmcl	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. R /\ D e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) ) -> ( ( C .x. D ) .+ B ) e. ( M LinCo V ) )

Proof

Step	Hyp	Ref	Expression
1		lincscmcl.s	|- .x. = ( .s ` M )
2		lincscmcl.r	|- R = ( Base ` ( Scalar ` M ) )
3		lincsumscmcl.b	|- .+ = ( +g ` M )
4	1 2	lincscmcl	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R /\ D e. ( M LinCo V ) ) -> ( C .x. D ) e. ( M LinCo V ) )
5	4	3adant3r3	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. R /\ D e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) ) -> ( C .x. D ) e. ( M LinCo V ) )
6		simpr3	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. R /\ D e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) ) -> B e. ( M LinCo V ) )
7	5 6	jca	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. R /\ D e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) ) -> ( ( C .x. D ) e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) )
8	3	lincsumcl	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C .x. D ) e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) ) -> ( ( C .x. D ) .+ B ) e. ( M LinCo V ) )
9	7 8	syldan	|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. R /\ D e. ( M LinCo V ) /\ B e. ( M LinCo V ) ) ) -> ( ( C .x. D ) .+ B ) e. ( M LinCo V ) )