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	|- ( ph -> X e. Fin )
	rrxbasefi.h	|- H = ( RR^ ` X )
	rrxbasefi.b	|- B = ( Base ` H )
Assertion	rrxbasefi	|- ( ph -> B = ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		rrxbasefi.x	|- ( ph -> X e. Fin )
2		rrxbasefi.h	|- H = ( RR^ ` X )
3		rrxbasefi.b	|- B = ( Base ` H )
4	2 3	rrxbase	|- ( X e. Fin -> B = { f e. ( RR ^m X ) | f finSupp 0 } )
5	1 4	syl	|- ( ph -> B = { f e. ( RR ^m X ) | f finSupp 0 } )
6		ssrab2	|- { f e. ( RR ^m X ) | f finSupp 0 } C_ ( RR ^m X )
7	5 6	eqsstrdi	|- ( ph -> B C_ ( RR ^m X ) )
8		simpr	|- ( ( ph /\ f e. ( RR ^m X ) ) -> f e. ( RR ^m X ) )
9		elmapi	|- ( f e. ( RR ^m X ) -> f : X --> RR )
10	9	adantl	|- ( ( ph /\ f e. ( RR ^m X ) ) -> f : X --> RR )
11	1	adantr	|- ( ( ph /\ f e. ( RR ^m X ) ) -> X e. Fin )
12		c0ex	|- 0 e. _V
13	12	a1i	|- ( ( ph /\ f e. ( RR ^m X ) ) -> 0 e. _V )
14	10 11 13	fdmfifsupp	|- ( ( ph /\ f e. ( RR ^m X ) ) -> f finSupp 0 )
15		rabid	|- ( f e. { f e. ( RR ^m X ) | f finSupp 0 } <-> ( f e. ( RR ^m X ) /\ f finSupp 0 ) )
16	8 14 15	sylanbrc	|- ( ( ph /\ f e. ( RR ^m X ) ) -> f e. { f e. ( RR ^m X ) | f finSupp 0 } )
17	5	eqcomd	|- ( ph -> { f e. ( RR ^m X ) | f finSupp 0 } = B )
18	17	adantr	|- ( ( ph /\ f e. ( RR ^m X ) ) -> { f e. ( RR ^m X ) | f finSupp 0 } = B )
19	16 18	eleqtrd	|- ( ( ph /\ f e. ( RR ^m X ) ) -> f e. B )
20	7 19	eqelssd	|- ( ph -> B = ( RR ^m X ) )