Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . 3
⊢ 𝐻 = (ℝ^‘𝐼) |
2 | 1 | rrxval 24551 |
. 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 20811 |
. . . 4
⊢ ℝ =
(Base‘ℝfld) |
8 | | remulr 20816 |
. . . 4
⊢ ·
= (.r‘ℝfld) |
9 | | eqid 2738 |
. . . 4
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(ℝfld freeLMod
𝐼)) |
10 | | eqid 2738 |
. . . 4
⊢
(0g‘(ℝfld freeLMod 𝐼)) =
(0g‘(ℝfld freeLMod 𝐼)) |
11 | | re0g 20817 |
. . . 4
⊢ 0 =
(0g‘ℝfld) |
12 | | refldcj 20825 |
. . . 4
⊢ ∗
= (*𝑟‘ℝfld) |
13 | | refld 20824 |
. . . . 5
⊢
ℝfld ∈ Field |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) |
15 | | fconstmpt 5649 |
. . . . 5
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
16 | 6, 7, 4 | frlmbasf 20967 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ) |
17 | 16 | ffnd 6601 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 Fn 𝐼) |
18 | 17 | 3adant3 1131 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼) |
19 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝐼 ∈ 𝑉) |
20 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
ℝfld ∈ Field) |
21 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼))) |
22 | 6, 7, 8, 4, 9 | frlmipval 20986 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ∈ 𝑉 ∧ ℝfld ∈ Field)
∧ (𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)))) →
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘f · 𝑓))) |
23 | 19, 20, 21, 21, 22 | syl22anc 836 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘f · 𝑓))) |
24 | | inidm 4152 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
25 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
26 | 17, 17, 19, 19, 24, 25, 25 | offval 7542 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥)))) |
27 | 16 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
28 | 27, 27 | remulcld 11005 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
29 | 26, 28 | fmpt3d 6990 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓):𝐼⟶ℝ) |
30 | | ovexd 7310 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) ∈
V) |
31 | 29 | ffund 6604 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → Fun
(𝑓 ∘f
· 𝑓)) |
32 | 6, 11, 4 | frlmbasfsupp 20965 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 finSupp 0) |
33 | | 0red 10978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0
∈ ℝ) |
34 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
35 | 34 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℂ) |
36 | 35 | mul02d 11173 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0
· 𝑥) =
0) |
37 | 19, 33, 16, 16, 36 | suppofss1d 8020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ⊆
(𝑓 supp
0)) |
38 | | fsuppsssupp 9144 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓 ∘f ·
𝑓) ∈ V ∧ Fun
(𝑓 ∘f
· 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘f ·
𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘f ·
𝑓) finSupp
0) |
39 | 30, 31, 32, 37, 38 | syl22anc 836 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) finSupp
0) |
40 | | regsumsupp 20827 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∘f ·
𝑓):𝐼⟶ℝ ∧ (𝑓 ∘f · 𝑓) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝfld
Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓 ∘f · 𝑓)‘𝑥)) |
41 | 29, 39, 19, 40 | syl3anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓 ∘f · 𝑓)‘𝑥)) |
42 | | suppssdm 7993 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 supp 0) ⊆ dom 𝑓 |
43 | 42, 16 | fssdm 6620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼) |
44 | 37, 43 | sstrd 3931 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ⊆
𝐼) |
45 | 44 | sselda 3921 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → 𝑥 ∈ 𝐼) |
46 | 17, 17, 19, 19, 24, 25, 25 | ofval 7544 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
47 | 45, 46 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓 ∘f ·
𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
48 | 47 | sumeq2dv 15415 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓 ∘f ·
𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
49 | 41, 48 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
50 | 23, 49 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
51 | 50 | 3adant3 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = Σ𝑥
∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥))) |
52 | | simp3 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) |
53 | 51, 52 | eqtr3d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
54 | 32 | fsuppimpd 9135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ∈
Fin) |
55 | 54, 37 | ssfid 9042 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ∈
Fin) |
56 | 45, 28 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
57 | 27 | msqge0d 11543 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
58 | 45, 57 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
59 | 55, 56, 58 | fsum00 15510 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) = 0)) |
60 | 59 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ∀𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
61 | 53, 60 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
62 | 61 | r19.21bi 3134 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)) →
((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
63 | 62 | adantlr 712 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0) |
64 | 27 | 3adantl3 1167 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℝ) |
65 | 64 | recnd 11003 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℂ) |
66 | 65, 65 | mul0ord 11625 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) =
0))) |
67 | 66 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → (((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
68 | 63, 67 | mpbid 231 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0)) |
69 | | oridm 902 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0) |
70 | 68, 69 | sylib 217 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → (𝑓‘𝑥) =
0) |
71 | 29 | 3adant3 1131 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑓 ∘f · 𝑓):𝐼⟶ℝ) |
72 | 71 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓 ∘f · 𝑓):𝐼⟶ℝ) |
73 | | ssidd 3944 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ ((𝑓 ∘f · 𝑓) supp 0) ⊆ ((𝑓 ∘f · 𝑓) supp 0)) |
74 | | simpl1 1190 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝐼 ∈ 𝑉) |
75 | | 0red 10978 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 0 ∈ ℝ) |
76 | 72, 73, 74, 75 | suppssr 8012 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘f · 𝑓) supp 0)))
→ ((𝑓 ∘f · 𝑓)‘𝑥) = 0) |
77 | 46 | 3adantl3 1167 |
. . . . . . . . . . . . 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 278 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
80 | 79, 69 | bitrdi 287 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘f · 𝑓)‘𝑥) = 0 ↔ (𝑓‘𝑥) =
0)) |
81 | 80 | biimpa 477 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ ((𝑓 ∘f · 𝑓)‘𝑥) = 0) → (𝑓‘𝑥) =
0) |
82 | 76, 81 | syldan 591 |
. . . . . . . 8
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ (𝐼 ∖ ((𝑓
∘f · 𝑓) supp 0)))
→ (𝑓‘𝑥) = 0) |
83 | | undif 4415 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∘f ·
𝑓) supp 0) ⊆ 𝐼 ↔ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) = 𝐼) |
84 | 44, 83 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(((𝑓 ∘f
· 𝑓) supp 0) ∪
(𝐼 ∖ ((𝑓 ∘f ·
𝑓) supp 0))) = 𝐼) |
85 | 84 | eleq2d 2824 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
86 | 85 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓
∘f · 𝑓) supp 0) ∪
(𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) ↔ 𝑥 ∈ 𝐼)) |
87 | 86 | biimpar 478 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓
∘f · 𝑓) supp
0)))) |
88 | | elun 4083 |
. . . . . . . . 9
⊢ (𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0)))) |
89 | 87, 88 | sylib 217 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼
∖ ((𝑓 ∘f · 𝑓) supp 0)))) |
90 | 70, 82, 89 | mpjaodan 956 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) = 0) |
91 | 90 | ralrimiva 3103 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼
(𝑓‘𝑥) = 0) |
92 | | fconstfv 7088 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)) |
93 | | c0ex 10969 |
. . . . . . . 8
⊢ 0 ∈
V |
94 | 93 | fconst2 7080 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0})) |
95 | 92, 94 | sylbb1 236 |
. . . . . 6
⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0})) |
96 | 18, 91, 95 | syl2anc 584 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 ×
{0})) |
97 | | isfld 20000 |
. . . . . . . . . . 11
⊢
(ℝfld ∈ Field ↔ (ℝfld ∈
DivRing ∧ ℝfld ∈ CRing)) |
98 | 13, 97 | mpbi 229 |
. . . . . . . . . 10
⊢
(ℝfld ∈ DivRing ∧ ℝfld ∈
CRing) |
99 | 98 | simpli 484 |
. . . . . . . . 9
⊢
ℝfld ∈ DivRing |
100 | | drngring 19998 |
. . . . . . . . 9
⊢
(ℝfld ∈ DivRing → ℝfld
∈ Ring) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . 8
⊢
ℝfld ∈ Ring |
102 | 6, 11 | frlm0 20961 |
. . . . . . . 8
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
103 | 101, 102 | mpan 687 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
104 | 103, 15 | eqtr3di 2793 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
(0g‘(ℝfld freeLMod 𝐼)) = (𝑥 ∈ 𝐼 ↦ 0)) |
105 | 104 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → (0g‘(ℝfld
freeLMod 𝐼)) = (𝑥 ∈ 𝐼
↦ 0)) |
106 | 15, 96, 105 | 3eqtr4a 2804 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0g‘(ℝfld freeLMod 𝐼))) |
107 | | cjre 14850 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(∗‘𝑥) = 𝑥) |
108 | 107 | adantl 482 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥) |
109 | | id 22 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
110 | 6, 7, 8, 4, 9, 10,
11, 12, 14, 106, 108, 109 | frlmphl 20988 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
PreHil) |
111 | 6 | frlmsca 20960 |
. . . . 5
⊢
((ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
112 | 13, 111 | mpan 687 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
113 | | df-refld 20810 |
. . . 4
⊢
ℝfld = (ℂfld ↾s
ℝ) |
114 | 112, 113 | eqtr3di 2793 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝfld
freeLMod 𝐼)) =
(ℂfld ↾s ℝ)) |
115 | | simpr1 1193 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ) |
116 | | simpr3 1195 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓) |
117 | 115, 116 | resqrtcld 15129 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈
ℝ) |
118 | 55, 56, 58 | fsumge0 15507 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
119 | 118, 49 | breqtrrd 5102 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(ℝfld Σg (𝑓 ∘f · 𝑓))) |
120 | 119, 23 | breqtrrd 5102 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)) |
121 | 3, 4, 5, 110, 114, 9, 117, 120 | tcphcph 24401 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(toℂPreHil‘(ℝfld freeLMod 𝐼)) ∈ ℂPreHil) |
122 | 2, 121 | eqeltrd 2839 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil) |