Metamath Proof Explorer


Theorem joinlmulsubmuli

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

Ref Expression
Hypotheses joinlmulsubmuli.1 𝐴 ∈ ℂ
joinlmulsubmuli.2 𝐵 ∈ ℂ
joinlmulsubmuli.3 𝐶 ∈ ℂ
joinlmulsubmuli.4 ( ( 𝐴 · 𝐵 ) − ( 𝐶 · 𝐵 ) ) = 𝐷
Assertion joinlmulsubmuli ( ( 𝐴𝐶 ) · 𝐵 ) = 𝐷

Proof

Step Hyp Ref Expression
1 joinlmulsubmuli.1 𝐴 ∈ ℂ
2 joinlmulsubmuli.2 𝐵 ∈ ℂ
3 joinlmulsubmuli.3 𝐶 ∈ ℂ
4 joinlmulsubmuli.4 ( ( 𝐴 · 𝐵 ) − ( 𝐶 · 𝐵 ) ) = 𝐷
5 1 3 2 subdiri ( ( 𝐴𝐶 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) − ( 𝐶 · 𝐵 ) )
6 5 4 eqtri ( ( 𝐴𝐶 ) · 𝐵 ) = 𝐷