Theorem ehlbase

Description: The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypothesis	ehlval.e	⊢ 𝐸 = ( 𝔼hil ‘ 𝑁 )
Assertion	ehlbase	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 1 ... 𝑁 ) ) = ( Base ‘ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		ehlval.e	⊢ 𝐸 = ( 𝔼hil ‘ 𝑁 )
2		rabid2	⊢ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) = { 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ 𝑓 finSupp 0 } ↔ ∀ 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) 𝑓 finSupp 0 )
3		elmapi	⊢ ( 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑓 : ( 1 ... 𝑁 ) ⟶ ℝ )
4		fzfid	⊢ ( 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
5		0red	⊢ ( 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 0 ∈ ℝ )
6	3 4 5	fdmfifsupp	⊢ ( 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑓 finSupp 0 )
7	2 6	mprgbir	⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) = { 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ 𝑓 finSupp 0 }
8		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
9		eqid	⊢ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) = ( ℝ^ ‘ ( 1 ... 𝑁 ) )
10		eqid	⊢ ( Base ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = ( Base ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
11	9 10	rrxbase	⊢ ( ( 1 ... 𝑁 ) ∈ V → ( Base ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = { 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ 𝑓 finSupp 0 } )
12	8 11	ax-mp	⊢ ( Base ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) = { 𝑓 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∣ 𝑓 finSupp 0 }
13	7 12	eqtr4i	⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) = ( Base ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
14	1	ehlval	⊢ ( 𝑁 ∈ ℕ0 → 𝐸 = ( ℝ^ ‘ ( 1 ... 𝑁 ) ) )
15	14	fveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( Base ‘ 𝐸 ) = ( Base ‘ ( ℝ^ ‘ ( 1 ... 𝑁 ) ) ) )
16	13 15	eqtr4id	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 1 ... 𝑁 ) ) = ( Base ‘ 𝐸 ) )