Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . 3
⊢ 𝐻 = (ℝ^‘𝐼) |
2 | 1 | rrxval 22983 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂHil‘(ℝfld freeLMod 𝐼))) |
3 | | eqid 2610 |
. . 3
⊢
(toℂHil‘(ℝfld freeLMod 𝐼)) =
(toℂHil‘(ℝfld freeLMod 𝐼)) |
4 | | eqid 2610 |
. . 3
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) |
5 | | eqid 2610 |
. . 3
⊢
(Scalar‘(ℝfld freeLMod 𝐼)) = (Scalar‘(ℝfld
freeLMod 𝐼)) |
6 | | eqid 2610 |
. . . 4
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) |
7 | | rebase 19771 |
. . . 4
⊢ ℝ =
(Base‘ℝfld) |
8 | | remulr 19776 |
. . . 4
⊢ ·
= (.r‘ℝfld) |
9 | | eqid 2610 |
. . . 4
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(ℝfld freeLMod
𝐼)) |
10 | | eqid 2610 |
. . . 4
⊢
(0g‘(ℝfld freeLMod 𝐼)) =
(0g‘(ℝfld freeLMod 𝐼)) |
11 | | re0g 19777 |
. . . 4
⊢ 0 =
(0g‘ℝfld) |
12 | | refldcj 19785 |
. . . 4
⊢ ∗
= (*𝑟‘ℝfld) |
13 | | refld 19784 |
. . . . 5
⊢
ℝfld ∈ Field |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) |
15 | | fconstmpt 5085 |
. . . . 5
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
16 | 6, 7, 4 | frlmbasf 19923 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ) |
17 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑓:𝐼⟶ℝ → 𝑓 Fn 𝐼) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 Fn 𝐼) |
19 | 18 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼) |
20 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝐼 ∈ 𝑉) |
21 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
ℝfld ∈ Field) |
22 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼))) |
23 | 6, 7, 8, 4, 9 | frlmipval 19937 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ∈ 𝑉 ∧ ℝfld ∈ Field)
∧ (𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)))) →
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘𝑓 · 𝑓))) |
24 | 20, 21, 22, 22, 23 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘𝑓 · 𝑓))) |
25 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ V |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ V) |
27 | | inidm 3784 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
28 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
29 | 18, 18, 20, 20, 27, 28, 28 | offval 6802 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥)))) |
30 | 18, 18, 20, 20, 27, 28, 28 | ofval 6804 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘𝑓 · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
31 | 16 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
32 | 31, 31 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
33 | 30, 32 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘𝑓 · 𝑓)‘𝑥) ∈ ℝ) |
34 | 26, 29, 33 | fmpt2d 6300 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓):𝐼⟶ℝ) |
35 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∘𝑓
· 𝑓) ∈
V |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓) ∈
V) |
37 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∘𝑓
· 𝑓):𝐼⟶ℝ → Fun
(𝑓
∘𝑓 · 𝑓)) |
38 | 34, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → Fun
(𝑓
∘𝑓 · 𝑓)) |
39 | 6, 11, 4 | frlmbasfsupp 19921 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 finSupp 0) |
40 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0
∈ ℝ) |
41 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
42 | 41 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℂ) |
43 | 42 | mul02d 10113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0
· 𝑥) =
0) |
44 | 20, 40, 16, 16, 43 | suppofss1d 7219 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓
∘𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0)) |
45 | | fsuppsssupp 8174 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓 ∘𝑓
· 𝑓) ∈ V ∧
Fun (𝑓
∘𝑓 · 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘𝑓
· 𝑓) finSupp
0) |
46 | 36, 38, 39, 44, 45 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓) finSupp
0) |
47 | | regsumsupp 19787 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∘𝑓
· 𝑓):𝐼⟶ℝ ∧ (𝑓 ∘𝑓
· 𝑓) finSupp 0 ∧
𝐼 ∈ 𝑉) → (ℝfld
Σg (𝑓 ∘𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓 ∘𝑓 · 𝑓)‘𝑥)) |
48 | 34, 46, 20, 47 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓 ∘𝑓 · 𝑓)‘𝑥)) |
49 | | suppssdm 7195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 supp 0) ⊆ dom 𝑓 |
50 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:𝐼⟶ℝ → dom 𝑓 = 𝐼) |
51 | 16, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → dom
𝑓 = 𝐼) |
52 | 49, 51 | syl5sseq 3616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼) |
53 | 44, 52 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓
∘𝑓 · 𝑓) supp 0) ⊆ 𝐼) |
54 | 53 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → 𝑥 ∈ 𝐼) |
55 | 54, 30 | syldan 486 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓 ∘𝑓
· 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
56 | 55 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
Σ𝑥 ∈ ((𝑓 ∘𝑓
· 𝑓) supp 0)((𝑓 ∘𝑓
· 𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
57 | 48, 56 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
58 | 24, 57 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘𝑓 ·
𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
59 | 58 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘𝑓 ·
𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
60 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) |
61 | 59, 60 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
62 | 39 | fsuppimpd 8165 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ∈
Fin) |
63 | | ssfi 8065 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 supp 0) ∈ Fin ∧
((𝑓
∘𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0)) → ((𝑓 ∘𝑓 · 𝑓) supp 0) ∈
Fin) |
64 | 62, 44, 63 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓
∘𝑓 · 𝑓) supp 0) ∈ Fin) |
65 | 54, 32 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
66 | 31 | msqge0d 10475 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
67 | 54, 66 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
68 | 64, 65, 67 | fsum00 14371 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(Σ𝑥 ∈ ((𝑓 ∘𝑓
· 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)) |
69 | 68 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ∀𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
70 | 61, 69 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
71 | 70 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
72 | 71 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0) |
73 | 31 | 3adantl3 1212 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℝ) |
74 | 73 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℂ) |
75 | 74, 74 | mul0ord 10556 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) =
0))) |
76 | 75 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → (((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
77 | 72, 76 | mpbid 221 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0)) |
78 | | oridm 535 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0) |
79 | 77, 78 | sylib 207 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → (𝑓‘𝑥) =
0) |
80 | 34 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘𝑓 · 𝑓):𝐼⟶ℝ) |
81 | 80 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓 ∘𝑓 ·
𝑓):𝐼⟶ℝ) |
82 | | ssid 3587 |
. . . . . . . . . . 11
⊢ ((𝑓 ∘𝑓
· 𝑓) supp 0) ⊆
((𝑓
∘𝑓 · 𝑓) supp 0) |
83 | 82 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ ((𝑓 ∘𝑓 ·
𝑓) supp 0) ⊆ ((𝑓 ∘𝑓 · 𝑓) supp 0)) |
84 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝐼 ∈ 𝑉) |
85 | | 0red 9920 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 0 ∈ ℝ) |
86 | 81, 83, 84, 85 | suppssr 7213 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘𝑓 · 𝑓) supp
0))) → ((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0) |
87 | 30 | 3adantl3 1212 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ ((𝑓 ∘𝑓 ·
𝑓)‘𝑥) = ((𝑓‘𝑥)
· (𝑓‘𝑥))) |
88 | 87 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
89 | 88, 75 | bitrd 267 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
90 | 89, 78 | syl6bb 275 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0 ↔ (𝑓‘𝑥) =
0)) |
91 | 90 | biimpa 500 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ ((𝑓 ∘𝑓 ·
𝑓)‘𝑥) = 0) → (𝑓‘𝑥) =
0) |
92 | 86, 91 | syldan 486 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘𝑓 · 𝑓) supp
0))) → (𝑓‘𝑥) = 0) |
93 | | undif 4001 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∘𝑓
· 𝑓) supp 0) ⊆
𝐼 ↔ (((𝑓 ∘𝑓
· 𝑓) supp 0) ∪
(𝐼 ∖ ((𝑓 ∘𝑓
· 𝑓) supp 0))) =
𝐼) |
94 | 53, 93 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(((𝑓
∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) = 𝐼) |
95 | 94 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
96 | 95 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓
∘𝑓 · 𝑓) supp 0)
∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
97 | 96 | biimpar 501 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝑥 ∈ (((𝑓 ∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓
∘𝑓 · 𝑓) supp
0)))) |
98 | | elun 3715 |
. . . . . . . . 9
⊢ (𝑥 ∈ (((𝑓 ∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0)))) |
99 | 97, 98 | sylib 207 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼
∖ ((𝑓 ∘𝑓
· 𝑓) supp 0)))) |
100 | 79, 92, 99 | mpjaodan 823 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) = 0) |
101 | 100 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼
(𝑓‘𝑥) = 0) |
102 | | fconstfv 6381 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)) |
103 | | c0ex 9913 |
. . . . . . . 8
⊢ 0 ∈
V |
104 | 103 | fconst2 6375 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0})) |
105 | 102, 104 | sylbb1 226 |
. . . . . 6
⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0})) |
106 | 19, 101, 105 | syl2anc 691 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 ×
{0})) |
107 | | isfld 18579 |
. . . . . . . . . . 11
⊢
(ℝfld ∈ Field ↔ (ℝfld ∈
DivRing ∧ ℝfld ∈ CRing)) |
108 | 13, 107 | mpbi 219 |
. . . . . . . . . 10
⊢
(ℝfld ∈ DivRing ∧ ℝfld ∈
CRing) |
109 | 108 | simpli 473 |
. . . . . . . . 9
⊢
ℝfld ∈ DivRing |
110 | | drngring 18577 |
. . . . . . . . 9
⊢
(ℝfld ∈ DivRing → ℝfld
∈ Ring) |
111 | 109, 110 | ax-mp 5 |
. . . . . . . 8
⊢
ℝfld ∈ Ring |
112 | 6, 11 | frlm0 19917 |
. . . . . . . 8
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
113 | 111, 112 | mpan 702 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
114 | 15, 113 | syl5reqr 2659 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
(0g‘(ℝfld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0)) |
115 | 114 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (0g‘(ℝfld
freeLMod 𝐼)) = (𝑥 ∈ 𝐼
↦ 0)) |
116 | 15, 106, 115 | 3eqtr4a 2670 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0g‘(ℝfld freeLMod 𝐼))) |
117 | | cjre 13727 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(∗‘𝑥) = 𝑥) |
118 | 117 | adantl 481 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥) |
119 | | id 22 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
120 | 6, 7, 8, 4, 9, 10,
11, 12, 14, 116, 118, 119 | frlmphl 19939 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
PreHil) |
121 | | df-refld 19770 |
. . . 4
⊢
ℝfld = (ℂfld ↾s
ℝ) |
122 | 6 | frlmsca 19916 |
. . . . 5
⊢
((ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
123 | 13, 122 | mpan 702 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
124 | 121, 123 | syl5reqr 2659 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝfld
freeLMod 𝐼)) =
(ℂfld ↾s ℝ)) |
125 | | simpr1 1060 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ) |
126 | | simpr3 1062 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓) |
127 | 125, 126 | resqrtcld 14004 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈
ℝ) |
128 | 64, 65, 67 | fsumge0 14368 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
Σ𝑥 ∈ ((𝑓 ∘𝑓
· 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
129 | 128, 57 | breqtrrd 4611 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(ℝfld Σg (𝑓 ∘𝑓 · 𝑓))) |
130 | 129, 24 | breqtrrd 4611 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)) |
131 | 3, 4, 5, 120, 124, 9, 127, 130 | tchcph 22844 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(toℂHil‘(ℝfld freeLMod 𝐼)) ∈ ℂPreHil) |
132 | 2, 131 | eqeltrd 2688 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil) |