Theorem affineequiv2

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

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	affineequiv	|- ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> ( C - B ) = ( D x. ( C - A ) ) ) )
6	3 1	subcld	|- ( ph -> ( C - A ) e. CC )
7	3 2	subcld	|- ( ph -> ( C - B ) e. CC )
8	4 6	mulcld	|- ( ph -> ( D x. ( C - A ) ) e. CC )
9	6 7 8	subcanad	|- ( ph -> ( ( ( C - A ) - ( C - B ) ) = ( ( C - A ) - ( D x. ( C - A ) ) ) <-> ( C - B ) = ( D x. ( C - A ) ) ) )
10	3 1 2	nnncan1d	|- ( ph -> ( ( C - A ) - ( C - B ) ) = ( B - A ) )
11		1cnd	|- ( ph -> 1 e. CC )
12	11 4 6	subdird	|- ( ph -> ( ( 1 - D ) x. ( C - A ) ) = ( ( 1 x. ( C - A ) ) - ( D x. ( C - A ) ) ) )
13	6	mulid2d	|- ( ph -> ( 1 x. ( C - A ) ) = ( C - A ) )
14	13	oveq1d	|- ( ph -> ( ( 1 x. ( C - A ) ) - ( D x. ( C - A ) ) ) = ( ( C - A ) - ( D x. ( C - A ) ) ) )
15	12 14	eqtr2d	|- ( ph -> ( ( C - A ) - ( D x. ( C - A ) ) ) = ( ( 1 - D ) x. ( C - A ) ) )
16	10 15	eqeq12d	|- ( ph -> ( ( ( C - A ) - ( C - B ) ) = ( ( C - A ) - ( D x. ( C - A ) ) ) <-> ( B - A ) = ( ( 1 - D ) x. ( C - A ) ) ) )
17	5 9 16	3bitr2d	|- ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> ( B - A ) = ( ( 1 - D ) x. ( C - A ) ) ) )