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	$⊢ φ \to X \in Fin$
	rrxbasefi.h	$⊢ H = msup$
	rrxbasefi.b	$⊢ B = {Base}_{H}$
Assertion	rrxbasefi	$⊢ φ \to B = ℝ^{X}$

Proof

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

Metamath Proof Explorer

Theorem rrxbasefi

Proof