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	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
	rrxbase.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion	rrxbase	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } )

Proof

Step	Hyp	Ref	Expression
1		rrxval.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2		rrxbase.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
3	1	rrxval	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
4	3	fveq2d	⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝐻 ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
5		eqid	⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
6		eqid	⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
7	5 6	tcphbas	⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
8	4 7	eqtr4di	⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝐻 ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
9	2	a1i	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐻 ) )
10		refld	⊢ ℝfld ∈ Field
11		eqid	⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
12		rebase	⊢ ℝ = ( Base ‘ ℝfld )
13		re0g	⊢ 0 = ( 0g ‘ ℝfld )
14		eqid	⊢ { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 }
15	11 12 13 14	frlmbas	⊢ ( ( ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉 ) → { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
16	10 15	mpan	⊢ ( 𝐼 ∈ 𝑉 → { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
17	8 9 16	3eqtr4d	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∣ 𝑓 finSupp 0 } )