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

Metamath Proof Explorer

Theorem rrxbase

Description: The base of the generalized real Euclidean space is the set of functions with finite support. (Contributed by Thierry Arnoux, 16-Jun-2019) (Proof shortened by AV, 22-Jul-2019)

Ref Expression
Hypotheses rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion rrxbase ( 𝐼 ∈ 𝑉 → 𝐵 = { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } )

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
3 1 rrxval ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
4 3 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝐻 ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
5 eqid ⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
6 eqid ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
7 5 6 tcphbas ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
8 4 7 eqtr4di ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝐻 ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
9 2 a1i ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐻 ) )
10 refld ⊢ ℝfld ∈ Field
11 eqid ⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
12 rebase ⊢ ℝ = ( Base ‘ ℝfld )
13 re0g ⊢ 0 = ( 0g ‘ ℝfld )
14 eqid ⊢ { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 }
15 11 12 13 14 frlmbas ⊢ ( ( ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉 ) → { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
16 10 15 mpan ⊢ ( 𝐼 ∈ 𝑉 → { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
17 8 9 16 3eqtr4d ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } )