Theorem affineequiv2

Description: Equivalence between two ways of expressing B as an affine combination of A and C . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	affineequiv.a	$$⊢\phi \to A\in ℂ$$
	affineequiv.b	$$⊢\phi \to B\in ℂ$$
	affineequiv.c	$$⊢\phi \to C\in ℂ$$
	affineequiv.d	$$⊢\phi \to D\in ℂ$$
Assertion	affineequiv2	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow B-A=\left(1-D\right)\left(C-A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		affineequiv.a	$$⊢\phi \to A\in ℂ$$
2		affineequiv.b	$$⊢\phi \to B\in ℂ$$
3		affineequiv.c	$$⊢\phi \to C\in ℂ$$
4		affineequiv.d	$$⊢\phi \to D\in ℂ$$
5	1 2 3 4	affineequiv	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow C-B=D\left(C-A\right)\right)$$
6	3 1	subcld	$$⊢\phi \to C-A\in ℂ$$
7	3 2	subcld	$$⊢\phi \to C-B\in ℂ$$
8	4 6	mulcld	$$⊢\phi \to D\left(C-A\right)\in ℂ$$
9	6 7 8	subcanad	$$⊢\phi \to \left(C-A-\left(C-B\right)=C-A-D\left(C-A\right)\leftrightarrow C-B=D\left(C-A\right)\right)$$
10	3 1 2	nnncan1d	$$⊢\phi \to C-A-\left(C-B\right)=B-A$$
11		1cnd	$$⊢\phi \to 1\in ℂ$$
12	11 4 6	subdird	$$⊢\phi \to \left(1-D\right)\left(C-A\right)=1\left(C-A\right)-D\left(C-A\right)$$
13	6	mullidd	$$⊢\phi \to 1\left(C-A\right)=C-A$$
14	13	oveq1d	$$⊢\phi \to 1\left(C-A\right)-D\left(C-A\right)=C-A-D\left(C-A\right)$$
15	12 14	eqtr2d	$$⊢\phi \to C-A-D\left(C-A\right)=\left(1-D\right)\left(C-A\right)$$
16	10 15	eqeq12d	$$⊢\phi \to \left(C-A-\left(C-B\right)=C-A-D\left(C-A\right)\leftrightarrow B-A=\left(1-D\right)\left(C-A\right)\right)$$
17	5 9 16	3bitr2d	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow B-A=\left(1-D\right)\left(C-A\right)\right)$$