Definition df-eeng 29538

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 29537	. 2 class EEG
2		vn	. . 3 setvar 𝑛
3		cn 12316	. . 3 class ℕ
4		cnx 17351	. . . . . . 7 class ndx
5		cbs 17367	. . . . . . 7 class Base
6	4, 5	cfv 6531	. . . . . 6 class (Base‘ndx)
7	2	cv 1569	. . . . . . 7 class 𝑛
8		cee 29447	. . . . . . 7 class 𝔼
9	7, 8	cfv 6531	. . . . . 6 class (𝔼‘𝑛)
10	6, 9	cop 4590	. . . . 5 class ⟨(Base‘ndx), (𝔼‘𝑛)⟩
11		cds 17417	. . . . . . 7 class dist
12	4, 11	cfv 6531	. . . . . 6 class (dist‘ndx)
13		vx	. . . . . . 7 setvar 𝑥
14		vy	. . . . . . 7 setvar 𝑦
15		c1 11182	. . . . . . . . 9 class 1
16		cfz 13620	. . . . . . . . 9 class ...
17	15, 7, 16	co 7412	. . . . . . . 8 class (1...𝑛)
18		vi	. . . . . . . . . . . 12 setvar 𝑖
19	18	cv 1569	. . . . . . . . . . 11 class 𝑖
20	13	cv 1569	. . . . . . . . . . 11 class 𝑥
21	19, 20	cfv 6531	. . . . . . . . . 10 class (𝑥‘𝑖)
22	14	cv 1569	. . . . . . . . . . 11 class 𝑦
23	19, 22	cfv 6531	. . . . . . . . . 10 class (𝑦‘𝑖)
24		cmin 11522	. . . . . . . . . 10 class −
25	21, 23, 24	co 7412	. . . . . . . . 9 class ((𝑥‘𝑖) − (𝑦‘𝑖))
26		c2 12378	. . . . . . . . 9 class 2
27		cexp 14184	. . . . . . . . 9 class ↑
28	25, 26, 27	co 7412	. . . . . . . 8 class (((𝑥‘𝑖) − (𝑦‘𝑖))↑2)
29	17, 28, 18	csu 15833	. . . . . . 7 class Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)
30	13, 14, 9, 9, 29	cmpo 7414	. . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))
31	12, 30	cop 4590	. . . . 5 class ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩
32	10, 31	cpr 4586	. . . 4 class {⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩}
33		citv 28877	. . . . . . 7 class Itv
34	4, 33	cfv 6531	. . . . . 6 class (Itv‘ndx)
35		vz	. . . . . . . . . 10 setvar 𝑧
36	35	cv 1569	. . . . . . . . 9 class 𝑧
37	20, 22	cop 4590	. . . . . . . . 9 class ⟨𝑥, 𝑦⟩
38		cbtwn 29448	. . . . . . . . 9 class Btwn
39	36, 37, 38	wbr 5103	. . . . . . . 8 wff 𝑧 Btwn ⟨𝑥, 𝑦⟩
40	39, 35, 9	crab 3413	. . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩}
41	13, 14, 9, 9, 40	cmpo 7414	. . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})
42	34, 41	cop 4590	. . . . 5 class ⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩
43		clng 28878	. . . . . . 7 class LineG
44	4, 43	cfv 6531	. . . . . 6 class (LineG‘ndx)
45	20	csn 4584	. . . . . . . 8 class {𝑥}
46	9, 45	cdif 3896	. . . . . . 7 class ((𝔼‘𝑛) ∖ {𝑥})
47	36, 22	cop 4590	. . . . . . . . . 10 class ⟨𝑧, 𝑦⟩
48	20, 47, 38	wbr 5103	. . . . . . . . 9 wff 𝑥 Btwn ⟨𝑧, 𝑦⟩
49	20, 36	cop 4590	. . . . . . . . . 10 class ⟨𝑥, 𝑧⟩
50	22, 49, 38	wbr 5103	. . . . . . . . 9 wff 𝑦 Btwn ⟨𝑥, 𝑧⟩
51	39, 48, 50	w3o 1102	. . . . . . . 8 wff (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
52	51, 35, 9	crab 3413	. . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)}
53	13, 14, 9, 46, 52	cmpo 7414	. . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})
54	44, 53	cop 4590	. . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩
55	42, 54	cpr 4586	. . . 4 class {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}
56	32, 55	cun 3897	. . 3 class ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})
57	2, 3, 56	cmpt 5186	. 2 class (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
58	1, 57	wceq 1570	1 wff EEG = (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))

This definition is used by:  eengv  29539