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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	rrxbasefi.h	⊢ 𝐻 = ( ℝ^ ‘ 𝑋 )
	rrxbasefi.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion	rrxbasefi	⊢ ( 𝜑 → 𝐵 = ( ℝ ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		rrxbasefi.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		rrxbasefi.h	⊢ 𝐻 = ( ℝ^ ‘ 𝑋 )
3		rrxbasefi.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
4	2 3	rrxbase	⊢ ( 𝑋 ∈ Fin → 𝐵 = { 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∣ 𝑓 finSupp 0 } )
5	1 4	syl	⊢ ( 𝜑 → 𝐵 = { 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∣ 𝑓 finSupp 0 } )
6		ssrab2	⊢ { 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∣ 𝑓 finSupp 0 } ⊆ ( ℝ ↑m 𝑋 )
7	5 6	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 ∈ ( ℝ ↑m 𝑋 ) )
9		elmapi	⊢ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) → 𝑓 : 𝑋 ⟶ ℝ )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 : 𝑋 ⟶ ℝ )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑋 ∈ Fin )
12		c0ex	⊢ 0 ∈ V
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 0 ∈ V )
14	10 11 13	fdmfifsupp	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 finSupp 0 )
15		rabid	⊢ ( 𝑓 ∈ { 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∣ 𝑓 finSupp 0 } ↔ ( 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑓 finSupp 0 ) )
16	8 14 15	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 ∈ { 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∣ 𝑓 finSupp 0 } )
17	5	eqcomd	⊢ ( 𝜑 → { 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∣ 𝑓 finSupp 0 } = 𝐵 )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → { 𝑓 ∈ ( ℝ ↑m 𝑋 ) ∣ 𝑓 finSupp 0 } = 𝐵 )
19	16 18	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) → 𝑓 ∈ 𝐵 )
20	7 19	eqelssd	⊢ ( 𝜑 → 𝐵 = ( ℝ ↑m 𝑋 ) )