Metamath Proof Explorer

Theorem affinecomb2

Description: Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023)

Ref Expression
Hypotheses affinecomb1.a 
|- ( ph -> A e. RR )
affinecomb1.b 
|- ( ph -> B e. RR )
affinecomb1.c 
|- ( ph -> C e. RR )
affinecomb1.d 
|- ( ph -> B =/= C )
affinecomb1.e 
|- ( ph -> E e. RR )
affinecomb1.f 
|- ( ph -> F e. RR )
affinecomb1.g 
|- ( ph -> G e. RR )
Assertion affinecomb2 
|- ( ph -> ( E. t e. RR ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) <-> ( ( C - B ) x. E ) = ( ( ( G - F ) x. A ) + ( ( F x. C ) - ( B x. G ) ) ) ) )

Proof

Step Hyp Ref Expression
1 affinecomb1.a 
 |-  ( ph -> A e. RR )
2 affinecomb1.b 
 |-  ( ph -> B e. RR )
3 affinecomb1.c 
 |-  ( ph -> C e. RR )
4 affinecomb1.d 
 |-  ( ph -> B =/= C )
5 affinecomb1.e 
 |-  ( ph -> E e. RR )
6 affinecomb1.f 
 |-  ( ph -> F e. RR )
7 affinecomb1.g 
 |-  ( ph -> G e. RR )
8 eqid 
 |-  ( ( G - F ) / ( C - B ) ) = ( ( G - F ) / ( C - B ) )
9 1 2 3 4 5 6 7 8 affinecomb1 
 |-  ( ph -> ( E. t e. RR ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) <-> E = ( ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) + F ) ) )
10 5 recnd 
 |-  ( ph -> E e. CC )
11 7 recnd 
 |-  ( ph -> G e. CC )
12 6 recnd 
 |-  ( ph -> F e. CC )
13 11 12 subcld 
 |-  ( ph -> ( G - F ) e. CC )
14 3 recnd 
 |-  ( ph -> C e. CC )
15 2 recnd 
 |-  ( ph -> B e. CC )
16 14 15 subcld 
 |-  ( ph -> ( C - B ) e. CC )
17 4 necomd 
 |-  ( ph -> C =/= B )
18 14 15 17 subne0d 
 |-  ( ph -> ( C - B ) =/= 0 )
19 13 16 18 divcld 
 |-  ( ph -> ( ( G - F ) / ( C - B ) ) e. CC )
20 1 recnd 
 |-  ( ph -> A e. CC )
21 20 15 subcld 
 |-  ( ph -> ( A - B ) e. CC )
22 19 21 mulcld 
 |-  ( ph -> ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) e. CC )
23 22 12 addcld 
 |-  ( ph -> ( ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) + F ) e. CC )
24 10 23 16 18 mulcand 
 |-  ( ph -> ( ( ( C - B ) x. E ) = ( ( C - B ) x. ( ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) + F ) ) <-> E = ( ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) + F ) ) )
25 16 22 12 adddid 
 |-  ( ph -> ( ( C - B ) x. ( ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) + F ) ) = ( ( ( C - B ) x. ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) ) + ( ( C - B ) x. F ) ) )
26 13 16 18 divcan2d 
 |-  ( ph -> ( ( C - B ) x. ( ( G - F ) / ( C - B ) ) ) = ( G - F ) )
27 26 oveq1d 
 |-  ( ph -> ( ( ( C - B ) x. ( ( G - F ) / ( C - B ) ) ) x. ( A - B ) ) = ( ( G - F ) x. ( A - B ) ) )
28 16 19 21 mulassd 
 |-  ( ph -> ( ( ( C - B ) x. ( ( G - F ) / ( C - B ) ) ) x. ( A - B ) ) = ( ( C - B ) x. ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) ) )
29 13 20 15 subdid 
 |-  ( ph -> ( ( G - F ) x. ( A - B ) ) = ( ( ( G - F ) x. A ) - ( ( G - F ) x. B ) ) )
30 27 28 29 3eqtr3d 
 |-  ( ph -> ( ( C - B ) x. ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) ) = ( ( ( G - F ) x. A ) - ( ( G - F ) x. B ) ) )
31 14 15 12 subdird 
 |-  ( ph -> ( ( C - B ) x. F ) = ( ( C x. F ) - ( B x. F ) ) )
