Metamath Proof Explorer

Theorem affineequiv

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 affineequiv 
|- ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> ( C - B ) = ( 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 4 3 mulcld 
 |-  ( ph -> ( D x. C ) e. CC )
6 4 1 mulcld 
 |-  ( ph -> ( D x. A ) e. CC )
7 3 5 6 subsubd 
 |-  ( ph -> ( C - ( ( D x. C ) - ( D x. A ) ) ) = ( ( C - ( D x. C ) ) + ( D x. A ) ) )
8 3 5 subcld 
 |-  ( ph -> ( C - ( D x. C ) ) e. CC )
9 8 6 addcomd 
 |-  ( ph -> ( ( C - ( D x. C ) ) + ( D x. A ) ) = ( ( D x. A ) + ( C - ( D x. C ) ) ) )
10 7 9 eqtr2d 
 |-  ( ph -> ( ( D x. A ) + ( C - ( D x. C ) ) ) = ( C - ( ( D x. C ) - ( D x. A ) ) ) )
11 1cnd 
 |-  ( ph -> 1 e. CC )
12 11 4 3 subdird 
 |-  ( ph -> ( ( 1 - D ) x. C ) = ( ( 1 x. C ) - ( D x. C ) ) )
13 3 mullidd 
 |-  ( ph -> ( 1 x. C ) = C )
14 13 oveq1d 
 |-  ( ph -> ( ( 1 x. C ) - ( D x. C ) ) = ( C - ( D x. C ) ) )
15 12 14 eqtrd 
 |-  ( ph -> ( ( 1 - D ) x. C ) = ( C - ( D x. C ) ) )
16 15 oveq2d 
 |-  ( ph -> ( ( D x. A ) + ( ( 1 - D ) x. C ) ) = ( ( D x. A ) + ( C - ( D x. C ) ) ) )
17 3 2 subcld 
 |-  ( ph -> ( C - B ) e. CC )
18 3 1 subcld 
 |-  ( ph -> ( C - A ) e. CC )
19 4 18 mulcld 
 |-  ( ph -> ( D x. ( C - A ) ) e. CC )
20 2 17 19 addsubassd 
 |-  ( ph -> ( ( B + ( C - B ) ) - ( D x. ( C - A ) ) ) = ( B + ( ( C - B ) - ( D x. ( C - A ) ) ) ) )
21 2 3 pncan3d 
 |-  ( ph -> ( B + ( C - B ) ) = C )
22 4 3 1 subdid 
 |-  ( ph -> ( D x. ( C - A ) ) = ( ( D x. C ) - ( D x. A ) ) )
23 21 22 oveq12d 
 |-  ( ph -> ( ( B + ( C - B ) ) - ( D x. ( C - A ) ) ) = ( C - ( ( D x. C ) - ( D x. A ) ) ) )
24 20 23 eqtr3d 
 |-  ( ph -> ( B + ( ( C - B ) - ( D x. ( C - A ) ) ) ) = ( C - ( ( D x. C ) - ( D x. A ) ) ) )
25 10 16 24 3eqtr4d 
 |-  ( ph -> ( ( D x. A ) + ( ( 1 - D ) x. C ) ) = ( B + ( ( C - B ) - ( D x. ( C - A ) ) ) ) )
26 25 eqeq2d 
 |-  ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> B = ( B + ( ( C - B ) - ( D x. ( C - A ) ) ) ) ) )
27 2 addridd 
 |-  ( ph -> ( B + 0 ) = B )
28 27 eqeq1d 
 |-  ( ph -> ( ( B + 0 ) = ( B + ( ( C - B ) - ( D x. ( C - A ) ) ) ) <-> B = ( B + ( ( C - B ) - ( D x. ( C - A ) ) ) ) ) )
29 0cnd 
 |-  ( ph -> 0 e. CC )
30 17 19 subcld 
 |-  ( ph -> ( ( C - B ) - ( D x. ( C - A ) ) ) e. CC )
31 2 29 30 addcand 
 |-  ( ph -> ( ( B + 0 ) = ( B + ( ( C - B ) - ( D x. ( C - A ) ) ) ) <-> 0 = ( ( C - B ) - ( D x. ( C - A ) ) ) ) )
32 26 28 31 3bitr2d 
 |-  ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> 0 = ( ( C - B ) - ( D x. ( C - A ) ) ) ) )
33 eqcom 
 |-  ( 0 = ( ( C - B ) - ( D x. ( C - A ) ) ) <-> ( ( C - B ) - ( D x. ( C - A ) ) ) = 0 )
34 32 33 bitrdi 
 |-  ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> ( ( C - B ) - ( D x. ( C - A ) ) ) = 0 ) )
35 17 19 subeq0ad 
 |-  ( ph -> ( ( ( C - B ) - ( D x. ( C - A ) ) ) = 0 <-> ( C - B ) = ( D x. ( C - A ) ) ) )
36 34 35 bitrd 
 |-  ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> ( C - B ) = ( D x. ( C - A ) ) ) )