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	⊢ · = ( ·𝑠 ‘ 𝑀 )
	lincscmcl.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
	lincsumscmcl.b	⊢ + = ( +g ‘ 𝑀 )
Assertion	lincsumscmcl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( ( 𝐶 · 𝐷 ) + 𝐵 ) ∈ ( 𝑀 LinCo 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lincscmcl.s	⊢ · = ( ·𝑠 ‘ 𝑀 )
2		lincscmcl.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
3		lincsumscmcl.b	⊢ + = ( +g ‘ 𝑀 )
4	1 2	lincscmcl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) → ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )
5	4	3adant3r3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )
6		simpr3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) )
7	5 6	jca	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) ) )
8	3	lincsumcl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( ( 𝐶 · 𝐷 ) + 𝐵 ) ∈ ( 𝑀 LinCo 𝑉 ) )
9	7 8	syldan	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐵 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( ( 𝐶 · 𝐷 ) + 𝐵 ) ∈ ( 𝑀 LinCo 𝑉 ) )