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

Metamath Proof Explorer

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 ‘ 𝐸 ) )