Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . 3
⊢ 𝐻 = (ℝ^‘𝐼) |
2 | 1 | rrxval 23175 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂHil‘(ℝfld freeLMod 𝐼))) |
3 | | eqid 2622 |
. . 3
⊢
(toℂHil‘(ℝfld freeLMod 𝐼)) =
(toℂHil‘(ℝfld freeLMod 𝐼)) |
4 | | eqid 2622 |
. . 3
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) |
5 | | eqid 2622 |
. . 3
⊢
(Scalar‘(ℝfld freeLMod 𝐼)) = (Scalar‘(ℝfld
freeLMod 𝐼)) |
6 | | eqid 2622 |
. . . 4
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) |
7 | | rebase 19952 |
. . . 4
⊢ ℝ =
(Base‘ℝfld) |
8 | | remulr 19957 |
. . . 4
⊢ ·
= (.r‘ℝfld) |
9 | | eqid 2622 |
. . . 4
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(ℝfld freeLMod
𝐼)) |
10 | | eqid 2622 |
. . . 4
⊢
(0g‘(ℝfld freeLMod 𝐼)) =
(0g‘(ℝfld freeLMod 𝐼)) |
11 | | re0g 19958 |
. . . 4
⊢ 0 =
(0g‘ℝfld) |
12 | | refldcj 19966 |
. . . 4
⊢ ∗
= (*𝑟‘ℝfld) |
13 | | refld 19965 |
. . . . 5
⊢
ℝfld ∈ Field |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) |
15 | | fconstmpt 5163 |
. . . . 5
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
16 | 6, 7, 4 | frlmbasf 20104 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ) |
17 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑓:𝐼⟶ℝ → 𝑓 Fn 𝐼) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 Fn 𝐼) |
19 | 18 | 3adant3 1081 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼) |
20 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝐼 ∈ 𝑉) |
21 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
ℝfld ∈ Field) |
22 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼))) |
23 | 6, 7, 8, 4, 9 | frlmipval 20118 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ∈ 𝑉 ∧ ℝfld ∈ Field)
∧ (𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)))) →
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘𝑓 · 𝑓))) |
24 | 20, 21, 22, 22, 23 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘𝑓 · 𝑓))) |
25 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ V) |
26 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
27 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
28 | 18, 18, 20, 20, 26, 27, 27 | offval 6904 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥)))) |
29 | 18, 18, 20, 20, 26, 27, 27 | ofval 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘𝑓 · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
30 | 16 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
31 | 30, 30 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
32 | 29, 31 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘𝑓 · 𝑓)‘𝑥) ∈ ℝ) |
33 | 25, 28, 32 | fmpt2d 6393 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓):𝐼⟶ℝ) |
34 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓) ∈
V) |
35 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∘𝑓
· 𝑓):𝐼⟶ℝ → Fun
(𝑓
∘𝑓 · 𝑓)) |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → Fun
(𝑓
∘𝑓 · 𝑓)) |
37 | 6, 11, 4 | frlmbasfsupp 20102 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 finSupp 0) |
38 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0
∈ ℝ) |
39 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
40 | 39 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℂ) |
41 | 40 | mul02d 10234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0
· 𝑥) =
0) |
42 | 20, 38, 16, 16, 41 | suppofss1d 7332 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓
∘𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0)) |
43 | | fsuppsssupp 8291 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓 ∘𝑓
· 𝑓) ∈ V ∧
Fun (𝑓
∘𝑓 · 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘𝑓
· 𝑓) finSupp
0) |
44 | 34, 36, 37, 42, 43 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘𝑓
· 𝑓) finSupp
0) |
45 | | regsumsupp 19968 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∘𝑓
· 𝑓):𝐼⟶ℝ ∧ (𝑓 ∘𝑓
· 𝑓) finSupp 0 ∧
𝐼 ∈ 𝑉) → (ℝfld
Σg (𝑓 ∘𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓 ∘𝑓 · 𝑓)‘𝑥)) |
46 | 33, 44, 20, 45 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓 ∘𝑓 · 𝑓)‘𝑥)) |
47 | | suppssdm 7308 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 supp 0) ⊆ dom 𝑓 |
48 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:𝐼⟶ℝ → dom 𝑓 = 𝐼) |
49 | 16, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → dom
𝑓 = 𝐼) |
50 | 47, 49 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼) |
51 | 42, 50 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓
∘𝑓 · 𝑓) supp 0) ⊆ 𝐼) |
52 | 51 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → 𝑥 ∈ 𝐼) |
53 | 52, 29 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓 ∘𝑓
· 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
54 | 53 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
Σ𝑥 ∈ ((𝑓 ∘𝑓
· 𝑓) supp 0)((𝑓 ∘𝑓
· 𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
55 | 46, 54 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
56 | 24, 55 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘𝑓 ·
𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
57 | 56 | 3adant3 1081 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘𝑓 ·
𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
58 | | simp3 1063 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) |
59 | 57, 58 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
60 | 37 | fsuppimpd 8282 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ∈
Fin) |
61 | | ssfi 8180 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 supp 0) ∈ Fin ∧
((𝑓
∘𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0)) → ((𝑓 ∘𝑓 · 𝑓) supp 0) ∈
Fin) |
62 | 60, 42, 61 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓
∘𝑓 · 𝑓) supp 0) ∈ Fin) |
63 | 52, 31 | syldan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
64 | 30 | msqge0d 10596 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
65 | 52, 64 | syldan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
66 | 62, 63, 65 | fsum00 14530 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(Σ𝑥 ∈ ((𝑓 ∘𝑓
· 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)) |
67 | 66 | 3adant3 1081 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ∀𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
68 | 59, 67 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
69 | 68 | r19.21bi 2932 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓
∘𝑓 · 𝑓) supp
0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
70 | 69 | adantlr 751 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0) |
71 | 30 | 3adantl3 1219 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℝ) |
72 | 71 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℂ) |
73 | 72, 72 | mul0ord 10677 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) =
0))) |
74 | 73 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → (((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
75 | 70, 74 | mpbid 222 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0)) |
76 | | oridm 536 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0) |
77 | 75, 76 | sylib 208 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0)) → (𝑓‘𝑥) =
0) |
78 | 33 | 3adant3 1081 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘𝑓 · 𝑓):𝐼⟶ℝ) |
79 | 78 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓 ∘𝑓 ·
𝑓):𝐼⟶ℝ) |
80 | | ssid 3624 |
. . . . . . . . . . 11
⊢ ((𝑓 ∘𝑓
· 𝑓) supp 0) ⊆
((𝑓
∘𝑓 · 𝑓) supp 0) |
81 | 80 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ ((𝑓 ∘𝑓 ·
𝑓) supp 0) ⊆ ((𝑓 ∘𝑓 · 𝑓) supp 0)) |
82 | | simpl1 1064 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝐼 ∈ 𝑉) |
83 | | 0red 10041 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 0 ∈ ℝ) |
84 | 79, 81, 82, 83 | suppssr 7326 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘𝑓 · 𝑓) supp
0))) → ((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0) |
85 | 29 | 3adantl3 1219 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ ((𝑓 ∘𝑓 ·
𝑓)‘𝑥) = ((𝑓‘𝑥)
· (𝑓‘𝑥))) |
86 | 85 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
87 | 86, 73 | bitrd 268 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
88 | 87, 76 | syl6bb 276 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘𝑓
· 𝑓)‘𝑥) = 0 ↔ (𝑓‘𝑥) =
0)) |
89 | 88 | biimpa 501 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ ((𝑓 ∘𝑓 ·
𝑓)‘𝑥) = 0) → (𝑓‘𝑥) =
0) |
90 | 84, 89 | syldan 487 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘𝑓 · 𝑓) supp
0))) → (𝑓‘𝑥) = 0) |
91 | | undif 4049 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∘𝑓
· 𝑓) supp 0) ⊆
𝐼 ↔ (((𝑓 ∘𝑓
· 𝑓) supp 0) ∪
(𝐼 ∖ ((𝑓 ∘𝑓
· 𝑓) supp 0))) =
𝐼) |
92 | 51, 91 | sylib 208 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(((𝑓
∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) = 𝐼) |
93 | 92 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
94 | 93 | 3adant3 1081 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓
∘𝑓 · 𝑓) supp 0)
∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
95 | 94 | biimpar 502 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝑥 ∈ (((𝑓 ∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓
∘𝑓 · 𝑓) supp
0)))) |
96 | | elun 3753 |
. . . . . . . . 9
⊢ (𝑥 ∈ (((𝑓 ∘𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘𝑓 · 𝑓) supp 0)))) |
97 | 95, 96 | sylib 208 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑥 ∈ ((𝑓 ∘𝑓 · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼
∖ ((𝑓 ∘𝑓
· 𝑓) supp 0)))) |
98 | 77, 90, 97 | mpjaodan 827 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) = 0) |
99 | 98 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼
(𝑓‘𝑥) = 0) |
100 | | fconstfv 6476 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)) |
101 | | c0ex 10034 |
. . . . . . . 8
⊢ 0 ∈
V |
102 | 101 | fconst2 6470 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0})) |
103 | 100, 102 | sylbb1 227 |
. . . . . 6
⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0})) |
104 | 19, 99, 103 | syl2anc 693 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 ×
{0})) |
105 | | isfld 18756 |
. . . . . . . . . . 11
⊢
(ℝfld ∈ Field ↔ (ℝfld ∈
DivRing ∧ ℝfld ∈ CRing)) |
106 | 13, 105 | mpbi 220 |
. . . . . . . . . 10
⊢
(ℝfld ∈ DivRing ∧ ℝfld ∈
CRing) |
107 | 106 | simpli 474 |
. . . . . . . . 9
⊢
ℝfld ∈ DivRing |
108 | | drngring 18754 |
. . . . . . . . 9
⊢
(ℝfld ∈ DivRing → ℝfld
∈ Ring) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . 8
⊢
ℝfld ∈ Ring |
110 | 6, 11 | frlm0 20098 |
. . . . . . . 8
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
111 | 109, 110 | mpan 706 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
112 | 15, 111 | syl5reqr 2671 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
(0g‘(ℝfld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0)) |
113 | 112 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (0g‘(ℝfld
freeLMod 𝐼)) = (𝑥 ∈ 𝐼
↦ 0)) |
114 | 15, 104, 113 | 3eqtr4a 2682 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0g‘(ℝfld freeLMod 𝐼))) |
115 | | cjre 13879 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(∗‘𝑥) = 𝑥) |
116 | 115 | adantl 482 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥) |
117 | | id 22 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
118 | 6, 7, 8, 4, 9, 10,
11, 12, 14, 114, 116, 117 | frlmphl 20120 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
PreHil) |
119 | | df-refld 19951 |
. . . 4
⊢
ℝfld = (ℂfld ↾s
ℝ) |
120 | 6 | frlmsca 20097 |
. . . . 5
⊢
((ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
121 | 13, 120 | mpan 706 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
122 | 119, 121 | syl5reqr 2671 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝfld
freeLMod 𝐼)) =
(ℂfld ↾s ℝ)) |
123 | | simpr1 1067 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ) |
124 | | simpr3 1069 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓) |
125 | 123, 124 | resqrtcld 14156 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈
ℝ) |
126 | 62, 63, 65 | fsumge0 14527 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
Σ𝑥 ∈ ((𝑓 ∘𝑓
· 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
127 | 126, 55 | breqtrrd 4681 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(ℝfld Σg (𝑓 ∘𝑓 · 𝑓))) |
128 | 127, 24 | breqtrrd 4681 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)) |
129 | 3, 4, 5, 118, 122, 9, 125, 128 | tchcph 23036 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(toℂHil‘(ℝfld freeLMod 𝐼)) ∈ ℂPreHil) |
130 | 2, 129 | eqeltrd 2701 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil) |