Theorem affineequiv4

Description: Equivalence between two ways of expressing A as an affine combination of B and C . (Contributed by AV, 22-Jan-2023)

	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	affineequiv4	$$⊢\phi \to \left(A=\left(1-D\right)B+DC\leftrightarrow A=D\left(C-B\right)+B\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	affineequiv3	$$⊢\phi \to \left(A=\left(1-D\right)B+DC\leftrightarrow A-B=D\left(C-B\right)\right)$$
6	3 2	subcld	$$⊢\phi \to C-B\in ℂ$$
7	4 6	mulcld	$$⊢\phi \to D\left(C-B\right)\in ℂ$$
8	1 2 7	subadd2d	$$⊢\phi \to \left(A-B=D\left(C-B\right)\leftrightarrow D\left(C-B\right)+B=A\right)$$
9		eqcom	$$⊢D\left(C-B\right)+B=A\leftrightarrow A=D\left(C-B\right)+B$$
10	8 9	bitrdi	$$⊢\phi \to \left(A-B=D\left(C-B\right)\leftrightarrow A=D\left(C-B\right)+B\right)$$
11	5 10	bitrd	$$⊢\phi \to \left(A=\left(1-D\right)B+DC\leftrightarrow A=D\left(C-B\right)+B\right)$$