Metamath Proof Explorer

Theorem rrxcph

Description: Generalized Euclidean real spaces are subcomplex pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019) (Proof shortened by AV, 22-Jul-2019)

Ref Expression
Hypotheses rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion rrxcph ( 𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil )

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 rrxbase.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
3 1 rrxval ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
4 eqid ⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
5 eqid ⊢ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Base ‘ ( ℝfld freeLMod 𝐼 ) )
6 eqid ⊢ ( Scalar ‘ ( ℝfld freeLMod 𝐼 ) ) = ( Scalar ‘ ( ℝfld freeLMod 𝐼 ) )
7 eqid ⊢ ( ℝfld freeLMod 𝐼 ) = ( ℝfld freeLMod 𝐼 )
8 rebase ⊢ ℝ = ( Base ‘ ℝfld )
9 remulr ⊢ · = ( .r ‘ ℝfld )
10 eqid ⊢ ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) )
11 eqid ⊢ ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 0g ‘ ( ℝfld freeLMod 𝐼 ) )
12 re0g ⊢ 0 = ( 0g ‘ ℝfld )
13 refldcj ⊢ ∗ = ( *𝑟 ‘ ℝfld )
14 refld ⊢ ℝfld ∈ Field
15 14 a1i ⊢ ( 𝐼 ∈ 𝑉 → ℝfld ∈ Field )
16 fconstmpt ⊢ ( 𝐼 × { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ 0 )
17 7 8 5 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 𝑓 : 𝐼 ⟶ ℝ )
18 17 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 𝑓 Fn 𝐼 )
19 18 3adant3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → 𝑓 Fn 𝐼 )
20 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 𝐼 ∈ 𝑉 )
21 14 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ℝfld ∈ Field )
22 simpr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) )
23 7 8 9 5 10 frlmipval ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ ℝfld ∈ Field ) ∧ ( 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ) → ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = ( ℝfld Σg ( 𝑓 ∘f · 𝑓 ) ) )
24 20 21 22 22 23 syl22anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = ( ℝfld Σg ( 𝑓 ∘f · 𝑓 ) ) )
25 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
26 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
27 18 18 20 20 25 26 26 offval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 ∘f · 𝑓 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) )
28 17 ffvelcdmda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
29 28 28 remulcld ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ∈ ℝ )
30 27 29 fmpt3d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 ∘f · 𝑓 ) : 𝐼 ⟶ ℝ )
31 ovexd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 ∘f · 𝑓 ) ∈ V )
32 30 ffund ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → Fun ( 𝑓 ∘f · 𝑓 ) )
33 7 12 5 frlmbasfsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 𝑓 finSupp 0 )
34 0red ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 0 ∈ ℝ )
35 simpr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
36 35 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
37 36 mul02d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 0 · 𝑥 ) = 0 )
38 20 34 17 17 37 suppofss1d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ⊆ ( 𝑓 supp 0 ) )
39 fsuppsssupp ⊢ ( ( ( ( 𝑓 ∘f · 𝑓 ) ∈ V ∧ Fun ( 𝑓 ∘f · 𝑓 ) ) ∧ ( 𝑓 finSupp 0 ∧ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ⊆ ( 𝑓 supp 0 ) ) ) → ( 𝑓 ∘f · 𝑓 ) finSupp 0 )
40 31 32 33 38 39 syl22anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 ∘f · 𝑓 ) finSupp 0 )
41 regsumsupp ⊢ ( ( ( 𝑓 ∘f · 𝑓 ) : 𝐼 ⟶ ℝ ∧ ( 𝑓 ∘f · 𝑓 ) finSupp 0 ∧ 𝐼 ∈ 𝑉 ) → ( ℝfld Σg ( 𝑓 ∘f · 𝑓 ) ) = Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) )
42 30 40 20 41 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( ℝfld Σg ( 𝑓 ∘f · 𝑓 ) ) = Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) )
43 suppssdm ⊢ ( 𝑓 supp 0 ) ⊆ dom 𝑓
44 43 17 fssdm ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 supp 0 ) ⊆ 𝐼 )
45 38 44 sstrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ⊆ 𝐼 )
46 45 sselda ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → 𝑥 ∈ 𝐼 )
47 18 18 20 20 25 26 26 ofval ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
48 46 47 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
49 48 sumeq2dv ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
50 42 49 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( ℝfld Σg ( 𝑓 ∘f · 𝑓 ) ) = Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
51 24 50 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
52 51 3adant3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
53 simp3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 )
54 52 53 eqtr3d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 )
55 33 fsuppimpd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑓 supp 0 ) ∈ Fin )
56 55 38 ssfid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∈ Fin )
57 46 29 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ∈ ℝ )
58 28 msqge0d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
59 46 58 syldan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → 0 ≤ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
60 56 57 59 fsum00 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 ↔ ∀ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 ) )
61 60 3adant3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ( Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 ↔ ∀ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 ) )
62 54 61 mpbid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ∀ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 )
63 62 r19.21bi ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 )
64 63 adantlr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 )
65 28 3adantl3 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
66 65 recnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
67 66 66 mul0ord ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 ↔ ( ( 𝑓 ‘ 𝑥 ) = 0 ∨ ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
68 67 adantr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → ( ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 ↔ ( ( 𝑓 ‘ 𝑥 ) = 0 ∨ ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
69 64 68 mpbid ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → ( ( 𝑓 ‘ 𝑥 ) = 0 ∨ ( 𝑓 ‘ 𝑥 ) = 0 ) )
70 oridm ⊢ ( ( ( 𝑓 ‘ 𝑥 ) = 0 ∨ ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( 𝑓 ‘ 𝑥 ) = 0 )
71 69 70 sylib ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) → ( 𝑓 ‘ 𝑥 ) = 0 )
72 30 3adant3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ( 𝑓 ∘f · 𝑓 ) : 𝐼 ⟶ ℝ )
73 72 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ∘f · 𝑓 ) : 𝐼 ⟶ ℝ )
74 ssidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ⊆ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) )
75 simpl1 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
76 0red ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ ℝ )
77 73 74 75 76 suppssr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) → ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = 0 )
78 47 3adantl3 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
79 78 eqeq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = 0 ) )
80 79 67 bitrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑓 ‘ 𝑥 ) = 0 ∨ ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
81 80 70 bitrdi ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = 0 ↔ ( 𝑓 ‘ 𝑥 ) = 0 ) )
82 81 biimpa ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ ( ( 𝑓 ∘f · 𝑓 ) ‘ 𝑥 ) = 0 ) → ( 𝑓 ‘ 𝑥 ) = 0 )
83 77 82 syldan ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) → ( 𝑓 ‘ 𝑥 ) = 0 )
84 undif ⊢ ( ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ⊆ 𝐼 ↔ ( ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∪ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) = 𝐼 )
85 45 84 sylib ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∪ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) = 𝐼 )
86 85 eleq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → ( 𝑥 ∈ ( ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∪ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) ↔ 𝑥 ∈ 𝐼 ) )
87 86 3adant3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ( 𝑥 ∈ ( ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∪ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) ↔ 𝑥 ∈ 𝐼 ) )
88 87 biimpar ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ ( ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∪ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) )
89 elun ⊢ ( 𝑥 ∈ ( ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∪ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) ↔ ( 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∨ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) )
90 88 89 sylib ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ∨ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ) ) )
91 71 83 90 mpjaodan ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) = 0 )
92 91 ralrimiva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) = 0 )
93 fconstfv ⊢ ( 𝑓 : 𝐼 ⟶ { 0 } ↔ ( 𝑓 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) = 0 ) )
94 c0ex ⊢ 0 ∈ V
95 94 fconst2 ⊢ ( 𝑓 : 𝐼 ⟶ { 0 } ↔ 𝑓 = ( 𝐼 × { 0 } ) )
96 93 95 sylbb1 ⊢ ( ( 𝑓 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) = 0 ) → 𝑓 = ( 𝐼 × { 0 } ) )
97 19 92 96 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → 𝑓 = ( 𝐼 × { 0 } ) )
98 isfld ⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
99 14 98 mpbi ⊢ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing )
100 99 simpli ⊢ ℝfld ∈ DivRing
101 drngring ⊢ ( ℝfld ∈ DivRing → ℝfld ∈ Ring )
102 100 101 ax-mp ⊢ ℝfld ∈ Ring
103 7 12 frlm0 ⊢ ( ( ℝfld ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) )
104 102 103 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) )
105 104 16 eqtr3di ⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) )
106 105 3ad2ant1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) = ( 𝑥 ∈ 𝐼 ↦ 0 ) )
107 16 97 106 3eqtr4a ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ∧ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) = 0 ) → 𝑓 = ( 0g ‘ ( ℝfld freeLMod 𝐼 ) ) )
108 cjre ⊢ ( 𝑥 ∈ ℝ → ( ∗ ‘ 𝑥 ) = 𝑥 )
109 108 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ℝ ) → ( ∗ ‘ 𝑥 ) = 𝑥 )
110 id ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉 )
111 7 8 9 5 10 11 12 13 15 107 109 110 frlmphl ⊢ ( 𝐼 ∈ 𝑉 → ( ℝfld freeLMod 𝐼 ) ∈ PreHil )
112 7 frlmsca ⊢ ( ( ℝfld ∈ Field ∧ 𝐼 ∈ 𝑉 ) → ℝfld = ( Scalar ‘ ( ℝfld freeLMod 𝐼 ) ) )
113 14 112 mpan ⊢ ( 𝐼 ∈ 𝑉 → ℝfld = ( Scalar ‘ ( ℝfld freeLMod 𝐼 ) ) )
114 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
115 113 114 eqtr3di ⊢ ( 𝐼 ∈ 𝑉 → ( Scalar ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ℂfld ↾s ℝ ) )
116 simpr1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓 ) ) → 𝑓 ∈ ℝ )
117 simpr3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓 ) ) → 0 ≤ 𝑓 )
118 116 117 resqrtcld ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑓 ∈ ℝ ∧ 𝑓 ∈ ℝ ∧ 0 ≤ 𝑓 ) ) → ( √ ‘ 𝑓 ) ∈ ℝ )
119 56 57 59 fsumge0 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 0 ≤ Σ 𝑥 ∈ ( ( 𝑓 ∘f · 𝑓 ) supp 0 ) ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
120 119 50 breqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 0 ≤ ( ℝfld Σg ( 𝑓 ∘f · 𝑓 ) ) )
121 120 24 breqtrrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ ( ℝfld freeLMod 𝐼 ) ) ) → 0 ≤ ( 𝑓 ( ·𝑖 ‘ ( ℝfld freeLMod 𝐼 ) ) 𝑓 ) )
122 4 5 6 111 115 10 118 121 tcphcph ⊢ ( 𝐼 ∈ 𝑉 → ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ∈ ℂPreHil )
123 3 122 eqeltrd ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil )