Definition df-eeng 27249

Description: Define the geometry structure for 𝔼↑𝑁. (Contributed by Thierry Arnoux, 24-Aug-2017.)

Assertion

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

Distinct variable group:   𝑖,𝑛,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-eeng

Step	Hyp	Ref	Expression
1		ceeng 27248	. 2 class EEG
2		vn	. . 3 setvar 𝑛
3		cn 11903	. . 3 class ℕ
4		cnx 16822	. . . . . . 7 class ndx
5		cbs 16840	. . . . . . 7 class Base
6	4, 5	cfv 6418	. . . . . 6 class (Base‘ndx)
7	2	cv 1538	. . . . . . 7 class 𝑛
8		cee 27159	. . . . . . 7 class 𝔼
9	7, 8	cfv 6418	. . . . . 6 class (𝔼‘𝑛)
10	6, 9	cop 4564	. . . . 5 class ⟨(Base‘ndx), (𝔼‘𝑛)⟩
11		cds 16897	. . . . . . 7 class dist
12	4, 11	cfv 6418	. . . . . 6 class (dist‘ndx)
13		vx	. . . . . . 7 setvar 𝑥
14		vy	. . . . . . 7 setvar 𝑦
15		c1 10803	. . . . . . . . 9 class 1
16		cfz 13168	. . . . . . . . 9 class ...
17	15, 7, 16	co 7255	. . . . . . . 8 class (1...𝑛)
18		vi	. . . . . . . . . . . 12 setvar 𝑖
19	18	cv 1538	. . . . . . . . . . 11 class 𝑖
20	13	cv 1538	. . . . . . . . . . 11 class 𝑥
21	19, 20	cfv 6418	. . . . . . . . . 10 class (𝑥‘𝑖)
22	14	cv 1538	. . . . . . . . . . 11 class 𝑦
23	19, 22	cfv 6418	. . . . . . . . . 10 class (𝑦‘𝑖)
24		cmin 11135	. . . . . . . . . 10 class −
25	21, 23, 24	co 7255	. . . . . . . . 9 class ((𝑥‘𝑖) − (𝑦‘𝑖))
26		c2 11958	. . . . . . . . 9 class 2
27		cexp 13710	. . . . . . . . 9 class ↑
28	25, 26, 27	co 7255	. . . . . . . 8 class (((𝑥‘𝑖) − (𝑦‘𝑖))↑2)
29	17, 28, 18	csu 15325	. . . . . . 7 class Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)
30	13, 14, 9, 9, 29	cmpo 7257	. . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))
31	12, 30	cop 4564	. . . . 5 class ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩
32	10, 31	cpr 4560	. . . 4 class {⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩}
33		citv 26699	. . . . . . 7 class Itv
34	4, 33	cfv 6418	. . . . . 6 class (Itv‘ndx)
35		vz	. . . . . . . . . 10 setvar 𝑧
36	35	cv 1538	. . . . . . . . 9 class 𝑧
37	20, 22	cop 4564	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
38		cbtwn 27160	. . . . . . . . 9 class Btwn
39	36, 37, 38	wbr 5070	. . . . . . . 8 wff 𝑧 Btwn ⟨𝑥, 𝑦⟩
40	39, 35, 9	crab 3067	. . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩}
41	13, 14, 9, 9, 40	cmpo 7257	. . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})
42	34, 41	cop 4564	. . . . 5 class ⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩
43		clng 26700	. . . . . . 7 class LineG
44	4, 43	cfv 6418	. . . . . 6 class (LineG‘ndx)
45	20	csn 4558	. . . . . . . 8 class {𝑥}
46	9, 45	cdif 3880	. . . . . . 7 class ((𝔼‘𝑛) ∖ {𝑥})
47	36, 22	cop 4564	. . . . . . . . . 10 class ⟨𝑧, 𝑦⟩
48	20, 47, 38	wbr 5070	. . . . . . . . 9 wff 𝑥 Btwn ⟨𝑧, 𝑦⟩
49	20, 36	cop 4564	. . . . . . . . . 10 class ⟨𝑥, 𝑧⟩
50	22, 49, 38	wbr 5070	. . . . . . . . 9 wff 𝑦 Btwn ⟨𝑥, 𝑧⟩
51	39, 48, 50	w3o 1084	. . . . . . . 8 wff (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
52	51, 35, 9	crab 3067	. . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)}
53	13, 14, 9, 46, 52	cmpo 7257	. . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})
54	44, 53	cop 4564	. . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩
55	42, 54	cpr 4560	. . . 4 class {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}
56	32, 55	cun 3881	. . 3 class ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})
57	2, 3, 56	cmpt 5153	. 2 class (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
58	1, 57	wceq 1539	1 wff EEG = (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))

This definition is referenced by:  eengv  27250