This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ehl0

Description: The Euclidean space of dimension 0 consists of the neutral element only. (Contributed by AV, 12-Feb-2023)

Ref Expression
Hypotheses ehl0base.e ⊢ 𝐸 = ( 𝔼hil ‘ 0 )
ehl0base.0 ⊢ 0 = ( 0g ‘ 𝐸 )
Assertion ehl0 ( Base ‘ 𝐸 ) = { 0 }

Proof

Step Hyp Ref Expression
1 ehl0base.e ⊢ 𝐸 = ( 𝔼hil ‘ 0 )
2 ehl0base.0 ⊢ 0 = ( 0g ‘ 𝐸 )
3 1 ehl0base ⊢ ( Base ‘ 𝐸 ) = { ∅ }
4 ovex ⊢ ( 1 ... 0 ) ∈ V
5 0nn0 ⊢ 0 ∈ ℕ0
6 1 ehlval ⊢ ( 0 ∈ ℕ0 → 𝐸 = ( ℝ^ ‘ ( 1 ... 0 ) ) )
7 5 6 ax-mp ⊢ 𝐸 = ( ℝ^ ‘ ( 1 ... 0 ) )
8 fz10 ⊢ ( 1 ... 0 ) = ∅
9 8 xpeq1i ⊢ ( ( 1 ... 0 ) × { 0 } ) = ( ∅ × { 0 } )
10 9 eqcomi ⊢ ( ∅ × { 0 } ) = ( ( 1 ... 0 ) × { 0 } )
11 7 10 rrx0 ⊢ ( ( 1 ... 0 ) ∈ V → ( 0g ‘ 𝐸 ) = ( ∅ × { 0 } ) )
12 4 11 ax-mp ⊢ ( 0g ‘ 𝐸 ) = ( ∅ × { 0 } )
13 2 12 eqtri ⊢ 0 = ( ∅ × { 0 } )
14 0xp ⊢ ( ∅ × { 0 } ) = ∅
15 13 14 eqtri ⊢ 0 = ∅
16 15 eqcomi ⊢ ∅ = 0
17 16 sneqi ⊢ { ∅ } = { 0 }
18 3 17 eqtri ⊢ ( Base ‘ 𝐸 ) = { 0 }