Metamath Proof Explorer

Theorem eengv

Description: The value of the Euclidean geometry for dimension N . (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion eengv ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ 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

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ n = N → 𝔼 ⁡ n = 𝔼 ⁡ N
2 1 opeq2d ⊢ n = N → Base ndx 𝔼 ⁡ n = Base ndx 𝔼 ⁡ N
3 1 adantr ⊢ n = N ∧ x ∈ 𝔼 ⁡ n → 𝔼 ⁡ n = 𝔼 ⁡ N
4 simpl ⊢ n = N ∧ x ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n → n = N
5 4 oveq2d ⊢ n = N ∧ x ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n → 1 … n = 1 … N
6 5 sumeq1d ⊢ n = N ∧ x ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n → ∑ i = 1 n x ⁡ i − y ⁡ i 2 = ∑ i = 1 N x ⁡ i − y ⁡ i 2
7 1 3 6 mpoeq123dva ⊢ n = N → x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2 = x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ ∑ i = 1 N x ⁡ i − y ⁡ i 2
8 7 opeq2d ⊢ n = N → dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2 = dist ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ ∑ i = 1 N x ⁡ i − y ⁡ i 2
9 2 8 preq12d ⊢ n = N → Base ndx 𝔼 ⁡ n dist ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ ∑ i = 1 n x ⁡ i − y ⁡ i 2 = Base ndx 𝔼 ⁡ N dist ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ ∑ i = 1 N x ⁡ i − y ⁡ i 2
10 1 adantr ⊢ n = N ∧ x ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n → 𝔼 ⁡ n = 𝔼 ⁡ N
11 10 rabeqdv ⊢ n = N ∧ x ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n → z ∈ 𝔼 ⁡ n | z Btwn x y = z ∈ 𝔼 ⁡ N | z Btwn x y
12 1 3 11 mpoeq123dva ⊢ n = N → x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y = x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y
13 12 opeq2d ⊢ n = N → Itv ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y = Itv ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y
14 3 difeq1d ⊢ n = N ∧ x ∈ 𝔼 ⁡ n → 𝔼 ⁡ n ∖ x = 𝔼 ⁡ N ∖ x
15 1 rabeqdv ⊢ n = N → z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z = z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
16 15 adantr ⊢ n = N ∧ x ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n ∖ x → z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z = z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
17 1 14 16 mpoeq123dva ⊢ n = N → x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z = x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
18 17 opeq2d ⊢ n = N → Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ n , y ∈ 𝔼 ⁡ n ∖ x ⟼ z ∈ 𝔼 ⁡ n | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z = Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
19 13 18 preq12d ⊢ n = N → 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 = 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
20 9 19 uneq12d ⊢ n = 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 = 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
21 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
22 prex ⊢ Base ndx 𝔼 ⁡ N dist ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ ∑ i = 1 N x ⁡ i − y ⁡ i 2 ∈ V
23 prex ⊢ 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 ∈ V
24 22 23 unex ⊢ 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 ∈ V
25 20 21 24 fvmpt ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ 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