# Metamath Proof Explorer

## Theorem rrxbasefi

Description: The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of ( RR ^m X ) for the development of the Lebesgue measure theory for n-dimensional real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses rrxbasefi.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
rrxbasefi.h ${⊢}{H}={{X}}^{}$
rrxbasefi.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
Assertion rrxbasefi ${⊢}{\phi }\to {B}={ℝ}^{{X}}$

### Proof

Step Hyp Ref Expression
1 rrxbasefi.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
2 rrxbasefi.h ${⊢}{H}={{X}}^{}$
3 rrxbasefi.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
4 2 3 rrxbase ${⊢}{X}\in \mathrm{Fin}\to {B}=\left\{{f}\in \left({ℝ}^{{X}}\right)|{finSupp}_{0}\left({f}\right)\right\}$
5 1 4 syl ${⊢}{\phi }\to {B}=\left\{{f}\in \left({ℝ}^{{X}}\right)|{finSupp}_{0}\left({f}\right)\right\}$
6 ssrab2 ${⊢}\left\{{f}\in \left({ℝ}^{{X}}\right)|{finSupp}_{0}\left({f}\right)\right\}\subseteq {ℝ}^{{X}}$
7 5 6 eqsstrdi ${⊢}{\phi }\to {B}\subseteq {ℝ}^{{X}}$
8 simpr ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}\in \left({ℝ}^{{X}}\right)$
9 elmapi ${⊢}{f}\in \left({ℝ}^{{X}}\right)\to {f}:{X}⟶ℝ$
10 9 adantl ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}:{X}⟶ℝ$
11 1 adantr ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {X}\in \mathrm{Fin}$
12 c0ex ${⊢}0\in \mathrm{V}$
13 12 a1i ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to 0\in \mathrm{V}$
14 10 11 13 fdmfifsupp ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {finSupp}_{0}\left({f}\right)$
15 rabid ${⊢}{f}\in \left\{{f}\in \left({ℝ}^{{X}}\right)|{finSupp}_{0}\left({f}\right)\right\}↔\left({f}\in \left({ℝ}^{{X}}\right)\wedge {finSupp}_{0}\left({f}\right)\right)$
16 8 14 15 sylanbrc ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}\in \left\{{f}\in \left({ℝ}^{{X}}\right)|{finSupp}_{0}\left({f}\right)\right\}$
17 5 eqcomd ${⊢}{\phi }\to \left\{{f}\in \left({ℝ}^{{X}}\right)|{finSupp}_{0}\left({f}\right)\right\}={B}$
18 17 adantr ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to \left\{{f}\in \left({ℝ}^{{X}}\right)|{finSupp}_{0}\left({f}\right)\right\}={B}$
19 16 18 eleqtrd ${⊢}\left({\phi }\wedge {f}\in \left({ℝ}^{{X}}\right)\right)\to {f}\in {B}$
20 7 19 eqelssd ${⊢}{\phi }\to {B}={ℝ}^{{X}}$