Metamath Proof Explorer

Theorem affineequiv3

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 affineequiv3 
|- ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> ( A - B ) = ( D x. ( 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 1cnd 
 |-  ( ph -> 1 e. CC )
6 5 4 subcld 
 |-  ( ph -> ( 1 - D ) e. CC )
7 6 2 mulcld 
 |-  ( ph -> ( ( 1 - D ) x. B ) e. CC )
8 4 3 mulcld 
 |-  ( ph -> ( D x. C ) e. CC )
9 7 8 addcomd 
 |-  ( ph -> ( ( ( 1 - D ) x. B ) + ( D x. C ) ) = ( ( D x. C ) + ( ( 1 - D ) x. B ) ) )
10 9 eqeq2d 
 |-  ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> A = ( ( D x. C ) + ( ( 1 - D ) x. B ) ) ) )
11 3 1 2 4 affineequiv 
 |-  ( ph -> ( A = ( ( D x. C ) + ( ( 1 - D ) x. B ) ) <-> ( B - A ) = ( D x. ( B - C ) ) ) )
12 1 2 negsubdi2d 
 |-  ( ph -> -u ( A - B ) = ( B - A ) )
13 12 eqcomd 
 |-  ( ph -> ( B - A ) = -u ( A - B ) )
14 13 eqeq1d 
 |-  ( ph -> ( ( B - A ) = ( D x. ( B - C ) ) <-> -u ( A - B ) = ( D x. ( B - C ) ) ) )
15 3 2 negsubdi2d 
 |-  ( ph -> -u ( C - B ) = ( B - C ) )
16 15 eqcomd 
 |-  ( ph -> ( B - C ) = -u ( C - B ) )
17 16 oveq2d 
 |-  ( ph -> ( D x. ( B - C ) ) = ( D x. -u ( C - B ) ) )
18 3 2 subcld 
 |-  ( ph -> ( C - B ) e. CC )
19 4 18 mulneg2d 
 |-  ( ph -> ( D x. -u ( C - B ) ) = -u ( D x. ( C - B ) ) )
20 17 19 eqtrd 
 |-  ( ph -> ( D x. ( B - C ) ) = -u ( D x. ( C - B ) ) )
21 20 eqeq2d 
 |-  ( ph -> ( -u ( A - B ) = ( D x. ( B - C ) ) <-> -u ( A - B ) = -u ( D x. ( C - B ) ) ) )
22 1 2 subcld 
 |-  ( ph -> ( A - B ) e. CC )
23 4 18 mulcld 
 |-  ( ph -> ( D x. ( C - B ) ) e. CC )
24 22 23 neg11ad 
 |-  ( ph -> ( -u ( A - B ) = -u ( D x. ( C - B ) ) <-> ( A - B ) = ( D x. ( C - B ) ) ) )
25 14 21 24 3bitrd 
 |-  ( ph -> ( ( B - A ) = ( D x. ( B - C ) ) <-> ( A - B ) = ( D x. ( C - B ) ) ) )
26 10 11 25 3bitrd 
 |-  ( ph -> ( A = ( ( ( 1 - D ) x. B ) + ( D x. C ) ) <-> ( A - B ) = ( D x. ( C - B ) ) ) )