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	|- ( ph -> A e. CC )
	affineequiv.b	|- ( ph -> B e. CC )
	affineequiv.c	|- ( ph -> C e. CC )
	affineequiv.d	|- ( ph -> D e. CC )
	affineequivne.d	|- ( ph -> B =/= C )
Assertion	affineequivne	|- ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> D = ( ( A - B ) / ( C - B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		affineequiv.a	|- ( ph -> A e. CC )
2		affineequiv.b	|- ( ph -> B e. CC )
3		affineequiv.c	|- ( ph -> C e. CC )
4		affineequiv.d	|- ( ph -> D e. CC )
5		affineequivne.d	|- ( ph -> B =/= C )
6	1 2 3 4	affineequiv3	|- ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> ( A - B ) = ( D x. ( C - B ) ) ) )
7	1 2	subcld	|- ( ph -> ( A - B ) e. CC )
8	3 2	subcld	|- ( ph -> ( C - B ) e. CC )
9	5	necomd	|- ( ph -> C =/= B )
10	3 2 9	subne0d	|- ( ph -> ( C - B ) =/= 0 )
11	7 4 8 10	divmul3d	|- ( ph -> ( ( ( A - B ) / ( C - B ) ) = D <-> ( A - B ) = ( D x. ( C - B ) ) ) )
12		eqcom	|- ( ( ( A - B ) / ( C - B ) ) = D <-> D = ( ( A - B ) / ( C - B ) ) )
13	11 12	bitr3di	|- ( ph -> ( ( A - B ) = ( D x. ( C - B ) ) <-> D = ( ( A - B ) / ( C - B ) ) ) )
14	6 13	bitrd	|- ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> D = ( ( A - B ) / ( C - B ) ) ) )