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