Metamath Proof Explorer

Theorem affinecomb1

Description: Combination of two real affine combinations, one class variable resolved. (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 )
affinecomb1.s 
|- S = ( ( G - F ) / ( C - B ) )
Assertion affinecomb1 
|- ( ph -> ( E. t e. RR ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) <-> E = ( ( S x. ( A - B ) ) + F ) ) )

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 affinecomb1.s 
 |-  S = ( ( G - F ) / ( C - B ) )
9 1 adantr 
 |-  ( ( ph /\ t e. RR ) -> A e. RR )
10 9 recnd 
 |-  ( ( ph /\ t e. RR ) -> A e. CC )
11 2 adantr 
 |-  ( ( ph /\ t e. RR ) -> B e. RR )
12 11 recnd 
 |-  ( ( ph /\ t e. RR ) -> B e. CC )
13 3 adantr 
 |-  ( ( ph /\ t e. RR ) -> C e. RR )
14 13 recnd 
 |-  ( ( ph /\ t e. RR ) -> C e. CC )
15 simpr 
 |-  ( ( ph /\ t e. RR ) -> t e. RR )
16 15 recnd 
 |-  ( ( ph /\ t e. RR ) -> t e. CC )
17 4 adantr 
 |-  ( ( ph /\ t e. RR ) -> B =/= C )
18 10 12 14 16 17 affineequivne 
 |-  ( ( ph /\ t e. RR ) -> ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) <-> t = ( ( A - B ) / ( C - B ) ) ) )
19 oveq2 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( 1 - t ) = ( 1 - ( ( A - B ) / ( C - B ) ) ) )
20 19 oveq1d 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( ( 1 - t ) x. F ) = ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) )
21 oveq1 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( t x. G ) = ( ( ( A - B ) / ( C - B ) ) x. G ) )
22 20 21 oveq12d 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( ( ( 1 - t ) x. F ) + ( t x. G ) ) = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) )
23 22 eqeq2d 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) <-> E = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) ) )
24 23 adantl 
 |-  ( ( ( ph /\ t e. RR ) /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) <-> E = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) ) )
25 eqidd 
 |-  ( ph -> ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) = ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) )
26 1 2 resubcld 
 |-  ( ph -> ( A - B ) e. RR )
27 3 2 resubcld 
 |-  ( ph -> ( C - B ) e. RR )
28 3 recnd 
 |-  ( ph -> C e. CC )
29 2 recnd 
 |-  ( ph -> B e. CC )
30 4 necomd 
 |-  ( ph -> C =/= B )
31 28 29 30 subne0d 
 |-  ( ph -> ( C - B ) =/= 0 )
32 26 27 31 redivcld 
 |-  ( ph -> ( ( A - B ) / ( C - B ) ) e. RR )
33 7 6 resubcld 
 |-  ( ph -> ( G - F ) e. RR )
34 32 33 remulcld 
 |-  ( ph -> ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) e. RR )
35 34 6 readdcld 
 |-  ( ph -> ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) e. RR )
36 35 recnd 
 |-  ( ph -> ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) e. CC )
37 6 recnd 
 |-  ( ph -> F e. CC )
38 7 recnd 
 |-  ( ph -> G e. CC )
39 32 recnd 
 |-  ( ph -> ( ( A - B ) / ( C - B ) ) e. CC )
40 36 37 38 39 affineequiv4 
 |-  ( ph -> ( ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) <-> ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) = ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) ) )
41 25 40 mpbird 
 |-  ( ph -> ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) )
42 26 recnd 
 |-  ( ph -> ( A - B ) e. CC )
43 27 recnd 
 |-  ( ph -> ( C - B ) e. CC )
44 33 recnd 
 |-  ( ph -> ( G - F ) e. CC )
45 42 43 44 31 div13d 
 |-  ( ph -> ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) = ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) )
46 8 oveq1i 
 |-  ( S x. ( A - B ) ) = ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) )
47 45 46 eqtr4di 
 |-  ( ph -> ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) = ( S x. ( A - B ) ) )
48 47 oveq1d 
 |-  ( ph -> ( ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) + F ) = ( ( S x. ( A - B ) ) + F ) )
49 41 48 eqtr3d 
 |-  ( ph -> ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) = ( ( S x. ( A - B ) ) + F ) )
50 49 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) = ( ( S x. ( A - B ) ) + F ) )
51 50 eqeq2d 
 |-  ( ( ph /\ t e. RR ) -> ( E = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) <-> E = ( ( S x. ( A - B ) ) + F ) ) )
52 51 biimpd 
 |-  ( ( ph /\ t e. RR ) -> ( E = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) -> E = ( ( S x. ( A - B ) ) + F ) ) )
