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 ( 0 ..^ 𝑁 ) ) = ( Base ‘ 𝐸 ) )

Proof

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