32 30 31 oveq12d 
 |-  ( ph -> ( ( ( C - B ) x. ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) ) + ( ( C - B ) x. F ) ) = ( ( ( ( G - F ) x. A ) - ( ( G - F ) x. B ) ) + ( ( C x. F ) - ( B x. F ) ) ) )
33 13 20 mulcld 
 |-  ( ph -> ( ( G - F ) x. A ) e. CC )
34 13 15 mulcld 
 |-  ( ph -> ( ( G - F ) x. B ) e. CC )
35 14 12 mulcld 
 |-  ( ph -> ( C x. F ) e. CC )
36 15 12 mulcld 
 |-  ( ph -> ( B x. F ) e. CC )
37 35 36 subcld 
 |-  ( ph -> ( ( C x. F ) - ( B x. F ) ) e. CC )
38 33 34 37 subadd23d 
 |-  ( ph -> ( ( ( ( G - F ) x. A ) - ( ( G - F ) x. B ) ) + ( ( C x. F ) - ( B x. F ) ) ) = ( ( ( G - F ) x. A ) + ( ( ( C x. F ) - ( B x. F ) ) - ( ( G - F ) x. B ) ) ) )
39 32 38 eqtrd 
 |-  ( ph -> ( ( ( C - B ) x. ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) ) + ( ( C - B ) x. F ) ) = ( ( ( G - F ) x. A ) + ( ( ( C x. F ) - ( B x. F ) ) - ( ( G - F ) x. B ) ) ) )
40 14 12 mulcomd 
 |-  ( ph -> ( C x. F ) = ( F x. C ) )
41 15 12 mulcomd 
 |-  ( ph -> ( B x. F ) = ( F x. B ) )
42 40 41 oveq12d 
 |-  ( ph -> ( ( C x. F ) - ( B x. F ) ) = ( ( F x. C ) - ( F x. B ) ) )
43 11 12 15 subdird 
 |-  ( ph -> ( ( G - F ) x. B ) = ( ( G x. B ) - ( F x. B ) ) )
44 42 43 oveq12d 
 |-  ( ph -> ( ( ( C x. F ) - ( B x. F ) ) - ( ( G - F ) x. B ) ) = ( ( ( F x. C ) - ( F x. B ) ) - ( ( G x. B ) - ( F x. B ) ) ) )
45 12 14 mulcld 
 |-  ( ph -> ( F x. C ) e. CC )
46 11 15 mulcld 
 |-  ( ph -> ( G x. B ) e. CC )
47 12 15 mulcld 
 |-  ( ph -> ( F x. B ) e. CC )
48 45 46 47 nnncan2d 
 |-  ( ph -> ( ( ( F x. C ) - ( F x. B ) ) - ( ( G x. B ) - ( F x. B ) ) ) = ( ( F x. C ) - ( G x. B ) ) )
49 11 15 mulcomd 
 |-  ( ph -> ( G x. B ) = ( B x. G ) )
50 49 oveq2d 
 |-  ( ph -> ( ( F x. C ) - ( G x. B ) ) = ( ( F x. C ) - ( B x. G ) ) )
51 44 48 50 3eqtrd 
 |-  ( ph -> ( ( ( C x. F ) - ( B x. F ) ) - ( ( G - F ) x. B ) ) = ( ( F x. C ) - ( B x. G ) ) )
52 51 oveq2d 
 |-  ( ph -> ( ( ( G - F ) x. A ) + ( ( ( C x. F ) - ( B x. F ) ) - ( ( G - F ) x. B ) ) ) = ( ( ( G - F ) x. A ) + ( ( F x. C ) - ( B x. G ) ) ) )
53 25 39 52 3eqtrd 
 |-  ( ph -> ( ( C - B ) x. ( ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) + F ) ) = ( ( ( G - F ) x. A ) + ( ( F x. C ) - ( B x. G ) ) ) )
54 53 eqeq2d 
 |-  ( ph -> ( ( ( C - B ) x. E ) = ( ( C - B ) x. ( ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) + F ) ) <-> ( ( C - B ) x. E ) = ( ( ( G - F ) x. A ) + ( ( F x. C ) - ( B x. G ) ) ) ) )
55 9 24 54 3bitr2d 
 |-  ( ph -> ( E. t e. RR ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) <-> ( ( C - B ) x. E ) = ( ( ( G - F ) x. A ) + ( ( F x. C ) - ( B x. G ) ) ) ) )