Theorem affineequiv

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	affineequiv	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow C-B=D\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	4 3	mulcld	$$⊢\phi \to DC\in ℂ$$
6	4 1	mulcld	$$⊢\phi \to DA\in ℂ$$
7	3 5 6	subsubd	$$⊢\phi \to C-\left(DC-DA\right)=C-DC+DA$$
8	3 5	subcld	$$⊢\phi \to C-DC\in ℂ$$
9	8 6	addcomd	$$⊢\phi \to C-DC+DA=DA+C-DC$$
10	7 9	eqtr2d	$$⊢\phi \to DA+C-DC=C-\left(DC-DA\right)$$
11		1cnd	$$⊢\phi \to 1\in ℂ$$
12	11 4 3	subdird	$$⊢\phi \to \left(1-D\right)C=1C-DC$$
13	3	mulid2d	$$⊢\phi \to 1C=C$$
14	13	oveq1d	$$⊢\phi \to 1C-DC=C-DC$$
15	12 14	eqtrd	$$⊢\phi \to \left(1-D\right)C=C-DC$$
16	15	oveq2d	$$⊢\phi \to DA+\left(1-D\right)C=DA+C-DC$$
17	3 2	subcld	$$⊢\phi \to C-B\in ℂ$$
18	3 1	subcld	$$⊢\phi \to C-A\in ℂ$$
19	4 18	mulcld	$$⊢\phi \to D\left(C-A\right)\in ℂ$$
20	2 17 19	addsubassd	$$⊢\phi \to B+\left(C-B\right)-D\left(C-A\right)=B+\left(C-B\right)-D\left(C-A\right)$$
21	2 3	pncan3d	$$⊢\phi \to B+C-B=C$$
22	4 3 1	subdid	$$⊢\phi \to D\left(C-A\right)=DC-DA$$
23	21 22	oveq12d	$$⊢\phi \to B+\left(C-B\right)-D\left(C-A\right)=C-\left(DC-DA\right)$$
24	20 23	eqtr3d	$$⊢\phi \to B+\left(C-B\right)-D\left(C-A\right)=C-\left(DC-DA\right)$$
25	10 16 24	3eqtr4d	$$⊢\phi \to DA+\left(1-D\right)C=B+\left(C-B\right)-D\left(C-A\right)$$
26	25	eqeq2d	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow B=B+\left(C-B\right)-D\left(C-A\right)\right)$$
27	2	addid1d	$$⊢\phi \to B+0=B$$
28	27	eqeq1d	$$⊢\phi \to \left(B+0=B+\left(C-B\right)-D\left(C-A\right)\leftrightarrow B=B+\left(C-B\right)-D\left(C-A\right)\right)$$
29		0cnd	$$⊢\phi \to 0\in ℂ$$
30	17 19	subcld	$$⊢\phi \to C-B-D\left(C-A\right)\in ℂ$$
31	2 29 30	addcand	$$⊢\phi \to \left(B+0=B+\left(C-B\right)-D\left(C-A\right)\leftrightarrow 0=C-B-D\left(C-A\right)\right)$$
32	26 28 31	3bitr2d	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow 0=C-B-D\left(C-A\right)\right)$$
33		eqcom	$$⊢0=C-B-D\left(C-A\right)\leftrightarrow C-B-D\left(C-A\right)=0$$
34	32 33	bitrdi	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow C-B-D\left(C-A\right)=0\right)$$
35	17 19	subeq0ad	$$⊢\phi \to \left(C-B-D\left(C-A\right)=0\leftrightarrow C-B=D\left(C-A\right)\right)$$
36	34 35	bitrd	$$⊢\phi \to \left(B=DA+\left(1-D\right)C\leftrightarrow C-B=D\left(C-A\right)\right)$$