MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eeng Structured version   Unicode version

Definition df-eeng 24698
Description: Define the geometry structure for  EE ^ N. (Contributed by Thierry Arnoux, 24-Aug-2017.)
Assertion
Ref Expression
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
>. ) } ) >. } ) )
Distinct variable group:    i, n, x, y, z

Detailed syntax breakdown of Definition df-eeng
StepHypRef Expression
1 ceeng 24697 . 2  class EEG
2 vn . . 3  setvar  n
3 cn 10576 . . 3  class  NN
4 cnx 14838 . . . . . . 7  class  ndx
5 cbs 14841 . . . . . . 7  class  Base
64, 5cfv 5569 . . . . . 6  class  ( Base `  ndx )
72cv 1404 . . . . . . 7  class  n
8 cee 24608 . . . . . . 7  class  EE
97, 8cfv 5569 . . . . . 6  class  ( EE
`  n )
106, 9cop 3978 . . . . 5  class  <. ( Base `  ndx ) ,  ( EE `  n
) >.
11 cds 14918 . . . . . . 7  class  dist
124, 11cfv 5569 . . . . . 6  class  ( dist `  ndx )
13 vx . . . . . . 7  setvar  x
14 vy . . . . . . 7  setvar  y
15 c1 9523 . . . . . . . . 9  class  1
16 cfz 11726 . . . . . . . . 9  class  ...
1715, 7, 16co 6278 . . . . . . . 8  class  ( 1 ... n )
18 vi . . . . . . . . . . . 12  setvar  i
1918cv 1404 . . . . . . . . . . 11  class  i
2013cv 1404 . . . . . . . . . . 11  class  x
2119, 20cfv 5569 . . . . . . . . . 10  class  ( x `
 i )
2214cv 1404 . . . . . . . . . . 11  class  y
2319, 22cfv 5569 . . . . . . . . . 10  class  ( y `
 i )
24 cmin 9841 . . . . . . . . . 10  class  -
2521, 23, 24co 6278 . . . . . . . . 9  class  ( ( x `  i )  -  ( y `  i ) )
26 c2 10626 . . . . . . . . 9  class  2
27 cexp 12210 . . . . . . . . 9  class  ^
2825, 26, 27co 6278 . . . . . . . 8  class  ( ( ( x `  i
)  -  ( y `
 i ) ) ^ 2 )
2917, 28, 18csu 13657 . . . . . . 7  class  sum_ i  e.  ( 1 ... n
) ( ( ( x `  i )  -  ( y `  i ) ) ^
2 )
3013, 14, 9, 9, 29cmpt2 6280 . . . . . 6  class  ( x  e.  ( EE `  n ) ,  y  e.  ( EE `  n )  |->  sum_ i  e.  ( 1 ... n
) ( ( ( x `  i )  -  ( y `  i ) ) ^
2 ) )
3112, 30cop 3978 . . . . 5  class  <. ( dist `  ndx ) ,  ( x  e.  ( EE `  n ) ,  y  e.  ( EE `  n ) 
|->  sum_ i  e.  ( 1 ... n ) ( ( ( x `
 i )  -  ( y `  i
) ) ^ 2 ) ) >.
3210, 31cpr 3974 . . . 4  class  { <. (
Base `  ndx ) ,  ( EE `  n
) >. ,  <. ( dist `  ndx ) ,  ( x  e.  ( EE `  n ) ,  y  e.  ( EE `  n ) 
|->  sum_ i  e.  ( 1 ... n ) ( ( ( x `
 i )  -  ( y `  i
) ) ^ 2 ) ) >. }
33 citv 24212 . . . . . . 7  class Itv
344, 33cfv 5569 . . . . . 6  class  (Itv `  ndx )
35 vz . . . . . . . . . 10  setvar  z
3635cv 1404 . . . . . . . . 9  class  z
3720, 22cop 3978 . . . . . . . . 9  class  <. x ,  y >.
38 cbtwn 24609 . . . . . . . . 9  class  Btwn
3936, 37, 38wbr 4395 . . . . . . . 8  wff  z  Btwn  <.
x ,  y >.
4039, 35, 9crab 2758 . . . . . . 7  class  { z  e.  ( EE `  n )  |  z 
Btwn  <. x ,  y
>. }
4113, 14, 9, 9, 40cmpt2 6280 . . . . . 6  class  ( x  e.  ( EE `  n ) ,  y  e.  ( EE `  n )  |->  { z  e.  ( EE `  n )  |  z 
Btwn  <. x ,  y
>. } )
4234, 41cop 3978 . . . . 5  class  <. (Itv ` 
ndx ) ,  ( x  e.  ( EE
`  n ) ,  y  e.  ( EE
`  n )  |->  { z  e.  ( EE
`  n )  |  z  Btwn  <. x ,  y >. } ) >.
43 clng 24213 . . . . . . 7  class LineG
444, 43cfv 5569 . . . . . 6  class  (LineG `  ndx )
4520csn 3972 . . . . . . . 8  class  { x }
469, 45cdif 3411 . . . . . . 7  class  ( ( EE `  n ) 
\  { x }
)
4736, 22cop 3978 . . . . . . . . . 10  class  <. z ,  y >.
4820, 47, 38wbr 4395 . . . . . . . . 9  wff  x  Btwn  <.
z ,  y >.
4920, 36cop 3978 . . . . . . . . . 10  class  <. x ,  z >.
5022, 49, 38wbr 4395 . . . . . . . . 9  wff  y  Btwn  <.
x ,  z >.
5139, 48, 50w3o 973 . . . . . . . 8  wff  ( z 
Btwn  <. x ,  y
>.  \/  x  Btwn  <. z ,  y >.  \/  y  Btwn  <. x ,  z
>. )
5251, 35, 9crab 2758 . . . . . . 7  class  { z  e.  ( EE `  n )  |  ( z  Btwn  <. x ,  y >.  \/  x  Btwn  <. z ,  y
>.  \/  y  Btwn  <. x ,  z >. ) }
5313, 14, 9, 46, 52cmpt2 6280 . . . . . 6  class  ( 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
>. ) } )
5444, 53cop 3978 . . . . 5  class  <. (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
>. ) } ) >.
5542, 54cpr 3974 . . . 4  class  { <. (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 >. ) } ) >. }
5632, 55cun 3412 . . 3  class  ( {
<. ( 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
>. ) } ) >. } )
572, 3, 56cmpt 4453 . 2  class  ( 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
>. ) } ) >. } ) )
581, 57wceq 1405 1  wff 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
>. ) } ) >. } ) )
Colors of variables: wff setvar class
This definition is referenced by:  eengv  24699
  Copyright terms: Public domain W3C validator