Theorem joinlmuladdmuli

Description: Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019)

	Ref	Expression
Hypotheses	joinlmuladdmuli.1	⊢ 𝐴 ∈ ℂ
	joinlmuladdmuli.2	⊢ 𝐵 ∈ ℂ
	joinlmuladdmuli.3	⊢ 𝐶 ∈ ℂ
	joinlmuladdmuli.4	⊢ ( ( 𝐴 · 𝐵 ) + ( 𝐶 · 𝐵 ) ) = 𝐷
Assertion	joinlmuladdmuli	⊢ ( ( 𝐴 + 𝐶 ) · 𝐵 ) = 𝐷

Proof

Step	Hyp	Ref	Expression
1		joinlmuladdmuli.1	⊢ 𝐴 ∈ ℂ
2		joinlmuladdmuli.2	⊢ 𝐵 ∈ ℂ
3		joinlmuladdmuli.3	⊢ 𝐶 ∈ ℂ
4		joinlmuladdmuli.4	⊢ ( ( 𝐴 · 𝐵 ) + ( 𝐶 · 𝐵 ) ) = 𝐷
5	1	a1i	⊢ ( ⊤ → 𝐴 ∈ ℂ )
6	2	a1i	⊢ ( ⊤ → 𝐵 ∈ ℂ )
7	3	a1i	⊢ ( ⊤ → 𝐶 ∈ ℂ )
8	4	a1i	⊢ ( ⊤ → ( ( 𝐴 · 𝐵 ) + ( 𝐶 · 𝐵 ) ) = 𝐷 )
9	5 6 7 8	joinlmuladdmuld	⊢ ( ⊤ → ( ( 𝐴 + 𝐶 ) · 𝐵 ) = 𝐷 )
10	9	mptru	⊢ ( ( 𝐴 + 𝐶 ) · 𝐵 ) = 𝐷