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 ffvelrnda ( ( ( 𝐼𝑉𝑓 ∈ ( 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 = ( ℂflds ℝ )
115 113 114 eqtr3di ( 𝐼𝑉 → ( Scalar ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ℂflds ℝ ) )
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 )