Theorem affineequivne

Description: Equivalence between two ways of expressing A as an affine combination of B and C if B and C are not equal. (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 ℂ$$
	affineequivne.d	$$⊢\phi \to B\ne C$$
Assertion	affineequivne	$$⊢\phi \to \left(A=\left(1-D\right)B+DC\leftrightarrow D=\frac{A-B}{C-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		affineequivne.d	$$⊢\phi \to B\ne C$$
6	1 2 3 4	affineequiv3	$$⊢\phi \to \left(A=\left(1-D\right)B+DC\leftrightarrow A-B=D\left(C-B\right)\right)$$
7	1 2	subcld	$$⊢\phi \to A-B\in ℂ$$
8	3 2	subcld	$$⊢\phi \to C-B\in ℂ$$
9	5	necomd	$$⊢\phi \to C\ne B$$
10	3 2 9	subne0d	$$⊢\phi \to C-B\ne 0$$
11	7 4 8 10	divmul3d	$$⊢\phi \to \left(\frac{A-B}{C-B}=D\leftrightarrow A-B=D\left(C-B\right)\right)$$
12		eqcom	$$⊢\frac{A-B}{C-B}=D\leftrightarrow D=\frac{A-B}{C-B}$$
13	11 12	bitr3di	$$⊢\phi \to \left(A-B=D\left(C-B\right)\leftrightarrow D=\frac{A-B}{C-B}\right)$$
14	6 13	bitrd	$$⊢\phi \to \left(A=\left(1-D\right)B+DC\leftrightarrow D=\frac{A-B}{C-B}\right)$$