Step | Hyp | Ref
| Expression |
1 | | recrng 19786 |
. . . . 5
⊢
ℝfld ∈ *-Ring |
2 | | srngring 18675 |
. . . . 5
⊢
(ℝfld ∈ *-Ring → ℝfld ∈
Ring) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢
ℝfld ∈ Ring |
4 | | eqid 2610 |
. . . . 5
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) |
5 | 4 | frlmlmod 19912 |
. . . 4
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (ℝfld freeLMod
𝐼) ∈
LMod) |
6 | 3, 5 | mpan 702 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
LMod) |
7 | | lmodgrp 18693 |
. . 3
⊢
((ℝfld freeLMod 𝐼) ∈ LMod → (ℝfld
freeLMod 𝐼) ∈
Grp) |
8 | | eqid 2610 |
. . . 4
⊢
(toℂHil‘(ℝfld freeLMod 𝐼)) =
(toℂHil‘(ℝfld freeLMod 𝐼)) |
9 | | eqid 2610 |
. . . 4
⊢
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) =
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) |
10 | | eqid 2610 |
. . . 4
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) |
11 | | eqid 2610 |
. . . 4
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(ℝfld freeLMod
𝐼)) |
12 | 8, 9, 10, 11 | tchnmfval 22835 |
. . 3
⊢
((ℝfld freeLMod 𝐼) ∈ Grp →
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ↦
(√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)))) |
13 | 6, 7, 12 | 3syl 18 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼))) = (𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ↦
(√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)))) |
14 | | rrxval.r |
. . . 4
⊢ 𝐻 = (ℝ^‘𝐼) |
15 | 14 | rrxval 22983 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂHil‘(ℝfld freeLMod 𝐼))) |
16 | 15 | fveq2d 6107 |
. 2
⊢ (𝐼 ∈ 𝑉 → (norm‘𝐻) =
(norm‘(toℂHil‘(ℝfld freeLMod 𝐼)))) |
17 | 15 | fveq2d 6107 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (Base‘𝐻) =
(Base‘(toℂHil‘(ℝfld freeLMod 𝐼)))) |
18 | | rrxbase.b |
. . . 4
⊢ 𝐵 = (Base‘𝐻) |
19 | 8, 10 | tchbas 22826 |
. . . 4
⊢
(Base‘(ℝfld freeLMod 𝐼)) =
(Base‘(toℂHil‘(ℝfld freeLMod 𝐼))) |
20 | 17, 18, 19 | 3eqtr4g 2669 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐵 = (Base‘(ℝfld
freeLMod 𝐼))) |
21 | 14, 18 | rrxbase 22984 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐵 = {𝑓 ∈ (ℝ ↑𝑚
𝐼) ∣ 𝑓 finSupp 0}) |
22 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑓 ∈ (ℝ
↑𝑚 𝐼) ∣ 𝑓 finSupp 0} ⊆ (ℝ
↑𝑚 𝐼) |
23 | 21, 22 | syl6eqss 3618 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → 𝐵 ⊆ (ℝ ↑𝑚
𝐼)) |
24 | 23 | sselda 3568 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ (ℝ ↑𝑚
𝐼)) |
25 | 15 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘𝐻) =
(·𝑖‘(toℂHil‘(ℝfld
freeLMod 𝐼)))) |
26 | 14, 18 | rrxip 22986 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (ℎ ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) =
(·𝑖‘𝐻)) |
27 | 8, 11 | tchip 22832 |
. . . . . . . . . 10
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(toℂHil‘(ℝfld
freeLMod 𝐼))) |
28 | 27 | a1i 11 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfld freeLMod
𝐼)) =
(·𝑖‘(toℂHil‘(ℝfld
freeLMod 𝐼)))) |
29 | 25, 26, 28 | 3eqtr4rd 2655 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfld freeLMod
𝐼)) = (ℎ ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))))) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) →
(·𝑖‘(ℝfld freeLMod
𝐼)) = (ℎ ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))))) |
31 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → ℎ = 𝑓) |
32 | 31 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (ℎ‘𝑥) = (𝑓‘𝑥)) |
33 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → 𝑔 = 𝑓) |
34 | 33 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (𝑔‘𝑥) = (𝑓‘𝑥)) |
35 | 32, 34 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
36 | 35 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
37 | | elmapi 7765 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℝ
↑𝑚 𝐼) → 𝑓:𝐼⟶ℝ) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) → 𝑓:𝐼⟶ℝ) |
39 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
40 | 39 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ) |
41 | 40 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℂ) |
42 | 41 | sqvald 12867 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)↑2) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
43 | 36, 42 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑓‘𝑥)↑2)) |
44 | 43 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))) |
45 | 44 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) ∧ (ℎ = 𝑓 ∧ 𝑔 = 𝑓)) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) = (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) |
46 | | simpr 476 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) → 𝑓 ∈ (ℝ
↑𝑚 𝐼)) |
47 | | ovex 6577 |
. . . . . . . 8
⊢
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))) ∈ V |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) →
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))) ∈ V) |
49 | 30, 45, 46, 46, 48 | ovmpt2d 6686 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (ℝ ↑𝑚
𝐼)) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) |
50 | 24, 49 | syldan 486 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) |
51 | 50 | eqcomd 2616 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))) = (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)) |
52 | 51 | fveq2d 6107 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ 𝐵) →
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2)))) = (√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓))) |
53 | 20, 52 | mpteq12dva 4662 |
. 2
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ↦
(√‘(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)))) |
54 | 13, 16, 53 | 3eqtr4rd 2655 |
1
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦
(√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (norm‘𝐻)) |