Metamath Proof Explorer

Theorem rrxprds

Description: Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion rrxprds ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
3 1 rrxval ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
4 refld ⊢ ℝfld ∈ Field
5 eqid ⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
6 eqid ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
7 5 6 frlmpws ⊢ ( ( ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld freeLMod 𝐼 ) = ( ( ( ringLMod ‘ ℝfld ) ↑s 𝐼 ) ↾s ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
8 4 7 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( ℝfld freeLMod 𝐼 ) = ( ( ( ringLMod ‘ ℝfld ) ↑s 𝐼 ) ↾s ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
9 fvex ⊢ ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) ∈ V
10 rlmval ⊢ ( ringLMod ‘ ℝfld ) = ( ( subringAlg ‘ ℝfld ) ‘ ( Base ‘ ℝfld ) )
11 rebase ⊢ ℝ = ( Base ‘ ℝfld )
12 11 fveq2i ⊢ ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℝfld ) ‘ ( Base ‘ ℝfld ) )
13 10 12 eqtr4i ⊢ ( ringLMod ‘ ℝfld ) = ( ( subringAlg ‘ ℝfld ) ‘ ℝ )
14 13 oveq1i ⊢ ( ( ringLMod ‘ ℝfld ) ↑s 𝐼 ) = ( ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) ↑s 𝐼 )
15 11 ressid ⊢ ( ℝfld ∈ Field → ( ℝfld ↾s ℝ ) = ℝfld )
16 4 15 ax-mp ⊢ ( ℝfld ↾s ℝ ) = ℝfld
17 eqidd ⊢ ( ⊤ → ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) )
18 11 eqimssi ⊢ ℝ ⊆ ( Base ‘ ℝfld )
19 18 a1i ⊢ ( ⊤ → ℝ ⊆ ( Base ‘ ℝfld ) )
20 17 19 srasca ⊢ ( ⊤ → ( ℝfld ↾s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) ) )
21 20 mptru ⊢ ( ℝfld ↾s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) )
22 16 21 eqtr3i ⊢ ℝfld = ( Scalar ‘ ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) )
23 14 22 pwsval ⊢ ( ( ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( ( ringLMod ‘ ℝfld ) ↑s 𝐼 ) = ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) )
24 9 23 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( ( ringLMod ‘ ℝfld ) ↑s 𝐼 ) = ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) )
25 24 eqcomd ⊢ ( 𝐼 ∈ 𝑉 → ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) = ( ( ringLMod ‘ ℝfld ) ↑s 𝐼 ) )
26 3 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝐻 ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
27 eqid ⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
28 27 6 tcphbas ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
29 26 2 28 3eqtr4g ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
30 25 29 oveq12d ⊢ ( 𝐼 ∈ 𝑉 → ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) = ( ( ( ringLMod ‘ ℝfld ) ↑s 𝐼 ) ↾s ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
31 8 30 eqtr4d ⊢ ( 𝐼 ∈ 𝑉 → ( ℝfld freeLMod 𝐼 ) = ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) )
32 31 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) )
33 3 32 eqtrd ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s 𝐵 ) ) )