MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rrxcph Structured version   Visualization version   GIF version

Theorem rrxcph 23419
Description: Generalized Euclidean real spaces are pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)
Hypotheses
Ref Expression
rrxval.r 𝐻 = (ℝ^‘𝐼)
rrxbase.b 𝐵 = (Base‘𝐻)
Assertion
Ref Expression
rrxcph (𝐼𝑉𝐻 ∈ ℂPreHil)

Proof of Theorem rrxcph
Dummy variables 𝑓 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rrxval.r . . 3 𝐻 = (ℝ^‘𝐼)
21rrxval 23414 . 2 (𝐼𝑉𝐻 = (toℂHil‘(ℝfld freeLMod 𝐼)))
3 eqid 2774 . . 3 (toℂHil‘(ℝfld freeLMod 𝐼)) = (toℂHil‘(ℝfld freeLMod 𝐼))
4 eqid 2774 . . 3 (Base‘(ℝfld freeLMod 𝐼)) = (Base‘(ℝfld freeLMod 𝐼))
5 eqid 2774 . . 3 (Scalar‘(ℝfld freeLMod 𝐼)) = (Scalar‘(ℝfld freeLMod 𝐼))
6 eqid 2774 . . . 4 (ℝfld freeLMod 𝐼) = (ℝfld freeLMod 𝐼)
7 rebase 20189 . . . 4 ℝ = (Base‘ℝfld)
8 remulr 20194 . . . 4 · = (.r‘ℝfld)
9 eqid 2774 . . . 4 (·𝑖‘(ℝfld freeLMod 𝐼)) = (·𝑖‘(ℝfld freeLMod 𝐼))
10 eqid 2774 . . . 4 (0g‘(ℝfld freeLMod 𝐼)) = (0g‘(ℝfld freeLMod 𝐼))
11 re0g 20195 . . . 4 0 = (0g‘ℝfld)
12 refldcj 20203 . . . 4 ∗ = (*𝑟‘ℝfld)
13 refld 20202 . . . . 5 fld ∈ Field
1413a1i 11 . . . 4 (𝐼𝑉 → ℝfld ∈ Field)
15 fconstmpt 5315 . . . . 5 (𝐼 × {0}) = (𝑥𝐼 ↦ 0)
166, 7, 4frlmbasf 20341 . . . . . . . 8 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 𝑓:𝐼⟶ℝ)
1716ffnd 6197 . . . . . . 7 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 𝑓 Fn 𝐼)
18173adant3 1153 . . . . . 6 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → 𝑓 Fn 𝐼)
19 simpl 469 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 𝐼𝑉)
2013a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → ℝfld ∈ Field)
21 simpr 472 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)))
226, 7, 8, 4, 9frlmipval 20355 . . . . . . . . . . . . . . . . 17 (((𝐼𝑉 ∧ ℝfld ∈ Field) ∧ (𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ 𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)))) → (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓𝑓 · 𝑓)))
2319, 20, 21, 21, 22syl22anc 856 . . . . . . . . . . . . . . . 16 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = (ℝfld Σg (𝑓𝑓 · 𝑓)))
24 ovexd 6846 . . . . . . . . . . . . . . . . . . 19 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥𝐼) → ((𝑓𝑥) · (𝑓𝑥)) ∈ V)
25 inidm 3978 . . . . . . . . . . . . . . . . . . . 20 (𝐼𝐼) = 𝐼
26 eqidd 2775 . . . . . . . . . . . . . . . . . . . 20 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥𝐼) → (𝑓𝑥) = (𝑓𝑥))
2717, 17, 19, 19, 25, 26, 26offval 7072 . . . . . . . . . . . . . . . . . . 19 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓𝑓 · 𝑓) = (𝑥𝐼 ↦ ((𝑓𝑥) · (𝑓𝑥))))
2817, 17, 19, 19, 25, 26, 26ofval 7074 . . . . . . . . . . . . . . . . . . . 20 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥𝐼) → ((𝑓𝑓 · 𝑓)‘𝑥) = ((𝑓𝑥) · (𝑓𝑥)))
2916ffvelrnda 6519 . . . . . . . . . . . . . . . . . . . . 21 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ ℝ)
3029, 29remulcld 10293 . . . . . . . . . . . . . . . . . . . 20 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥𝐼) → ((𝑓𝑥) · (𝑓𝑥)) ∈ ℝ)
3128, 30eqeltrd 2853 . . . . . . . . . . . . . . . . . . 19 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥𝐼) → ((𝑓𝑓 · 𝑓)‘𝑥) ∈ ℝ)
3224, 27, 31fmpt2d 6553 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓𝑓 · 𝑓):𝐼⟶ℝ)
33 ovexd 6846 . . . . . . . . . . . . . . . . . . 19 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓𝑓 · 𝑓) ∈ V)
3432ffund 6200 . . . . . . . . . . . . . . . . . . 19 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → Fun (𝑓𝑓 · 𝑓))
356, 11, 4frlmbasfsupp 20339 . . . . . . . . . . . . . . . . . . 19 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 𝑓 finSupp 0)
36 0red 10264 . . . . . . . . . . . . . . . . . . . 20 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 0 ∈ ℝ)
37 simpr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
3837recnd 10291 . . . . . . . . . . . . . . . . . . . . 21 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
3938mul02d 10457 . . . . . . . . . . . . . . . . . . . 20 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
4019, 36, 16, 16, 39suppofss1d 7505 . . . . . . . . . . . . . . . . . . 19 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → ((𝑓𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0))
41 fsuppsssupp 8468 . . . . . . . . . . . . . . . . . . 19 ((((𝑓𝑓 · 𝑓) ∈ V ∧ Fun (𝑓𝑓 · 𝑓)) ∧ (𝑓 finSupp 0 ∧ ((𝑓𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0))) → (𝑓𝑓 · 𝑓) finSupp 0)
4233, 34, 35, 40, 41syl22anc 856 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓𝑓 · 𝑓) finSupp 0)
43 regsumsupp 20205 . . . . . . . . . . . . . . . . . 18 (((𝑓𝑓 · 𝑓):𝐼⟶ℝ ∧ (𝑓𝑓 · 𝑓) finSupp 0 ∧ 𝐼𝑉) → (ℝfld Σg (𝑓𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑓 · 𝑓)‘𝑥))
4432, 42, 19, 43syl3anc 1480 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (ℝfld Σg (𝑓𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑓 · 𝑓)‘𝑥))
45 suppssdm 7480 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 supp 0) ⊆ dom 𝑓
4645, 16fssdm 6212 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓 supp 0) ⊆ 𝐼)
4740, 46sstrd 3768 . . . . . . . . . . . . . . . . . . . 20 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → ((𝑓𝑓 · 𝑓) supp 0) ⊆ 𝐼)
4847sselda 3758 . . . . . . . . . . . . . . . . . . 19 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → 𝑥𝐼)
4948, 28syldan 580 . . . . . . . . . . . . . . . . . 18 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → ((𝑓𝑓 · 𝑓)‘𝑥) = ((𝑓𝑥) · (𝑓𝑥)))
5049sumeq2dv 14663 . . . . . . . . . . . . . . . . 17 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑓 · 𝑓)‘𝑥) = Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)))
5144, 50eqtrd 2808 . . . . . . . . . . . . . . . 16 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (ℝfld Σg (𝑓𝑓 · 𝑓)) = Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)))
5223, 51eqtrd 2808 . . . . . . . . . . . . . . 15 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)))
53523adant3 1153 . . . . . . . . . . . . . 14 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)))
54 simp3 1159 . . . . . . . . . . . . . 14 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0)
5553, 54eqtr3d 2810 . . . . . . . . . . . . 13 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)) = 0)
5635fsuppimpd 8459 . . . . . . . . . . . . . . . 16 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑓 supp 0) ∈ Fin)
57 ssfi 8357 . . . . . . . . . . . . . . . 16 (((𝑓 supp 0) ∈ Fin ∧ ((𝑓𝑓 · 𝑓) supp 0) ⊆ (𝑓 supp 0)) → ((𝑓𝑓 · 𝑓) supp 0) ∈ Fin)
5856, 40, 57syl2anc 574 . . . . . . . . . . . . . . 15 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → ((𝑓𝑓 · 𝑓) supp 0) ∈ Fin)
5948, 30syldan 580 . . . . . . . . . . . . . . 15 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → ((𝑓𝑥) · (𝑓𝑥)) ∈ ℝ)
6029msqge0d 10819 . . . . . . . . . . . . . . . 16 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥) · (𝑓𝑥)))
6148, 60syldan 580 . . . . . . . . . . . . . . 15 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → 0 ≤ ((𝑓𝑥) · (𝑓𝑥)))
6258, 59, 61fsum00 14759 . . . . . . . . . . . . . 14 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)) = 0))
63623adant3 1153 . . . . . . . . . . . . 13 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → (Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)) = 0 ↔ ∀𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)) = 0))
6455, 63mpbid 223 . . . . . . . . . . . 12 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → ∀𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)) = 0)
6564r19.21bi 3084 . . . . . . . . . . 11 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → ((𝑓𝑥) · (𝑓𝑥)) = 0)
6665adantlr 695 . . . . . . . . . 10 ((((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → ((𝑓𝑥) · (𝑓𝑥)) = 0)
67293adantl3 1200 . . . . . . . . . . . . 13 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ ℝ)
6867recnd 10291 . . . . . . . . . . . 12 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ ℂ)
6968, 68mul0ord 10900 . . . . . . . . . . 11 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (((𝑓𝑥) · (𝑓𝑥)) = 0 ↔ ((𝑓𝑥) = 0 ∨ (𝑓𝑥) = 0)))
7069adantr 467 . . . . . . . . . 10 ((((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → (((𝑓𝑥) · (𝑓𝑥)) = 0 ↔ ((𝑓𝑥) = 0 ∨ (𝑓𝑥) = 0)))
7166, 70mpbid 223 . . . . . . . . 9 ((((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → ((𝑓𝑥) = 0 ∨ (𝑓𝑥) = 0))
72 oridm 917 . . . . . . . . 9 (((𝑓𝑥) = 0 ∨ (𝑓𝑥) = 0) ↔ (𝑓𝑥) = 0)
7371, 72sylib 209 . . . . . . . 8 ((((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) ∧ 𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)) → (𝑓𝑥) = 0)
74323adant3 1153 . . . . . . . . . . 11 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → (𝑓𝑓 · 𝑓):𝐼⟶ℝ)
7574adantr 467 . . . . . . . . . 10 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (𝑓𝑓 · 𝑓):𝐼⟶ℝ)
76 ssid 3780 . . . . . . . . . . 11 ((𝑓𝑓 · 𝑓) supp 0) ⊆ ((𝑓𝑓 · 𝑓) supp 0)
7776a1i 11 . . . . . . . . . 10 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → ((𝑓𝑓 · 𝑓) supp 0) ⊆ ((𝑓𝑓 · 𝑓) supp 0))
78 simpl1 1233 . . . . . . . . . 10 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → 𝐼𝑉)
79 0red 10264 . . . . . . . . . 10 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → 0 ∈ ℝ)
8075, 77, 78, 79suppssr 7499 . . . . . . . . 9 ((((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))) → ((𝑓𝑓 · 𝑓)‘𝑥) = 0)
81283adantl3 1200 . . . . . . . . . . . . 13 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → ((𝑓𝑓 · 𝑓)‘𝑥) = ((𝑓𝑥) · (𝑓𝑥)))
8281eqeq1d 2776 . . . . . . . . . . . 12 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (((𝑓𝑓 · 𝑓)‘𝑥) = 0 ↔ ((𝑓𝑥) · (𝑓𝑥)) = 0))
8382, 69bitrd 269 . . . . . . . . . . 11 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (((𝑓𝑓 · 𝑓)‘𝑥) = 0 ↔ ((𝑓𝑥) = 0 ∨ (𝑓𝑥) = 0)))
8483, 72syl6bb 277 . . . . . . . . . 10 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (((𝑓𝑓 · 𝑓)‘𝑥) = 0 ↔ (𝑓𝑥) = 0))
8584biimpa 463 . . . . . . . . 9 ((((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) ∧ ((𝑓𝑓 · 𝑓)‘𝑥) = 0) → (𝑓𝑥) = 0)
8680, 85syldan 580 . . . . . . . 8 ((((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) ∧ 𝑥 ∈ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))) → (𝑓𝑥) = 0)
87 undif 4201 . . . . . . . . . . . . 13 (((𝑓𝑓 · 𝑓) supp 0) ⊆ 𝐼 ↔ (((𝑓𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))) = 𝐼)
8847, 87sylib 209 . . . . . . . . . . . 12 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (((𝑓𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))) = 𝐼)
8988eleq2d 2839 . . . . . . . . . . 11 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → (𝑥 ∈ (((𝑓𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))) ↔ 𝑥𝐼))
90893adant3 1153 . . . . . . . . . 10 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → (𝑥 ∈ (((𝑓𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))) ↔ 𝑥𝐼))
9190biimpar 464 . . . . . . . . 9 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → 𝑥 ∈ (((𝑓𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))))
92 elun 3911 . . . . . . . . 9 (𝑥 ∈ (((𝑓𝑓 · 𝑓) supp 0) ∪ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))) ↔ (𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))))
9391, 92sylib 209 . . . . . . . 8 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0) ∨ 𝑥 ∈ (𝐼 ∖ ((𝑓𝑓 · 𝑓) supp 0))))
9473, 86, 93mpjaodan 970 . . . . . . 7 (((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) ∧ 𝑥𝐼) → (𝑓𝑥) = 0)
9594ralrimiva 3118 . . . . . 6 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → ∀𝑥𝐼 (𝑓𝑥) = 0)
96 fconstfv 6639 . . . . . . 7 (𝑓:𝐼⟶{0} ↔ (𝑓 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑓𝑥) = 0))
97 c0ex 10257 . . . . . . . 8 0 ∈ V
9897fconst2 6633 . . . . . . 7 (𝑓:𝐼⟶{0} ↔ 𝑓 = (𝐼 × {0}))
9996, 98sylbb1 228 . . . . . 6 ((𝑓 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑓𝑥) = 0) → 𝑓 = (𝐼 × {0}))
10018, 95, 99syl2anc 574 . . . . 5 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (𝐼 × {0}))
101 isfld 18986 . . . . . . . . . . 11 (ℝfld ∈ Field ↔ (ℝfld ∈ DivRing ∧ ℝfld ∈ CRing))
10213, 101mpbi 221 . . . . . . . . . 10 (ℝfld ∈ DivRing ∧ ℝfld ∈ CRing)
103102simpli 471 . . . . . . . . 9 fld ∈ DivRing
104 drngring 18984 . . . . . . . . 9 (ℝfld ∈ DivRing → ℝfld ∈ Ring)
105103, 104ax-mp 5 . . . . . . . 8 fld ∈ Ring
1066, 11frlm0 20335 . . . . . . . 8 ((ℝfld ∈ Ring ∧ 𝐼𝑉) → (𝐼 × {0}) = (0g‘(ℝfld freeLMod 𝐼)))
107105, 106mpan 671 . . . . . . 7 (𝐼𝑉 → (𝐼 × {0}) = (0g‘(ℝfld freeLMod 𝐼)))
10815, 107syl5reqr 2823 . . . . . 6 (𝐼𝑉 → (0g‘(ℝfld freeLMod 𝐼)) = (𝑥𝐼 ↦ 0))
1091083ad2ant1 1154 . . . . 5 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → (0g‘(ℝfld freeLMod 𝐼)) = (𝑥𝐼 ↦ 0))
11015, 100, 1093eqtr4a 2834 . . . 4 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼)) ∧ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓) = 0) → 𝑓 = (0g‘(ℝfld freeLMod 𝐼)))
111 cjre 14109 . . . . 5 (𝑥 ∈ ℝ → (∗‘𝑥) = 𝑥)
112111adantl 468 . . . 4 ((𝐼𝑉𝑥 ∈ ℝ) → (∗‘𝑥) = 𝑥)
113 id 22 . . . 4 (𝐼𝑉𝐼𝑉)
1146, 7, 8, 4, 9, 10, 11, 12, 14, 110, 112, 113frlmphl 20357 . . 3 (𝐼𝑉 → (ℝfld freeLMod 𝐼) ∈ PreHil)
115 df-refld 20188 . . . 4 fld = (ℂflds ℝ)
1166frlmsca 20334 . . . . 5 ((ℝfld ∈ Field ∧ 𝐼𝑉) → ℝfld = (Scalar‘(ℝfld freeLMod 𝐼)))
11713, 116mpan 671 . . . 4 (𝐼𝑉 → ℝfld = (Scalar‘(ℝfld freeLMod 𝐼)))
118115, 117syl5reqr 2823 . . 3 (𝐼𝑉 → (Scalar‘(ℝfld freeLMod 𝐼)) = (ℂflds ℝ))
119 simpr1 1239 . . . 4 ((𝐼𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 𝑓 ∈ ℝ)
120 simpr3 1243 . . . 4 ((𝐼𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → 0 ≤ 𝑓)
121119, 120resqrtcld 14386 . . 3 ((𝐼𝑉 ∧ (𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓)) → (√‘𝑓) ∈ ℝ)
12258, 59, 61fsumge0 14756 . . . . 5 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 0 ≤ Σ𝑥 ∈ ((𝑓𝑓 · 𝑓) supp 0)((𝑓𝑥) · (𝑓𝑥)))
123122, 51breqtrrd 4825 . . . 4 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 0 ≤ (ℝfld Σg (𝑓𝑓 · 𝑓)))
124123, 23breqtrrd 4825 . . 3 ((𝐼𝑉𝑓 ∈ (Base‘(ℝfld freeLMod 𝐼))) → 0 ≤ (𝑓(·𝑖‘(ℝfld freeLMod 𝐼))𝑓))
1253, 4, 5, 114, 118, 9, 121, 124tchcph 23275 . 2 (𝐼𝑉 → (toℂHil‘(ℝfld freeLMod 𝐼)) ∈ ℂPreHil)
1262, 125eqeltrd 2853 1 (𝐼𝑉𝐻 ∈ ℂPreHil)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383  wo 863  w3a 1098   = wceq 1634  wcel 2148  wral 3064  Vcvv 3355  cdif 3726  cun 3727  wss 3729  {csn 4326   class class class wbr 4797  cmpt 4876   × cxp 5261  Fun wfun 6036   Fn wfn 6037  wf 6038  cfv 6042  (class class class)co 6812  𝑓 cof 7063   supp csupp 7467  Fincfn 8130   finSupp cfsupp 8452  cr 10158  0cc0 10159   · cmul 10164  cle 10298  ccj 14066  Σcsu 14646  Basecbs 16084  s cress 16085  Scalarcsca 16172  ·𝑖cip 16174  0gc0g 16328   Σg cgsu 16329  Ringcrg 18775  CRingccrg 18776  DivRingcdr 18977  Fieldcfield 18978  fldccnfld 19981  fldcrefld 20187   freeLMod cfrlm 20327  ℂPreHilccph 23205  toℂHilctch 23206  ℝ^crrx 23410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-inf2 8723  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237  ax-addf 10238  ax-mulf 10239
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-fal 1640  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-of 7065  df-om 7234  df-1st 7336  df-2nd 7337  df-supp 7468  df-tpos 7525  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-oadd 7738  df-er 7917  df-map 8032  df-ixp 8084  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-fsupp 8453  df-sup 8525  df-inf 8526  df-oi 8592  df-card 8986  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-4 11304  df-5 11305  df-6 11306  df-7 11307  df-8 11308  df-9 11309  df-n0 11517  df-z 11602  df-dec 11718  df-uz 11911  df-q 12014  df-rp 12053  df-xneg 12168  df-xadd 12169  df-xmul 12170  df-ico 12405  df-fz 12556  df-fzo 12696  df-seq 13031  df-exp 13090  df-hash 13344  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-clim 14449  df-sum 14647  df-struct 16086  df-ndx 16087  df-slot 16088  df-base 16090  df-sets 16091  df-ress 16092  df-plusg 16182  df-mulr 16183  df-starv 16184  df-sca 16185  df-vsca 16186  df-ip 16187  df-tset 16188  df-ple 16189  df-ds 16192  df-unif 16193  df-hom 16194  df-cco 16195  df-rest 16311  df-topn 16312  df-0g 16330  df-gsum 16331  df-topgen 16332  df-prds 16336  df-pws 16338  df-mgm 17470  df-sgrp 17512  df-mnd 17523  df-mhm 17563  df-submnd 17564  df-grp 17653  df-minusg 17654  df-sbg 17655  df-subg 17819  df-ghm 17886  df-cntz 17977  df-cmn 18422  df-abl 18423  df-mgp 18718  df-ur 18730  df-ring 18777  df-cring 18778  df-oppr 18851  df-dvdsr 18869  df-unit 18870  df-invr 18900  df-dvr 18911  df-rnghom 18945  df-drng 18979  df-field 18980  df-subrg 19008  df-abv 19047  df-staf 19075  df-srng 19076  df-lmod 19095  df-lss 19163  df-lmhm 19255  df-lvec 19336  df-sra 19407  df-rgmod 19408  df-psmet 19973  df-xmet 19974  df-met 19975  df-bl 19976  df-mopn 19977  df-cnfld 19982  df-refld 20188  df-phl 20208  df-dsmm 20313  df-frlm 20328  df-top 20939  df-topon 20956  df-topsp 20978  df-bases 20991  df-xms 22365  df-ms 22366  df-nm 22627  df-ngp 22628  df-tng 22629  df-nrg 22630  df-nlm 22631  df-clm 23102  df-cph 23207  df-tch 23208  df-rrx 23412
This theorem is referenced by:  rrxngp  41025
  Copyright terms: Public domain W3C validator