53 52 adantr 
 |-  ( ( ( ph /\ t e. RR ) /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( E = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. F ) + ( ( ( A - B ) / ( C - B ) ) x. G ) ) -> E = ( ( S x. ( A - B ) ) + F ) ) )
54 24 53 sylbid 
 |-  ( ( ( ph /\ t e. RR ) /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) -> E = ( ( S x. ( A - B ) ) + F ) ) )
55 54 ex 
 |-  ( ( ph /\ t e. RR ) -> ( t = ( ( A - B ) / ( C - B ) ) -> ( E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) -> E = ( ( S x. ( A - B ) ) + F ) ) ) )
56 18 55 sylbid 
 |-  ( ( ph /\ t e. RR ) -> ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) -> ( E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) -> E = ( ( S x. ( A - B ) ) + F ) ) ) )
57 56 impd 
 |-  ( ( ph /\ t e. RR ) -> ( ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) -> E = ( ( S x. ( A - B ) ) + F ) ) )
58 57 rexlimdva 
 |-  ( ph -> ( E. t e. RR ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) -> E = ( ( S x. ( A - B ) ) + F ) ) )
59 5 adantr 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> E e. RR )
60 59 recnd 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> E e. CC )
61 37 adantr 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> F e. CC )
62 38 adantr 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> G e. CC )
63 32 adantr 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( ( A - B ) / ( C - B ) ) e. RR )
64 eleq1 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( t e. RR <-> ( ( A - B ) / ( C - B ) ) e. RR ) )
65 64 adantl 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( t e. RR <-> ( ( A - B ) / ( C - B ) ) e. RR ) )
66 63 65 mpbird 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> t e. RR )
67 66 recnd 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> t e. CC )
68 60 61 62 67 affineequiv4 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) <-> E = ( ( t x. ( G - F ) ) + F ) ) )
69 19 oveq1d 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( ( 1 - t ) x. B ) = ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. B ) )
70 oveq1 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( t x. C ) = ( ( ( A - B ) / ( C - B ) ) x. C ) )
71 69 70 oveq12d 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( ( ( 1 - t ) x. B ) + ( t x. C ) ) = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. B ) + ( ( ( A - B ) / ( C - B ) ) x. C ) ) )
72 eqidd 
 |-  ( ph -> ( ( A - B ) / ( C - B ) ) = ( ( A - B ) / ( C - B ) ) )
73 1 recnd 
 |-  ( ph -> A e. CC )
74 73 29 28 39 4 affineequivne 
 |-  ( ph -> ( A = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. B ) + ( ( ( A - B ) / ( C - B ) ) x. C ) ) <-> ( ( A - B ) / ( C - B ) ) = ( ( A - B ) / ( C - B ) ) ) )
75 72 74 mpbird 
 |-  ( ph -> A = ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. B ) + ( ( ( A - B ) / ( C - B ) ) x. C ) ) )
76 75 eqcomd 
 |-  ( ph -> ( ( ( 1 - ( ( A - B ) / ( C - B ) ) ) x. B ) + ( ( ( A - B ) / ( C - B ) ) x. C ) ) = A )
77 71 76 sylan9eqr 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( ( ( 1 - t ) x. B ) + ( t x. C ) ) = A )
78 77 eqcomd 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) )
79 78 biantrurd 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) <-> ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) ) )
80 45 adantr 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) = ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) )
81 oveq1 
 |-  ( t = ( ( A - B ) / ( C - B ) ) -> ( t x. ( G - F ) ) = ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) )
82 81 adantl 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( t x. ( G - F ) ) = ( ( ( A - B ) / ( C - B ) ) x. ( G - F ) ) )
83 46 a1i 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( S x. ( A - B ) ) = ( ( ( G - F ) / ( C - B ) ) x. ( A - B ) ) )
84 80 82 83 3eqtr4d 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( t x. ( G - F ) ) = ( S x. ( A - B ) ) )
85 84 oveq1d 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( ( t x. ( G - F ) ) + F ) = ( ( S x. ( A - B ) ) + F ) )
86 85 eqeq2d 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( E = ( ( t x. ( G - F ) ) + F ) <-> E = ( ( S x. ( A - B ) ) + F ) ) )
87 68 79 86 3bitr3d 
 |-  ( ( ph /\ t = ( ( A - B ) / ( C - B ) ) ) -> ( ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) <-> E = ( ( S x. ( A - B ) ) + F ) ) )
88 32 87 rspcedv 
 |-  ( ph -> ( E = ( ( S x. ( A - B ) ) + F ) -> E. t e. RR ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) ) )
89 58 88 impbid 
 |-  ( ph -> ( E. t e. RR ( A = ( ( ( 1 - t ) x. B ) + ( t x. C ) ) /\ E = ( ( ( 1 - t ) x. F ) + ( t x. G ) ) ) <-> E = ( ( S x. ( A - B ) ) + F ) ) )