Metamath Proof Explorer

Definition df-eeng

Description: Define the geometry structure for EE ^ N . (Contributed by Thierry Arnoux, 24-Aug-2017)

Ref Expression
Assertion df-eeng ⊢ 𝔼 𝒢 = n ∈ ℕ ⟼ Base ndx 𝔼 ⁡ n dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2 ∪ Itv ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceeng class 𝔼 𝒢
1 vn setvar n
2 cn class ℕ
3 cbs class Base
4 cnx class ndx
5 4 3 cfv class Base ndx
6 cee class 𝔼
7 1 cv setvar n
8 7 6 cfv class 𝔼 ⁡ n
9 5 8 cop class Base ndx 𝔼 ⁡ n
10 cds class dist
11 4 10 cfv class dist ⁡ ndx
12 vx setvar x
13 vy setvar y
14 vi setvar i
15 c1 class 1
16 cfz class …
17 15 7 16 co class 1 … n
18 12 cv setvar x
19 14 cv setvar i
20 19 18 cfv class x ⁡ i
21 cmin class −
22 13 cv setvar y
23 19 22 cfv class y ⁡ i
24 20 23 21 co class x ⁡ i − y ⁡ i
25 cexp class ^
26 c2 class 2
27 24 26 25 co class x ⁡ i − y ⁡ i 2
28 17 27 14 csu class ∑ i = 1 n x ⁡ i − y ⁡ i 2
29 12 13 8 8 28 cmpo class x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2
30 11 29 cop class dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2
31 9 30 cpr class Base ndx 𝔼 ⁡ n dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2
32 citv class Itv
33 4 32 cfv class Itv ⁡ ndx
34 vz setvar z
35 34 cv setvar z
36 cbtwn class Btwn
37 18 22 cop class x y
38 35 37 36 wbr wff z Btwn x y
39 38 34 8 crab class z ∈ 𝔼 ⁡ n | z Btwn x y
40 12 13 8 8 39 cmpo class x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y
41 33 40 cop class Itv ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y
42 clng class Line 𝒢
43 4 42 cfv class Line 𝒢 ⁡ ndx
44 18 csn class x
45 8 44 cdif class 𝔼 ⁡ n ∖ x
46 35 22 cop class z y
47 18 46 36 wbr wff x Btwn z y
48 18 35 cop class x z
49 22 48 36 wbr wff y Btwn x z
50 38 47 49 w3o wff z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
51 50 34 8 crab class z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
52 12 13 8 45 51 cmpo class x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
53 43 52 cop class Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
54 41 53 cpr class Itv ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
55 31 54 cun class Base ndx 𝔼 ⁡ n dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2 ∪ Itv ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
56 1 2 55 cmpt class n ∈ ℕ ⟼ Base ndx 𝔼 ⁡ n dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2 ∪ Itv ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
57 0 56 wceq wff 𝔼 𝒢 = n ∈ ℕ ⟼ Base ndx 𝔼 ⁡ n dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2 ∪ Itv ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z