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

Definition df-eeng 25839
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 25838 . 2 class EEG
2 vn . . 3 setvar 𝑛
3 cn 11005 . . 3 class
4 cnx 15835 . . . . . . 7 class ndx
5 cbs 15838 . . . . . . 7 class Base
64, 5cfv 5876 . . . . . 6 class (Base‘ndx)
72cv 1480 . . . . . . 7 class 𝑛
8 cee 25749 . . . . . . 7 class 𝔼
97, 8cfv 5876 . . . . . 6 class (𝔼‘𝑛)
106, 9cop 4174 . . . . 5 class ⟨(Base‘ndx), (𝔼‘𝑛)⟩
11 cds 15931 . . . . . . 7 class dist
124, 11cfv 5876 . . . . . 6 class (dist‘ndx)
13 vx . . . . . . 7 setvar 𝑥
14 vy . . . . . . 7 setvar 𝑦
15 c1 9922 . . . . . . . . 9 class 1
16 cfz 12311 . . . . . . . . 9 class ...
1715, 7, 16co 6635 . . . . . . . 8 class (1...𝑛)
18 vi . . . . . . . . . . . 12 setvar 𝑖
1918cv 1480 . . . . . . . . . . 11 class 𝑖
2013cv 1480 . . . . . . . . . . 11 class 𝑥
2119, 20cfv 5876 . . . . . . . . . 10 class (𝑥𝑖)
2214cv 1480 . . . . . . . . . . 11 class 𝑦
2319, 22cfv 5876 . . . . . . . . . 10 class (𝑦𝑖)
24 cmin 10251 . . . . . . . . . 10 class
2521, 23, 24co 6635 . . . . . . . . 9 class ((𝑥𝑖) − (𝑦𝑖))
26 c2 11055 . . . . . . . . 9 class 2
27 cexp 12843 . . . . . . . . 9 class
2825, 26, 27co 6635 . . . . . . . 8 class (((𝑥𝑖) − (𝑦𝑖))↑2)
2917, 28, 18csu 14397 . . . . . . 7 class Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2)
3013, 14, 9, 9, 29cmpt2 6637 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))
3112, 30cop 4174 . . . . 5 class ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩
3210, 31cpr 4170 . . . 4 class {⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩}
33 citv 25316 . . . . . . 7 class Itv
344, 33cfv 5876 . . . . . 6 class (Itv‘ndx)
35 vz . . . . . . . . . 10 setvar 𝑧
3635cv 1480 . . . . . . . . 9 class 𝑧
3720, 22cop 4174 . . . . . . . . 9 class 𝑥, 𝑦
38 cbtwn 25750 . . . . . . . . 9 class Btwn
3936, 37, 38wbr 4644 . . . . . . . 8 wff 𝑧 Btwn ⟨𝑥, 𝑦
4039, 35, 9crab 2913 . . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩}
4113, 14, 9, 9, 40cmpt2 6637 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})
4234, 41cop 4174 . . . . 5 class ⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩
43 clng 25317 . . . . . . 7 class LineG
444, 43cfv 5876 . . . . . 6 class (LineG‘ndx)
4520csn 4168 . . . . . . . 8 class {𝑥}
469, 45cdif 3564 . . . . . . 7 class ((𝔼‘𝑛) ∖ {𝑥})
4736, 22cop 4174 . . . . . . . . . 10 class 𝑧, 𝑦
4820, 47, 38wbr 4644 . . . . . . . . 9 wff 𝑥 Btwn ⟨𝑧, 𝑦
4920, 36cop 4174 . . . . . . . . . 10 class 𝑥, 𝑧
5022, 49, 38wbr 4644 . . . . . . . . 9 wff 𝑦 Btwn ⟨𝑥, 𝑧
5139, 48, 50w3o 1035 . . . . . . . 8 wff (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
5251, 35, 9crab 2913 . . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)}
5313, 14, 9, 46, 52cmpt2 6637 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})
5444, 53cop 4174 . . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩
5542, 54cpr 4170 . . . 4 class {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}
5632, 55cun 3565 . . 3 class ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})
572, 3, 56cmpt 4720 . 2 class (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
581, 57wceq 1481 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  25840
  Copyright terms: Public domain W3C validator