Definition df-eeng 25858

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

Step	Hyp	Ref	Expression
1		ceeng 25857	. 2 class EEG
2		vn	. . 3 setvar n
3		cn 11020	. . 3 class NN
4		cnx 15854	. . . . . . 7 class ndx
5		cbs 15857	. . . . . . 7 class Base
6	4, 5	cfv 5888	. . . . . 6 class ( Base ` ndx )
7	2	cv 1482	. . . . . . 7 class n
8		cee 25768	. . . . . . 7 class EE
9	7, 8	cfv 5888	. . . . . 6 class ( EE ` n )
10	6, 9	cop 4183	. . . . 5 class <. ( Base ` ndx ) , ( EE ` n ) >.
11		cds 15950	. . . . . . 7 class dist
12	4, 11	cfv 5888	. . . . . 6 class ( dist ` ndx )
13		vx	. . . . . . 7 setvar x
14		vy	. . . . . . 7 setvar y
15		c1 9937	. . . . . . . . 9 class 1
16		cfz 12326	. . . . . . . . 9 class ...
17	15, 7, 16	co 6650	. . . . . . . 8 class ( 1 ... n )
18		vi	. . . . . . . . . . . 12 setvar i
19	18	cv 1482	. . . . . . . . . . 11 class i
20	13	cv 1482	. . . . . . . . . . 11 class x
21	19, 20	cfv 5888	. . . . . . . . . 10 class ( x ` i )
22	14	cv 1482	. . . . . . . . . . 11 class y
23	19, 22	cfv 5888	. . . . . . . . . 10 class ( y ` i )
24		cmin 10266	. . . . . . . . . 10 class -
25	21, 23, 24	co 6650	. . . . . . . . 9 class ( ( x ` i ) - ( y ` i ) )
26		c2 11070	. . . . . . . . 9 class 2
27		cexp 12860	. . . . . . . . 9 class ^
28	25, 26, 27	co 6650	. . . . . . . 8 class ( ( ( x ` i ) - ( y ` i ) ) ^ 2 )
29	17, 28, 18	csu 14416	. . . . . . 7 class sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 )
30	13, 14, 9, 9, 29	cmpt2 6652	. . . . . 6 class ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) )
31	12, 30	cop 4183	. . . . 5 class <. ( dist ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> sum_ i e. ( 1 ... n ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >.
32	10, 31	cpr 4179	. . . 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 25335	. . . . . . 7 class Itv
34	4, 33	cfv 5888	. . . . . 6 class (Itv ` ndx )
35		vz	. . . . . . . . . 10 setvar z
36	35	cv 1482	. . . . . . . . 9 class z
37	20, 22	cop 4183	. . . . . . . . 9 class <. x , y >.
38		cbtwn 25769	. . . . . . . . 9 class Btwn
39	36, 37, 38	wbr 4653	. . . . . . . 8 wff z Btwn <. x , y >.
40	39, 35, 9	crab 2916	. . . . . . 7 class { z e. ( EE ` n ) | z Btwn <. x , y >. }
41	13, 14, 9, 9, 40	cmpt2 6652	. . . . . 6 class ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } )
42	34, 41	cop 4183	. . . . 5 class <. (Itv ` ndx ) , ( x e. ( EE ` n ) , y e. ( EE ` n ) |-> { z e. ( EE ` n ) | z Btwn <. x , y >. } ) >.
43		clng 25336	. . . . . . 7 class LineG
44	4, 43	cfv 5888	. . . . . 6 class (LineG ` ndx )
45	20	csn 4177	. . . . . . . 8 class { x }
46	9, 45	cdif 3571	. . . . . . 7 class ( ( EE ` n ) \ { x } )
47	36, 22	cop 4183	. . . . . . . . . 10 class <. z , y >.
48	20, 47, 38	wbr 4653	. . . . . . . . 9 wff x Btwn <. z , y >.
49	20, 36	cop 4183	. . . . . . . . . 10 class <. x , z >.
50	22, 49, 38	wbr 4653	. . . . . . . . 9 wff y Btwn <. x , z >.
51	39, 48, 50	w3o 1036	. . . . . . . 8 wff ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. )
52	51, 35, 9	crab 2916	. . . . . . 7 class { z e. ( EE ` n ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) }
53	13, 14, 9, 46, 52	cmpt2 6652	. . . . . 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 >. ) } )
54	44, 53	cop 4183	. . . . 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 >. ) } ) >.
55	42, 54	cpr 4179	. . . 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 >. ) } ) >. }
56	32, 55	cun 3572	. . 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 >. ) } ) >. } )
57	2, 3, 56	cmpt 4729	. 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 >. ) } ) >. } ) )
58	1, 57	wceq 1483	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 >. ) } ) >. } ) )

This definition is referenced by:  eengv  25859