Step |
Hyp |
Ref |
Expression |
1 |
|
eengstr |
⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct 〈 1 , ; 1 7 〉 ) |
2 |
|
fvexd |
⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) ∈ V ) |
3 |
|
opex |
⊢ 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 ∈ V |
4 |
3
|
prid1 |
⊢ 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 ∈ { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } |
5 |
|
elun1 |
⊢ ( 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 ∈ { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } → 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 ∈ ( { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } ∪ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } ) ) |
6 |
4 5
|
ax-mp |
⊢ 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 ∈ ( { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } ∪ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } ) |
7 |
|
eengv |
⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) = ( { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } ∪ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } ) ) |
8 |
6 7
|
eleqtrrid |
⊢ ( 𝑁 ∈ ℕ → 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 ∈ ( EEG ‘ 𝑁 ) ) |
9 |
1 2 8
|
opelstrbas |
⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) ) |