Metamath Proof Explorer

Definition df-eeng

Description: Define the geometry structure for EE ^ N . (Contributed by Thierry Arnoux, 24-Aug-2017)

Ref Expression
Assertion df-eeng 
|- EEG = ( n e. NN |-> ( { <. ( 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 >. ) } ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceeng 
 |-  EEG
1 vn 
 |-  n
2 cn 
 |-  NN
3 cbs 
 |-  Base
4 cnx 
 |-  ndx
5 4 3 cfv 
 |-  ( Base ` ndx )
6 cee 
 |-  EE
7 1 cv 
 |-  n
8 7 6 cfv 
 |-  ( EE ` n )
9 5 8 cop 
 |-  <. ( Base ` ndx ) , ( EE ` n ) >.
10 cds 
 |-  dist
11 4 10 cfv 
 |-  ( dist ` ndx )
12 vx 
 |-  x
13 vy 
 |-  y
14 vi 
 |-  i
15 c1 
 |-  1
16 cfz 
 |-  ...
17 15 7 16 co 
 |-  ( 1 ... n )
18 12 cv 
 |-  x
19 14 cv 
 |-  i
20 19 18 cfv 
 |-  ( x ` i )
21 cmin 
 |-  -
22 13 cv 
 |-  y
23 19 22 cfv 
 |-  ( y ` i )
24 20 23 21 co 
 |-  ( ( x ` i ) - ( y ` i ) )
25 cexp 
 |-  ^
26 c2 
 |-  2
27 24 26 25 co 
 |-  ( ( ( x ` i ) - ( y ` i ) ) ^ 2 )
28 17 27 14 csu 
 |-  sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 )
29 12 13 8 8 28 cmpo 
 |-  ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) )
30 11 29 cop 
 |-  <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >.
31 9 30 cpr 
 |-  { <. ( Base ` ndx ) , ( EE ` n ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. }
32 citv 
 |-  Itv
33 4 32 cfv 
 |-  ( Itv ` ndx )
34 vz 
 |-  z
35 34 cv 
 |-  z
36 cbtwn 
 |-  Btwn
37 18 22 cop 
 |-  <. x , y >.
38 35 37 36 wbr 
 |-  z Btwn <. x , y >.
39 38 34 8 crab 
 |-  { z e. ( EE ` n ) | z Btwn <. x , y >. }
40 12 13 8 8 39 cmpo 
 |-  ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } )
41 33 40 cop 
 |-  <. ( Itv ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } ) >.
42 clng 
 |-  LineG
43 4 42 cfv 
 |-  ( LineG ` ndx )
44 18 csn 
 |-  { x }
45 8 44 cdif 
 |-  ( ( EE ` n ) \ { x } )
46 35 22 cop 
 |-  <. z , y >.
47 18 46 36 wbr 
 |-  x Btwn <. z , y >.
48 18 35 cop 
 |-  <. x , z >.
49 22 48 36 wbr 
 |-  y Btwn <. x , z >.
50 38 47 49 w3o 
 |-  ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. )
51 50 34 8 crab 
 |-  { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) }
52 12 13 8 45 51 cmpo 
 |-  ( 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 >. ) } )
53 43 52 cop 
 |-  <. ( 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 >. ) } ) >.
54 41 53 cpr 
 |-  { <. ( 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 >. ) } ) >. }
55 31 54 cun 
 |-  ( { <. ( 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 >. ) } ) >. } )
56 1 2 55 cmpt 
 |-  ( n e. NN |-> ( { <. ( 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 >. ) } ) >. } ) )
57 0 56 wceq 
 |-  EEG = ( n e. NN |-> ( { <. ( 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 >. ) } ) >. } ) )