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	|- ( ph -> A e. CC )
	affineequiv.b	|- ( ph -> B e. CC )
	affineequiv.c	|- ( ph -> C e. CC )
	affineequiv.d	|- ( ph -> D e. CC )
Assertion	affineequiv4	|- ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> A = ( ( D x. ( C - B ) ) + 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	1 2 3 4	affineequiv3	|- ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> ( A - B ) = ( D x. ( C - B ) ) ) )
6	3 2	subcld	|- ( ph -> ( C - B ) e. CC )
7	4 6	mulcld	|- ( ph -> ( D x. ( C - B ) ) e. CC )
8	1 2 7	subadd2d	|- ( ph -> ( ( A - B ) = ( D x. ( C - B ) ) <-> ( ( D x. ( C - B ) ) + B ) = A ) )
9		eqcom	|- ( ( ( D x. ( C - B ) ) + B ) = A <-> A = ( ( D x. ( C - B ) ) + B ) )
10	8 9	bitrdi	|- ( ph -> ( ( A - B ) = ( D x. ( C - B ) ) <-> A = ( ( D x. ( C - B ) ) + B ) ) )
11	5 10	bitrd	|- ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> A = ( ( D x. ( C - B ) ) + B ) ) )