This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ‘ 𝐻 ) = ( ♯ ‘ 𝐼 ) )