| Step | Hyp | Ref
| Expression |
| 1 | | rrxval.r |
. . 3
⊢ 𝐻 = (ℝ^‘𝐼) |
| 2 | 1 | rrxval 25421 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂPreHil‘(ℝfld freeLMod 𝐼))) |
| 3 | | eqid 2737 |
. . 3
⊢
(toℂPreHil‘(ℝfld freeLMod 𝐼)) =
(toℂPreHil‘(ℝfld freeLMod 𝐼)) |
| 4 | | eqid 2737 |
. . 3
⊢
(Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld
freeLMod 𝐼)) |
| 5 | | eqid 2737 |
. . 3
⊢
(Scalar‘(ℝfld freeLMod 𝐼)) = (Scalar‘(ℝfld
freeLMod 𝐼)) |
| 6 | | eqid 2737 |
. . . 4
⊢
(ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼) |
| 7 | | rebase 21624 |
. . . 4
⊢ ℝ =
(Base‘ℝfld) |
| 8 | | remulr 21629 |
. . . 4
⊢ ·
= (.r‘ℝfld) |
| 9 | | eqid 2737 |
. . . 4
⊢
(·𝑖‘(ℝfld
freeLMod 𝐼)) =
(·𝑖‘(ℝfld freeLMod
𝐼)) |
| 10 | | eqid 2737 |
. . . 4
⊢
(0g‘(ℝfld freeLMod 𝐼)) =
(0g‘(ℝfld freeLMod 𝐼)) |
| 11 | | re0g 21630 |
. . . 4
⊢ 0 =
(0g‘ℝfld) |
| 12 | | refldcj 21638 |
. . . 4
⊢ ∗
= (*𝑟‘ℝfld) |
| 13 | | refld 21637 |
. . . . 5
⊢
ℝfld ∈ Field |
| 14 | 13 | a1i 11 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) |
| 15 | | fconstmpt 5747 |
. . . . 5
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
| 16 | 6, 7, 4 | frlmbasf 21780 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ) |
| 17 | 16 | ffnd 6737 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 Fn 𝐼) |
| 18 | 17 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼) |
| 19 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝐼 ∈ 𝑉) |
| 20 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
ℝfld ∈ Field) |
| 21 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼))) |
| 22 | 6, 7, 8, 4, 9 | frlmipval 21799 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ∈ 𝑉 ∧ ℝfld ∈ Field)
∧ (𝑓 ∈
(Base‘(ℝfld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)))) →
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘f · 𝑓))) |
| 23 | 19, 20, 21, 21, 22 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓 ∘f · 𝑓))) |
| 24 | | inidm 4227 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
| 25 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
| 26 | 17, 17, 19, 19, 24, 25, 25 | offval 7706 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑓‘𝑥)))) |
| 27 | 16 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℝ) |
| 28 | 27, 27 | remulcld 11291 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
| 29 | 26, 28 | fmpt3d 7136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓):𝐼⟶ℝ) |
| 30 | | ovexd 7466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) ∈
V) |
| 31 | 29 | ffund 6740 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → Fun
(𝑓 ∘f
· 𝑓)) |
| 32 | 6, 11, 4 | frlmbasfsupp 21778 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 𝑓 finSupp 0) |
| 33 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0
∈ ℝ) |
| 34 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
| 35 | 34 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℂ) |
| 36 | 35 | mul02d 11459 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0
· 𝑥) =
0) |
| 37 | 19, 33, 16, 16, 36 | suppofss1d 8229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ⊆
(𝑓 supp
0)) |
| 38 | | fsuppsssupp 9421 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓 ∘f ·
𝑓) ∈ V ∧ Fun
(𝑓 ∘f
· 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓 ∘f ·
𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓 ∘f ·
𝑓) finSupp
0) |
| 39 | 30, 31, 32, 37, 38 | syl22anc 839 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 ∘f ·
𝑓) finSupp
0) |
| 40 | | regsumsupp 21640 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∘f ·
𝑓):𝐼⟶ℝ ∧ (𝑓 ∘f · 𝑓) finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝfld
Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓 ∘f · 𝑓)‘𝑥)) |
| 41 | 29, 39, 19, 40 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓 ∘f · 𝑓)‘𝑥)) |
| 42 | | suppssdm 8202 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 supp 0) ⊆ dom 𝑓 |
| 43 | 42, 16 | fssdm 6755 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼) |
| 44 | 37, 43 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ⊆
𝐼) |
| 45 | 44 | sselda 3983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → 𝑥 ∈ 𝐼) |
| 46 | 17, 17, 19, 19, 24, 25, 25 | ofval 7708 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → ((𝑓 ∘f · 𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
| 47 | 45, 46 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓 ∘f ·
𝑓)‘𝑥) = ((𝑓‘𝑥) · (𝑓‘𝑥))) |
| 48 | 47 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓 ∘f ·
𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
| 49 | 41, 48 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(ℝfld Σg (𝑓 ∘f · 𝑓)) = Σ𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
| 50 | 23, 49 | eqtrd 2777 |
. . . . . . . . . . . . . . 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 2779 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
| 54 | 32 | fsuppimpd 9409 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → (𝑓 supp 0) ∈
Fin) |
| 55 | 54, 37 | ssfid 9301 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
((𝑓 ∘f
· 𝑓) supp 0) ∈
Fin) |
| 56 | 45, 28 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥) · (𝑓‘𝑥)) ∈ ℝ) |
| 57 | 27 | msqge0d 11831 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ 𝐼) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
| 58 | 45, 57 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → 0 ≤ ((𝑓‘𝑥) · (𝑓‘𝑥))) |
| 59 | 55, 56, 58 | fsum00 15834 |
. . . . . . . . . . . . . 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 232 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓
∘f · 𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥)) =
0) |
| 62 | 61 | r19.21bi 3251 |
. . . . . . . . . . 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 11289 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) ∈ ℂ) |
| 66 | 65, 65 | mul0ord 11913 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓‘𝑥) · (𝑓‘𝑥)) =
0 ↔ ((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) =
0))) |
| 67 | 66 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → (((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0 ↔ ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0))) |
| 68 | 63, 67 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
∧ 𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0)) → ((𝑓‘𝑥) = 0
∨ (𝑓‘𝑥) = 0)) |
| 69 | | oridm 905 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) = 0 ∨ (𝑓‘𝑥) = 0) ↔ (𝑓‘𝑥) = 0) |
| 70 | 68, 69 | sylib 218 |
. . . . . . . 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 480 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓 ∘f · 𝑓):𝐼⟶ℝ) |
| 73 | | ssidd 4007 |
. . . . . . . . . 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 11264 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 0 ∈ ℝ) |
| 76 | 72, 73, 74, 75 | suppssr 8220 |
. . . . . . . . 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 2739 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (((𝑓 ∘f · 𝑓)‘𝑥) = 0 ↔ ((𝑓‘𝑥)
· (𝑓‘𝑥)) = 0)) |
| 79 | 78, 66 | bitrd 279 |
. . . . . . . . . . 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 476 |
. . . . . . . . 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 4482 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∘f ·
𝑓) supp 0) ⊆ 𝐼 ↔ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) = 𝐼) |
| 84 | 44, 83 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) →
(((𝑓 ∘f
· 𝑓) supp 0) ∪
(𝐼 ∖ ((𝑓 ∘f ·
𝑓) supp 0))) = 𝐼) |
| 85 | 84 | eleq2d 2827 |
. . . . . . . . . . 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 477 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ 𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓
∘f · 𝑓) supp
0)))) |
| 88 | | elun 4153 |
. . . . . . . . 9
⊢ (𝑥 ∈ (((𝑓 ∘f · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓 ∘f · 𝑓) supp 0)))) |
| 89 | 87, 88 | sylib 218 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑥 ∈ ((𝑓 ∘f · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼
∖ ((𝑓 ∘f · 𝑓) supp 0)))) |
| 90 | 70, 82, 89 | mpjaodan 961 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ 𝐼)
→ (𝑓‘𝑥) = 0) |
| 91 | 90 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ 𝐼
(𝑓‘𝑥) = 0) |
| 92 | | fconstfv 7232 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0)) |
| 93 | | c0ex 11255 |
. . . . . . . 8
⊢ 0 ∈
V |
| 94 | 93 | fconst2 7225 |
. . . . . . 7
⊢ (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0})) |
| 95 | 92, 94 | sylbb1 237 |
. . . . . 6
⊢ ((𝑓 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) = 0) → 𝑓 = (𝐼 × {0})) |
| 96 | 18, 91, 95 | syl2anc 584 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 ×
{0})) |
| 97 | | isfld 20740 |
. . . . . . . . . . 11
⊢
(ℝfld ∈ Field ↔ (ℝfld ∈
DivRing ∧ ℝfld ∈ CRing)) |
| 98 | 13, 97 | mpbi 230 |
. . . . . . . . . 10
⊢
(ℝfld ∈ DivRing ∧ ℝfld ∈
CRing) |
| 99 | 98 | simpli 483 |
. . . . . . . . 9
⊢
ℝfld ∈ DivRing |
| 100 | | drngring 20736 |
. . . . . . . . 9
⊢
(ℝfld ∈ DivRing → ℝfld
∈ Ring) |
| 101 | 99, 100 | ax-mp 5 |
. . . . . . . 8
⊢
ℝfld ∈ Ring |
| 102 | 6, 11 | frlm0 21774 |
. . . . . . . 8
⊢
((ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
| 103 | 101, 102 | mpan 690 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) =
(0g‘(ℝfld freeLMod 𝐼))) |
| 104 | 103, 15 | eqtr3di 2792 |
. . . . . 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 2803 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0g‘(ℝfld freeLMod 𝐼))) |
| 107 | | cjre 15178 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(∗‘𝑥) = 𝑥) |
| 108 | 107 | adantl 481 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥) |
| 109 | | id 22 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
| 110 | 6, 7, 8, 4, 9, 10,
11, 12, 14, 106, 108, 109 | frlmphl 21801 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (ℝfld freeLMod
𝐼) ∈
PreHil) |
| 111 | 6 | frlmsca 21773 |
. . . . 5
⊢
((ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉) → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
| 112 | 13, 111 | mpan 690 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ℝfld =
(Scalar‘(ℝfld freeLMod 𝐼))) |
| 113 | | df-refld 21623 |
. . . 4
⊢
ℝfld = (ℂfld ↾s
ℝ) |
| 114 | 112, 113 | eqtr3di 2792 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Scalar‘(ℝfld
freeLMod 𝐼)) =
(ℂfld ↾s ℝ)) |
| 115 | | simpr1 1195 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ) |
| 116 | | simpr3 1197 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓) |
| 117 | 115, 116 | resqrtcld 15456 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈
ℝ) |
| 118 | 55, 56, 58 | fsumge0 15831 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
Σ𝑥 ∈ ((𝑓 ∘f ·
𝑓) supp 0)((𝑓‘𝑥) · (𝑓‘𝑥))) |
| 119 | 118, 49 | breqtrrd 5171 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(ℝfld Σg (𝑓 ∘f · 𝑓))) |
| 120 | 119, 23 | breqtrrd 5171 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑓 ∈ (Base‘(ℝfld
freeLMod 𝐼))) → 0 ≤
(𝑓(·𝑖‘(ℝfld
freeLMod 𝐼))𝑓)) |
| 121 | 3, 4, 5, 110, 114, 9, 117, 120 | tcphcph 25271 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(toℂPreHil‘(ℝfld freeLMod 𝐼)) ∈ ℂPreHil) |
| 122 | 2, 121 | eqeltrd 2841 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil) |