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 ) ) ) ) ) |