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 }