| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rrxsca.r | . . . 4
⊢ 𝐻 = (ℝ^‘𝐼) | 
| 2 |  | eqid 2737 | . . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 3 | 1, 2 | rrxprds 25423 | . . 3
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)))) | 
| 4 | 3 | fveq2d 6910 | . 2
⊢ (𝐼 ∈ 𝑉 → (Scalar‘𝐻) =
(Scalar‘(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))))) | 
| 5 |  | fvex 6919 | . . . . 5
⊢
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ∈
V | 
| 6 | 5 | mptex 7243 | . . . 4
⊢ (𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥))) ∈ V | 
| 7 |  | eqid 2737 | . . . . . 6
⊢
(((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)) toNrmGrp
(𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥)))) = (((ℝfldXs(𝐼 ×
{((subringAlg ‘ℝfld)‘ℝ)})) ↾s (Base‘𝐻)) toNrmGrp (𝑥 ∈ (Base‘((ℝfldXs(𝐼 ×
{((subringAlg ‘ℝfld)‘ℝ)})) ↾s (Base‘𝐻))) ↦ (√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥)))) | 
| 8 |  | eqid 2737 | . . . . . 6
⊢
(Scalar‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) =
(Scalar‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) | 
| 9 | 7, 8 | tngsca 24662 | . . . . 5
⊢ ((𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥))) ∈ V →
(Scalar‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s (Base‘𝐻))) = (Scalar‘(((ℝfldXs(𝐼 ×
{((subringAlg ‘ℝfld)‘ℝ)})) ↾s (Base‘𝐻)) toNrmGrp (𝑥 ∈ (Base‘((ℝfldXs(𝐼 ×
{((subringAlg ‘ℝfld)‘ℝ)})) ↾s (Base‘𝐻))) ↦ (√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥)))))) | 
| 10 | 9 | eqcomd 2743 | . . . 4
⊢ ((𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥))) ∈ V →
(Scalar‘(((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s (Base‘𝐻)) toNrmGrp (𝑥
∈ (Base‘((ℝfldXs(𝐼 ×
{((subringAlg ‘ℝfld)‘ℝ)})) ↾s (Base‘𝐻))) ↦ (√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥))))) = (Scalar‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))) | 
| 11 | 6, 10 | mp1i 13 | . . 3
⊢ (𝐼 ∈ 𝑉 →
(Scalar‘(((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)) toNrmGrp
(𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥))))) = (Scalar‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))) | 
| 12 |  | eqid 2737 | . . . . . 6
⊢
(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) =
(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) | 
| 13 |  | eqid 2737 | . . . . . 6
⊢
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) =
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) | 
| 14 |  | eqid 2737 | . . . . . 6
⊢
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) =
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) | 
| 15 | 12, 13, 14 | tcphval 25252 | . . . . 5
⊢
(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) =
(((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)) toNrmGrp
(𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥)))) | 
| 16 | 15 | fveq2i 6909 | . . . 4
⊢
(Scalar‘(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)))) =
(Scalar‘(((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)) toNrmGrp
(𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥))))) | 
| 17 | 16 | a1i 11 | . . 3
⊢ (𝐼 ∈ 𝑉 →
(Scalar‘(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)))) =
(Scalar‘(((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)) toNrmGrp
(𝑥 ∈
(Base‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻))) ↦
(√‘(𝑥(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)}))
↾s (Base‘𝐻)))𝑥)))))) | 
| 18 |  | eqid 2737 | . . . . 5
⊢
(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) = (ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) | 
| 19 |  | refld 21637 | . . . . . 6
⊢
ℝfld ∈ Field | 
| 20 | 19 | a1i 11 | . . . . 5
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) | 
| 21 |  | id 22 | . . . . . 6
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) | 
| 22 |  | snex 5436 | . . . . . . 7
⊢
{((subringAlg ‘ℝfld)‘ℝ)} ∈
V | 
| 23 | 22 | a1i 11 | . . . . . 6
⊢ (𝐼 ∈ 𝑉 → {((subringAlg
‘ℝfld)‘ℝ)} ∈ V) | 
| 24 | 21, 23 | xpexd 7771 | . . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) ∈ V) | 
| 25 | 18, 20, 24 | prdssca 17501 | . . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld =
(Scalar‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})))) | 
| 26 |  | fvex 6919 | . . . . 5
⊢
(Base‘𝐻)
∈ V | 
| 27 |  | eqid 2737 | . . . . . 6
⊢
((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)) =
((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)) | 
| 28 |  | eqid 2737 | . . . . . 6
⊢
(Scalar‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(Scalar‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) | 
| 29 | 27, 28 | resssca 17387 | . . . . 5
⊢
((Base‘𝐻)
∈ V → (Scalar‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(Scalar‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)))) | 
| 30 | 26, 29 | mp1i 13 | . . . 4
⊢ (𝐼 ∈ 𝑉 →
(Scalar‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(Scalar‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)))) | 
| 31 | 25, 30 | eqtrd 2777 | . . 3
⊢ (𝐼 ∈ 𝑉 → ℝfld =
(Scalar‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)))) | 
| 32 | 11, 17, 31 | 3eqtr4d 2787 | . 2
⊢ (𝐼 ∈ 𝑉 →
(Scalar‘(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s
(Base‘𝐻)))) =
ℝfld) | 
| 33 | 4, 32 | eqtrd 2777 | 1
⊢ (𝐼 ∈ 𝑉 → (Scalar‘𝐻) = ℝfld) |