Definition df-eeng

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

	Ref	Expression
Assertion	df-eeng	⊢ EEG = ( 𝑛 ∈ ℕ ↦ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑛 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceeng	⊢ EEG
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3		cbs	⊢ Base
4		cnx	⊢ ndx
5	4 3	cfv	⊢ ( Base ‘ ndx )
6		cee	⊢ 𝔼
7	1	cv	⊢ 𝑛
8	7 6	cfv	⊢ ( 𝔼 ‘ 𝑛 )
9	5 8	cop	⊢ ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑛 ) ⟩
10		cds	⊢ dist
11	4 10	cfv	⊢ ( dist ‘ ndx )
12		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14		vi	⊢ 𝑖
15		c1	⊢ 1
16		cfz	⊢ ...
17	15 7 16	co	⊢ ( 1 ... 𝑛 )
18	12	cv	⊢ 𝑥
19	14	cv	⊢ 𝑖
20	19 18	cfv	⊢ ( 𝑥 ‘ 𝑖 )
21		cmin	⊢ −
22	13	cv	⊢ 𝑦
23	19 22	cfv	⊢ ( 𝑦 ‘ 𝑖 )
24	20 23 21	co	⊢ ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) )
25		cexp	⊢ ↑
26		c2	⊢ 2
27	24 26 25	co	⊢ ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 )
28	17 27 14	csu	⊢ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 )
29	12 13 8 8 28	cmpo	⊢ ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) )
30	11 29	cop	⊢ ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩
31	9 30	cpr	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑛 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ }
32		citv	⊢ Itv
33	4 32	cfv	⊢ ( Itv ‘ ndx )
34		vz	⊢ 𝑧
35	34	cv	⊢ 𝑧
36		cbtwn	⊢ Btwn
37	18 22	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
38	35 37 36	wbr	⊢ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩
39	38 34 8	crab	⊢ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ }
40	12 13 8 8 39	cmpo	⊢ ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } )
41	33 40	cop	⊢ ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩
42		clng	⊢ LineG
43	4 42	cfv	⊢ ( LineG ‘ ndx )
44	18	csn	⊢ { 𝑥 }
45	8 44	cdif	⊢ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } )
46	35 22	cop	⊢ ⟨ 𝑧 , 𝑦 ⟩
47	18 46 36	wbr	⊢ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩
48	18 35	cop	⊢ ⟨ 𝑥 , 𝑧 ⟩
49	22 48 36	wbr	⊢ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩
50	38 47 49	w3o	⊢ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ )
51	50 34 8	crab	⊢ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) }
52	12 13 8 45 51	cmpo	⊢ ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } )
53	43 52	cop	⊢ ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩
54	41 53	cpr	⊢ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ }
55	31 54	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑛 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } )
56	1 2 55	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑛 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
57	0 56	wceq	⊢ EEG = ( 𝑛 ∈ ℕ ↦ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑛 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )