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

Definition df-eeng 26078
 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
StepHypRef Expression
1 ceeng 26077 . 2 class EEG
2 vn . . 3 setvar 𝑛
3 cn 11221 . . 3 class
4 cnx 16060 . . . . . . 7 class ndx
5 cbs 16063 . . . . . . 7 class Base
64, 5cfv 6031 . . . . . 6 class (Base‘ndx)
72cv 1629 . . . . . . 7 class 𝑛
8 cee 25988 . . . . . . 7 class 𝔼
97, 8cfv 6031 . . . . . 6 class (𝔼‘𝑛)
106, 9cop 4320 . . . . 5 class ⟨(Base‘ndx), (𝔼‘𝑛)⟩
11 cds 16157 . . . . . . 7 class dist
124, 11cfv 6031 . . . . . 6 class (dist‘ndx)
13 vx . . . . . . 7 setvar 𝑥
14 vy . . . . . . 7 setvar 𝑦
15 c1 10138 . . . . . . . . 9 class 1
16 cfz 12532 . . . . . . . . 9 class ...
1715, 7, 16co 6792 . . . . . . . 8 class (1...𝑛)
18 vi . . . . . . . . . . . 12 setvar 𝑖
1918cv 1629 . . . . . . . . . . 11 class 𝑖
2013cv 1629 . . . . . . . . . . 11 class 𝑥
2119, 20cfv 6031 . . . . . . . . . 10 class (𝑥𝑖)
2214cv 1629 . . . . . . . . . . 11 class 𝑦
2319, 22cfv 6031 . . . . . . . . . 10 class (𝑦𝑖)
24 cmin 10467 . . . . . . . . . 10 class
2521, 23, 24co 6792 . . . . . . . . 9 class ((𝑥𝑖) − (𝑦𝑖))
26 c2 11271 . . . . . . . . 9 class 2
27 cexp 13066 . . . . . . . . 9 class
2825, 26, 27co 6792 . . . . . . . 8 class (((𝑥𝑖) − (𝑦𝑖))↑2)
2917, 28, 18csu 14623 . . . . . . 7 class Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2)
3013, 14, 9, 9, 29cmpt2 6794 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))
3112, 30cop 4320 . . . . 5 class ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩
3210, 31cpr 4316 . . . 4 class {⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩}
33 citv 25555 . . . . . . 7 class Itv
344, 33cfv 6031 . . . . . 6 class (Itv‘ndx)
35 vz . . . . . . . . . 10 setvar 𝑧
3635cv 1629 . . . . . . . . 9 class 𝑧
3720, 22cop 4320 . . . . . . . . 9 class 𝑥, 𝑦
38 cbtwn 25989 . . . . . . . . 9 class Btwn
3936, 37, 38wbr 4784 . . . . . . . 8 wff 𝑧 Btwn ⟨𝑥, 𝑦
4039, 35, 9crab 3064 . . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩}
4113, 14, 9, 9, 40cmpt2 6794 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})
4234, 41cop 4320 . . . . 5 class ⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩
43 clng 25556 . . . . . . 7 class LineG
444, 43cfv 6031 . . . . . 6 class (LineG‘ndx)
4520csn 4314 . . . . . . . 8 class {𝑥}
469, 45cdif 3718 . . . . . . 7 class ((𝔼‘𝑛) ∖ {𝑥})
4736, 22cop 4320 . . . . . . . . . 10 class 𝑧, 𝑦
4820, 47, 38wbr 4784 . . . . . . . . 9 wff 𝑥 Btwn ⟨𝑧, 𝑦
4920, 36cop 4320 . . . . . . . . . 10 class 𝑥, 𝑧
5022, 49, 38wbr 4784 . . . . . . . . 9 wff 𝑦 Btwn ⟨𝑥, 𝑧
5139, 48, 50w3o 1069 . . . . . . . 8 wff (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
5251, 35, 9crab 3064 . . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)}
5313, 14, 9, 46, 52cmpt2 6794 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})
5444, 53cop 4320 . . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩
5542, 54cpr 4316 . . . 4 class {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}
5632, 55cun 3719 . . 3 class ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})
572, 3, 56cmpt 4861 . 2 class (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
581, 57wceq 1630 1 wff EEG = (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  eengv  26079
 Copyright terms: Public domain W3C validator