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 ⊢ H = I
rrxbase.b ⊢ B = Base H
Assertion rrxbase ⊢ I ∈ V → B = f ∈ ℝ I | finSupp 0 ⁡ f

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ H = I
2 rrxbase.b ⊢ B = Base H
3 1 rrxval ⊢ I ∈ V → H = toCPreHil ⁡ ℝ fld freeLMod I
4 3 fveq2d ⊢ I ∈ V → Base H = Base toCPreHil ⁡ ℝ fld freeLMod I
5 eqid ⊢ toCPreHil ⁡ ℝ fld freeLMod I = toCPreHil ⁡ ℝ fld freeLMod I
6 eqid ⊢ Base ℝ fld freeLMod I = Base ℝ fld freeLMod I
7 5 6 tcphbas ⊢ Base ℝ fld freeLMod I = Base toCPreHil ⁡ ℝ fld freeLMod I
8 4 7 eqtr4di ⊢ I ∈ V → Base H = Base ℝ fld freeLMod I
9 2 a1i ⊢ I ∈ V → B = Base H
10 refld ⊢ ℝ fld ∈ Field
11 eqid ⊢ ℝ fld freeLMod I = ℝ fld freeLMod I
12 rebase ⊢ ℝ = Base ℝ fld
13 re0g ⊢ 0 = 0 ℝ fld
14 eqid ⊢ f ∈ ℝ I | finSupp 0 ⁡ f = f ∈ ℝ I | finSupp 0 ⁡ f
15 11 12 13 14 frlmbas ⊢ ℝ fld ∈ Field ∧ I ∈ V → f ∈ ℝ I | finSupp 0 ⁡ f = Base ℝ fld freeLMod I
16 10 15 mpan ⊢ I ∈ V → f ∈ ℝ I | finSupp 0 ⁡ f = Base ℝ fld freeLMod I
17 8 9 16 3eqtr4d ⊢ I ∈ V → B = f ∈ ℝ I | finSupp 0 ⁡ f