Step |
Hyp |
Ref |
Expression |
1 |
|
ebtwntg.1 |
|- ( ph -> N e. NN ) |
2 |
|
ebtwntg.2 |
|- P = ( Base ` ( EEG ` N ) ) |
3 |
|
ebtwntg.3 |
|- I = ( Itv ` ( EEG ` N ) ) |
4 |
|
ebtwntg.x |
|- ( ph -> X e. P ) |
5 |
|
ebtwntg.y |
|- ( ph -> Y e. P ) |
6 |
|
ebtwntg.z |
|- ( ph -> Z e. P ) |
7 |
|
itvid |
|- Itv = Slot ( Itv ` ndx ) |
8 |
|
fvexd |
|- ( ph -> ( EEG ` N ) e. _V ) |
9 |
|
eengstr |
|- ( N e. NN -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. ) |
10 |
1 9
|
syl |
|- ( ph -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. ) |
11 |
|
structn0fun |
|- ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> Fun ( ( EEG ` N ) \ { (/) } ) ) |
12 |
10 11
|
syl |
|- ( ph -> Fun ( ( EEG ` N ) \ { (/) } ) ) |
13 |
|
structcnvcnv |
|- ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) ) |
14 |
10 13
|
syl |
|- ( ph -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) ) |
15 |
14
|
funeqd |
|- ( ph -> ( Fun `' `' ( EEG ` N ) <-> Fun ( ( EEG ` N ) \ { (/) } ) ) ) |
16 |
12 15
|
mpbird |
|- ( ph -> Fun `' `' ( EEG ` N ) ) |
17 |
|
opex |
|- <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. _V |
18 |
17
|
prid1 |
|- <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } |
19 |
|
elun2 |
|- ( <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } -> <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) ) |
20 |
18 19
|
ax-mp |
|- <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) |
21 |
|
eengv |
|- ( N e. NN -> ( EEG ` N ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) ) |
22 |
1 21
|
syl |
|- ( ph -> ( EEG ` N ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) ) |
23 |
20 22
|
eleqtrrid |
|- ( ph -> <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. ( EEG ` N ) ) |
24 |
|
fvex |
|- ( EE ` N ) e. _V |
25 |
24 24
|
mpoex |
|- ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) e. _V |
26 |
25
|
a1i |
|- ( ph -> ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) e. _V ) |
27 |
7 8 16 23 26
|
strfv2d |
|- ( ph -> ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) = ( Itv ` ( EEG ` N ) ) ) |
28 |
3 27
|
eqtr4id |
|- ( ph -> I = ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) ) |
29 |
|
simprl |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X ) |
30 |
|
simprr |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y ) |
31 |
29 30
|
opeq12d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> <. x , y >. = <. X , Y >. ) |
32 |
31
|
breq2d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( z Btwn <. x , y >. <-> z Btwn <. X , Y >. ) ) |
33 |
32
|
rabbidv |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> { z e. ( EE ` N ) | z Btwn <. x , y >. } = { z e. ( EE ` N ) | z Btwn <. X , Y >. } ) |
34 |
4 2
|
eleqtrdi |
|- ( ph -> X e. ( Base ` ( EEG ` N ) ) ) |
35 |
|
eengbas |
|- ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) ) |
36 |
1 35
|
syl |
|- ( ph -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) ) |
37 |
34 36
|
eleqtrrd |
|- ( ph -> X e. ( EE ` N ) ) |
38 |
5 2
|
eleqtrdi |
|- ( ph -> Y e. ( Base ` ( EEG ` N ) ) ) |
39 |
38 36
|
eleqtrrd |
|- ( ph -> Y e. ( EE ` N ) ) |
40 |
24
|
rabex |
|- { z e. ( EE ` N ) | z Btwn <. X , Y >. } e. _V |
41 |
40
|
a1i |
|- ( ph -> { z e. ( EE ` N ) | z Btwn <. X , Y >. } e. _V ) |
42 |
28 33 37 39 41
|
ovmpod |
|- ( ph -> ( X I Y ) = { z e. ( EE ` N ) | z Btwn <. X , Y >. } ) |
43 |
42
|
eleq2d |
|- ( ph -> ( Z e. ( X I Y ) <-> Z e. { z e. ( EE ` N ) | z Btwn <. X , Y >. } ) ) |
44 |
6 2
|
eleqtrdi |
|- ( ph -> Z e. ( Base ` ( EEG ` N ) ) ) |
45 |
44 36
|
eleqtrrd |
|- ( ph -> Z e. ( EE ` N ) ) |
46 |
|
breq1 |
|- ( z = Z -> ( z Btwn <. X , Y >. <-> Z Btwn <. X , Y >. ) ) |
47 |
46
|
elrab3 |
|- ( Z e. ( EE ` N ) -> ( Z e. { z e. ( EE ` N ) | z Btwn <. X , Y >. } <-> Z Btwn <. X , Y >. ) ) |
48 |
45 47
|
syl |
|- ( ph -> ( Z e. { z e. ( EE ` N ) | z Btwn <. X , Y >. } <-> Z Btwn <. X , Y >. ) ) |
49 |
43 48
|
bitr2d |
|- ( ph -> ( Z Btwn <. X , Y >. <-> Z e. ( X I Y ) ) ) |