# 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 ${⊢}{H}={{I}}^{}$
rrxbase.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
Assertion rrxcph ${⊢}{I}\in {V}\to {H}\in \mathrm{CPreHil}$

### Proof

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