rrxdim

Description: Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023)

		Ref	Expression
	Hypothesis	rrxdim.1	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
	Assertion	rrxdim	⊢ ( 𝐼 ∈ 𝑉 → ( dim ‘ 𝐻 ) = ( ♯ ‘ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		rrxdim.1	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2	1	rrxval	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) )
3		eqid	⊢ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) )
4		eqid	⊢ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) )
5		eqid	⊢ ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) )
6	3 4 5	tcphval	⊢ ( toℂPreHil ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( ( ℝ_fld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) )
7	2 6	eqtrdi	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( ( ℝ_fld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) )
8	7	fveq2d	⊢ ( 𝐼 ∈ 𝑉 → ( dim ‘ 𝐻 ) = ( dim ‘ ( ( ℝ_fld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) ) )
9		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂ_fld ) ∧ ℝ_fld ∈ DivRing )
10	9	simpri	⊢ ℝ_fld ∈ DivRing
11		eqid	⊢ ( ℝ_fld freeLMod 𝐼 ) = ( ℝ_fld freeLMod 𝐼 )
12	11	frlmlvec	⊢ ( ( ℝ_fld ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( ℝ_fld freeLMod 𝐼 ) ∈ LVec )
13	10 12	mpan	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ_fld freeLMod 𝐼 ) ∈ LVec )
14	4	tcphex	⊢ ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) ∈ V
15		eqid	⊢ ( ( ℝ_fld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) = ( ( ℝ_fld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) )
16	15	tngdim	⊢ ( ( ( ℝ_fld freeLMod 𝐼 ) ∈ LVec ∧ ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) ∈ V ) → ( dim ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( dim ‘ ( ( ℝ_fld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) ) )
17	13 14 16	sylancl	⊢ ( 𝐼 ∈ 𝑉 → ( dim ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( dim ‘ ( ( ℝ_fld freeLMod 𝐼 ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ℝ_fld freeLMod 𝐼 ) ) ↦ ( √ ‘ ( 𝑥 ( ·_𝑖 ‘ ( ℝ_fld freeLMod 𝐼 ) ) 𝑥 ) ) ) ) ) )
18	11	frlmdim	⊢ ( ( ℝ_fld ∈ DivRing ∧ 𝐼 ∈ 𝑉 ) → ( dim ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
19	10 18	mpan	⊢ ( 𝐼 ∈ 𝑉 → ( dim ‘ ( ℝ_fld freeLMod 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
20	8 17 19	3eqtr2d	⊢ ( 𝐼 ∈ 𝑉 → ( dim ‘ 𝐻 ) = ( ♯ ‘ 𝐼 ) )

Metamath Proof Explorer

Theorem rrxdim

Proof