| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | resrng 21640 | . . . . 5
⊢
ℝfld ∈ *-Ring | 
| 2 |  | srngring 20848 | . . . . 5
⊢
(ℝfld ∈ *-Ring → ℝfld ∈
Ring) | 
| 3 | 1, 2 | ax-mp 5 | . . . 4
⊢
ℝfld ∈ Ring | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) | 
| 5 | 4 | frlmlmod 21770 | . . . 4
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (ℝfld freeLMod
𝐼) ∈
LMod) | 
| 6 | 3, 5 | mpan 690 | . . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
LMod) | 
| 7 |  | lmodgrp 20866 | . . 3
⊢
((ℝfld freeLMod 𝐼) ∈ LMod → (ℝfld
freeLMod 𝐼) ∈
Grp) | 
| 8 |  | eqid 2736 | . . . 4
⊢
(toℂPreHil‘(ℝfld freeLMod 𝐼)) =
(toℂPreHil‘(ℝfld freeLMod 𝐼)) | 
| 9 |  | eqid 2736 | . . . 4
⊢
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) =
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) | 
| 10 |  | eqid 2736 | . . . 4
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) | 
| 11 |  | eqid 2736 | . . . 4
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(ℝfld freeLMod
𝐼)) | 
| 12 | 8, 9, 10, 11 | tchnmfval 25263 | . . 3
⊢
((ℝfld freeLMod 𝐼) ∈ Grp →
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ↦
(√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)))) | 
| 13 | 6, 7, 12 | 3syl 18 | . 2
⊢ (𝐼 ∈ 𝑉 →
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ↦
(√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)))) | 
| 14 |  | rrxval.r | . . . 4
⊢ 𝐻 = (ℝ^‘𝐼) | 
| 15 | 14 | rrxval 25422 | . . 3
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂPreHil‘(ℝfld freeLMod 𝐼))) | 
| 16 | 15 | fveq2d 6909 | . 2
⊢ (𝐼 ∈ 𝑉 → (norm‘𝐻) =
(norm‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))) | 
| 17 | 15 | fveq2d 6909 | . . . 4
⊢ (𝐼 ∈ 𝑉 → (Base‘𝐻) =
(Base‘(toℂPreHil‘(ℝfld freeLMod 𝐼)))) | 
| 18 |  | rrxbase.b | . . . 4
⊢ 𝐵 = (Base‘𝐻) | 
| 19 | 8, 10 | tcphbas 25254 | . . . 4
⊢
(Base‘(ℝfld freeLMod 𝐼)) =
(Base‘(toℂPreHil‘(ℝfld freeLMod 𝐼))) | 
| 20 | 17, 18, 19 | 3eqtr4g 2801 | . . 3
⊢ (𝐼 ∈ 𝑉 → 𝐵 = (Base‘(ℝfld
freeLMod 𝐼))) | 
| 21 | 14, 18 | rrxbase 25423 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐵 = {𝑓 ∈ (ℝ ↑m 𝐼) ∣ 𝑓 finSupp 0}) | 
| 22 |  | ssrab2 4079 | . . . . . . . 8
⊢ {𝑓 ∈ (ℝ
↑m 𝐼)
∣ 𝑓 finSupp 0}
⊆ (ℝ ↑m 𝐼) | 
| 23 | 21, 22 | eqsstrdi 4027 | . . . . . . 7
⊢ (𝐼 ∈ 𝑉 → 𝐵 ⊆ (ℝ ↑m 𝐼)) | 
| 24 | 23 | sselda 3982 | . . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ (ℝ ↑m 𝐼)) | 
| 25 | 15 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘𝐻) =
(·𝑖‘(toℂPreHil‘(ℝfld
freeLMod 𝐼)))) | 
| 26 | 14, 18 | rrxip 25425 | . . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (ℎ ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) =
(·𝑖‘𝐻)) | 
| 27 | 8, 11 | tcphip 25260 | . . . . . . . . . 10
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(toℂPreHil‘(ℝfld
freeLMod 𝐼))) | 
| 28 | 27 | a1i 11 | . . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfld freeLMod
𝐼)) =
(·𝑖‘(toℂPreHil‘(ℝfld
freeLMod 𝐼)))) | 
| 29 | 25, 26, 28 | 3eqtr4rd 2787 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfld freeLMod
𝐼)) = (ℎ ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))))) | 
| 30 | 29 | adantr 480 | . . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) →
(·𝑖‘(ℝfld freeLMod
𝐼)) = (ℎ ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))))) | 
| 31 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → ℎ = 𝑓) | 
| 32 | 31 | fveq1d 6907 | . . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (ℎ‘𝑥) = (𝑓‘𝑥)) | 
| 33 |  | simprr 772 | . . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → 𝑔 = 𝑓) | 
| 34 | 33 | fveq1d 6907 | . . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (𝑔‘𝑥) = (𝑓‘𝑥)) | 
| 35 | 32, 34 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑓‘𝑥) · (𝑓‘𝑥))) | 
| 36 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑓‘𝑥) · (𝑓‘𝑥))) | 
| 37 |  | elmapi 8890 | . . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℝ
↑m 𝐼)
→ 𝑓:𝐼⟶ℝ) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) → 𝑓:𝐼⟶ℝ) | 
| 39 | 38 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) | 
| 40 | 39 | recnd 11290 | . . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ) | 
| 41 | 40 | adantlr 715 | . . . . . . . . . . 11
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ) | 
| 42 | 41 | sqvald 14184 | . . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)↑2) = ((𝑓‘𝑥) · (𝑓‘𝑥))) | 
| 43 | 36, 42 | eqtr4d 2779 | . . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑓‘𝑥)↑2)) | 
| 44 | 43 | mpteq2dva 5241 | . . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))) | 
| 45 | 44 | oveq2d 7448 | . . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) = (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) | 
| 46 |  | simpr 484 | . . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) → 𝑓 ∈ (ℝ ↑m 𝐼)) | 
| 47 |  | ovexd 7467 | . . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))) ∈ V) | 
| 48 | 30, 45, 46, 46, 47 | ovmpod 7586 | . . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑m 𝐼)) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) | 
| 49 | 24, 48 | syldan 591 | . . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) | 
| 50 | 49 | eqcomd 2742 | . . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))) = (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)) | 
| 51 | 50 | fveq2d 6909 | . . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) = (√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓))) | 
| 52 | 20, 51 | mpteq12dva 5230 | . 2
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ↦
(√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)))) | 
| 53 | 13, 16, 52 | 3eqtr4rd 2787 | 1
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (norm‘𝐻)) |