Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . 3
⊢ 𝐻 = (ℝ^‘𝐼) |
2 | 1 | rrxval 24132 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂPreHil‘(ℝfld freeLMod 𝐼))) |
3 | | eqid 2738 |
. . 3
⊢
(toℂPreHil‘(ℝfld freeLMod 𝐼)) =
(toℂPreHil‘(ℝfld freeLMod 𝐼)) |
4 | | eqid 2738 |
. . 3
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) |
5 | | eqid 2738 |
. . 3
⊢
(Scalar‘(ℝfld freeLMod 𝐼)) = (Scalar‘(ℝfld
freeLMod 𝐼)) |
6 | | eqid 2738 |
. . . 4
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) |
7 | | rebase 20415 |
. . . 4
⊢ ℝ =
(Base‘ℝfld) |
8 | | remulr 20420 |
. . . 4
⊢ ·
= (.r‘ℝfld) |
9 | | eqid 2738 |
. . . 4
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(ℝfld freeLMod
𝐼)) |
10 | | eqid 2738 |
. . . 4
⊢
(0g‘(ℝfld freeLMod 𝐼)) =
(0g‘(ℝfld freeLMod 𝐼)) |
11 | | re0g 20421 |
. . . 4
⊢ 0 =
(0g‘ℝfld) |
12 | | refldcj 20429 |
. . . 4
⊢ ∗
= (*𝑟‘ℝfld) |
13 | | refld 20428 |
. . . . 5
⊢
ℝfld ∈ Field |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) |
15 | | fconstmpt 5579 |
. . . . 5
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
16 | 6, 7, 4 | frlmbasf 20569 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ) |
17 | 16 | ffnd 6499 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 Fn 𝐼) |
18 | 17 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼) |
19 | | simpl 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝐼 ∈ 𝑉) |
20 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
ℝfld ∈ Field) |
21 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼))) |
22 | 6, 7, 8, 4, 9 | frlmipval 20588 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ∈ 𝑉 ∧ ℝfld ∈ Field)
∧ (𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)))) →
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘f · 𝑓))) |
23 | 19, 20, 21, 21, 22 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘f · 𝑓))) |
24 | | inidm 4107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
25 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
26 | 17, 17, 19, 19, 24, 25, 25 | offval 7427 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥)))) |
27 | 16 | ffvelrnda 6855 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
28 | 27, 27 | remulcld 10742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
29 | 26, 28 | fmpt3d 6884 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓):𝐼⟶ℝ) |
30 | | ovexd 7199 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) ∈
V) |
31 | 29 | ffund 6502 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → Fun
(𝑓 ∘f
· 𝑓)) |
32 | 6, 11, 4 | frlmbasfsupp 20567 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 finSupp 0) |
33 | | 0red 10715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0
∈ ℝ) |
34 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
35 | 34 | recnd 10740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℂ) |
36 | 35 | mul02d 10909 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0
· 𝑥) =
0) |
37 | 19, 33, 16, 16, 36 | suppofss1d 7892 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ⊆
(𝑓 supp
0)) |
38 | | fsuppsssupp 8915 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓 ∘f ·
𝑓) ∈ V ∧ Fun
(𝑓 ∘f
· 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘f ·
𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘f ·
𝑓) finSupp
0) |
39 | 30, 31, 32, 37, 38 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) finSupp
0) |
40 | | regsumsupp 20431 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∘f ·
𝑓):𝐼⟶ℝ ∧ (𝑓 ∘f · 𝑓) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝfld
Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓 ∘f · 𝑓)‘𝑥)) |
41 | 29, 39, 19, 40 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓 ∘f · 𝑓)‘𝑥)) |
42 | | suppssdm 7865 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 supp 0) ⊆ dom 𝑓 |
43 | 42, 16 | fssdm 6518 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼) |
44 | 37, 43 | sstrd 3885 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ⊆
𝐼) |
45 | 44 | sselda 3875 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → 𝑥 ∈ 𝐼) |
46 | 17, 17, 19, 19, 24, 25, 25 | ofval 7429 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
47 | 45, 46 | syldan 594 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓 ∘f ·
𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
48 | 47 | sumeq2dv 15146 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓 ∘f ·
𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
49 | 41, 48 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
50 | 23, 49 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
51 | 50 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
52 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) |
53 | 51, 52 | eqtr3d 2775 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
54 | 32 | fsuppimpd 8906 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ∈
Fin) |
55 | 54, 37 | ssfid 8812 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ∈
Fin) |
56 | 45, 28 | syldan 594 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
57 | 27 | msqge0d 11279 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
58 | 45, 57 | syldan 594 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
59 | 55, 56, 58 | fsum00 15239 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)) |
60 | 59 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ∀𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
61 | 53, 60 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
62 | 61 | r19.21bi 3120 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)) →
((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
63 | 62 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0) |
64 | 27 | 3adantl3 1169 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℝ) |
65 | 64 | recnd 10740 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℂ) |
66 | 65, 65 | mul0ord 11361 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) =
0))) |
67 | 66 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → (((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
68 | 63, 67 | mpbid 235 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0)) |
69 | | oridm 904 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0) |
70 | 68, 69 | sylib 221 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → (𝑓‘𝑥) =
0) |
71 | 29 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘f · 𝑓):𝐼⟶ℝ) |
72 | 71 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓 ∘f · 𝑓):𝐼⟶ℝ) |
73 | | ssidd 3898 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ ((𝑓 ∘f · 𝑓) supp 0) ⊆ ((𝑓 ∘f · 𝑓) supp 0)) |
74 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝐼 ∈ 𝑉) |
75 | | 0red 10715 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 0 ∈ ℝ) |
76 | 72, 73, 74, 75 | suppssr 7884 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘f · 𝑓) supp 0)))
→ ((𝑓 ∘f · 𝑓)‘𝑥) = 0) |
77 | 46 | 3adantl3 1169 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ ((𝑓 ∘f · 𝑓)‘𝑥) = ((𝑓‘𝑥)
· (𝑓‘𝑥))) |
78 | 77 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
79 | 78, 66 | bitrd 282 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
80 | 79, 69 | bitrdi 290 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘f · 𝑓)‘𝑥) = 0 ↔ (𝑓‘𝑥) =
0)) |
81 | 80 | biimpa 480 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ ((𝑓 ∘f · 𝑓)‘𝑥) = 0) → (𝑓‘𝑥) =
0) |
82 | 76, 81 | syldan 594 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘f · 𝑓) supp 0)))
→ (𝑓‘𝑥) = 0) |
83 | | undif 4368 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∘f ·
𝑓) supp 0) ⊆ 𝐼 ↔ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) = 𝐼) |
84 | 44, 83 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(((𝑓 ∘f
· 𝑓) supp 0) ∪
(𝐼 ∖ ((𝑓 ∘f ·
𝑓) supp 0))) = 𝐼) |
85 | 84 | eleq2d 2818 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
86 | 85 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓
∘f · 𝑓) supp 0) ∪
(𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
87 | 86 | biimpar 481 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓
∘f · 𝑓) supp
0)))) |
88 | | elun 4037 |
. . . . . . . . 9
⊢ (𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0)))) |
89 | 87, 88 | sylib 221 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼
∖ ((𝑓 ∘f · 𝑓) supp 0)))) |
90 | 70, 82, 89 | mpjaodan 958 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) = 0) |
91 | 90 | ralrimiva 3096 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼
(𝑓‘𝑥) = 0) |
92 | | fconstfv 6979 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)) |
93 | | c0ex 10706 |
. . . . . . . 8
⊢ 0 ∈
V |
94 | 93 | fconst2 6971 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0})) |
95 | 92, 94 | sylbb1 240 |
. . . . . 6
⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0})) |
96 | 18, 91, 95 | syl2anc 587 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 ×
{0})) |
97 | | isfld 19623 |
. . . . . . . . . . 11
⊢
(ℝfld ∈ Field ↔ (ℝfld ∈
DivRing ∧ ℝfld ∈ CRing)) |
98 | 13, 97 | mpbi 233 |
. . . . . . . . . 10
⊢
(ℝfld ∈ DivRing ∧ ℝfld ∈
CRing) |
99 | 98 | simpli 487 |
. . . . . . . . 9
⊢
ℝfld ∈ DivRing |
100 | | drngring 19621 |
. . . . . . . . 9
⊢
(ℝfld ∈ DivRing → ℝfld
∈ Ring) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . 8
⊢
ℝfld ∈ Ring |
102 | 6, 11 | frlm0 20563 |
. . . . . . . 8
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
103 | 101, 102 | mpan 690 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
104 | 15, 103 | syl5reqr 2788 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
(0g‘(ℝfld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0)) |
105 | 104 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (0g‘(ℝfld
freeLMod 𝐼)) = (𝑥 ∈ 𝐼
↦ 0)) |
106 | 15, 96, 105 | 3eqtr4a 2799 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0g‘(ℝfld freeLMod 𝐼))) |
107 | | cjre 14581 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(∗‘𝑥) = 𝑥) |
108 | 107 | adantl 485 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥) |
109 | | id 22 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
110 | 6, 7, 8, 4, 9, 10,
11, 12, 14, 106, 108, 109 | frlmphl 20590 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
PreHil) |
111 | | df-refld 20414 |
. . . 4
⊢
ℝfld = (ℂfld ↾s
ℝ) |
112 | 6 | frlmsca 20562 |
. . . . 5
⊢
((ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
113 | 13, 112 | mpan 690 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
114 | 111, 113 | syl5reqr 2788 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝfld
freeLMod 𝐼)) =
(ℂfld ↾s ℝ)) |
115 | | simpr1 1195 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ) |
116 | | simpr3 1197 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓) |
117 | 115, 116 | resqrtcld 14860 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈
ℝ) |
118 | 55, 56, 58 | fsumge0 15236 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
119 | 118, 49 | breqtrrd 5055 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(ℝfld Σg (𝑓 ∘f · 𝑓))) |
120 | 119, 23 | breqtrrd 5055 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)) |
121 | 3, 4, 5, 110, 114, 9, 117, 120 | tcphcph 23982 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(toℂPreHil‘(ℝfld freeLMod 𝐼)) ∈ ℂPreHil) |
122 | 2, 121 | eqeltrd 2833 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil) |