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 26692
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 26691 . 2 class EEG
2 vn . . 3 setvar 𝑛
3 cn 11627 . . 3 class
4 cnx 16470 . . . . . . 7 class ndx
5 cbs 16473 . . . . . . 7 class Base
64, 5cfv 6349 . . . . . 6 class (Base‘ndx)
72cv 1527 . . . . . . 7 class 𝑛
8 cee 26602 . . . . . . 7 class 𝔼
97, 8cfv 6349 . . . . . 6 class (𝔼‘𝑛)
106, 9cop 4565 . . . . 5 class ⟨(Base‘ndx), (𝔼‘𝑛)⟩
11 cds 16564 . . . . . . 7 class dist
124, 11cfv 6349 . . . . . 6 class (dist‘ndx)
13 vx . . . . . . 7 setvar 𝑥
14 vy . . . . . . 7 setvar 𝑦
15 c1 10527 . . . . . . . . 9 class 1
16 cfz 12882 . . . . . . . . 9 class ...
1715, 7, 16co 7145 . . . . . . . 8 class (1...𝑛)
18 vi . . . . . . . . . . . 12 setvar 𝑖
1918cv 1527 . . . . . . . . . . 11 class 𝑖
2013cv 1527 . . . . . . . . . . 11 class 𝑥
2119, 20cfv 6349 . . . . . . . . . 10 class (𝑥𝑖)
2214cv 1527 . . . . . . . . . . 11 class 𝑦
2319, 22cfv 6349 . . . . . . . . . 10 class (𝑦𝑖)
24 cmin 10859 . . . . . . . . . 10 class
2521, 23, 24co 7145 . . . . . . . . 9 class ((𝑥𝑖) − (𝑦𝑖))
26 c2 11681 . . . . . . . . 9 class 2
27 cexp 13419 . . . . . . . . 9 class
2825, 26, 27co 7145 . . . . . . . 8 class (((𝑥𝑖) − (𝑦𝑖))↑2)
2917, 28, 18csu 15032 . . . . . . 7 class Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2)
3013, 14, 9, 9, 29cmpo 7147 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))
3112, 30cop 4565 . . . . 5 class ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩
3210, 31cpr 4561 . . . 4 class {⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩}
33 citv 26150 . . . . . . 7 class Itv
344, 33cfv 6349 . . . . . 6 class (Itv‘ndx)
35 vz . . . . . . . . . 10 setvar 𝑧
3635cv 1527 . . . . . . . . 9 class 𝑧
3720, 22cop 4565 . . . . . . . . 9 class 𝑥, 𝑦
38 cbtwn 26603 . . . . . . . . 9 class Btwn
3936, 37, 38wbr 5058 . . . . . . . 8 wff 𝑧 Btwn ⟨𝑥, 𝑦
4039, 35, 9crab 3142 . . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩}
4113, 14, 9, 9, 40cmpo 7147 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})
4234, 41cop 4565 . . . . 5 class ⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩
43 clng 26151 . . . . . . 7 class LineG
444, 43cfv 6349 . . . . . 6 class (LineG‘ndx)
4520csn 4559 . . . . . . . 8 class {𝑥}
469, 45cdif 3932 . . . . . . 7 class ((𝔼‘𝑛) ∖ {𝑥})
4736, 22cop 4565 . . . . . . . . . 10 class 𝑧, 𝑦
4820, 47, 38wbr 5058 . . . . . . . . 9 wff 𝑥 Btwn ⟨𝑧, 𝑦
4920, 36cop 4565 . . . . . . . . . 10 class 𝑥, 𝑧
5022, 49, 38wbr 5058 . . . . . . . . 9 wff 𝑦 Btwn ⟨𝑥, 𝑧
5139, 48, 50w3o 1078 . . . . . . . 8 wff (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
5251, 35, 9crab 3142 . . . . . . 7 class {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)}
5313, 14, 9, 46, 52cmpo 7147 . . . . . 6 class (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})
5444, 53cop 4565 . . . . 5 class ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩
5542, 54cpr 4561 . . . 4 class {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}
5632, 55cun 3933 . . 3 class ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩})
572, 3, 56cmpt 5138 . 2 class (𝑛 ∈ ℕ ↦ ({⟨(Base‘ndx), (𝔼‘𝑛)⟩, ⟨(dist‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ Σ𝑖 ∈ (1...𝑛)(((𝑥𝑖) − (𝑦𝑖))↑2))⟩} ∪ {⟨(Itv‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ (𝔼‘𝑛) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ 𝑧 Btwn ⟨𝑥, 𝑦⟩})⟩, ⟨(LineG‘ndx), (𝑥 ∈ (𝔼‘𝑛), 𝑦 ∈ ((𝔼‘𝑛) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑛) ∣ (𝑧 Btwn ⟨𝑥, 𝑦⟩ ∨ 𝑥 Btwn ⟨𝑧, 𝑦⟩ ∨ 𝑦 Btwn ⟨𝑥, 𝑧⟩)})⟩}))
581, 57wceq 1528 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  26693
  Copyright terms: Public domain W3C validator