Metamath Proof Explorer

Theorem tcphcph

Description: The standard definition of a norm turns any pre-Hilbert space over a subfield of CCfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses tcphval.n ${⊢}{G}=\mathrm{toCPreHil}\left({W}\right)$
tcphcph.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
tcphcph.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
tcphcph.1 ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$
tcphcph.2 ${⊢}{\phi }\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}$
tcphcph.h
tcphcph.3 ${⊢}\left({\phi }\wedge \left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to \sqrt{{x}}\in {K}$
tcphcph.4
Assertion tcphcph ${⊢}{\phi }\to {G}\in \mathrm{CPreHil}$

Proof

Step Hyp Ref Expression
1 tcphval.n ${⊢}{G}=\mathrm{toCPreHil}\left({W}\right)$
2 tcphcph.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
3 tcphcph.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
4 tcphcph.1 ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$
5 tcphcph.2 ${⊢}{\phi }\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}$
6 tcphcph.h
7 tcphcph.3 ${⊢}\left({\phi }\wedge \left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to \sqrt{{x}}\in {K}$
8 tcphcph.4
9 1 tcphphl ${⊢}{W}\in \mathrm{PreHil}↔{G}\in \mathrm{PreHil}$
10 4 9 sylib ${⊢}{\phi }\to {G}\in \mathrm{PreHil}$
11 1 2 6 tcphval
12 eqid ${⊢}{-}_{{W}}={-}_{{W}}$
13 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
14 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
15 4 14 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
16 lmodgrp ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$
17 15 16 syl ${⊢}{\phi }\to {W}\in \mathrm{Grp}$
18 1 2 3 4 5 6 tcphcphlem3
19 18 8 resqrtcld
20 19 fmpttd
21 oveq12
22 21 anidms
23 22 fveq2d
24 eqid
25 fvex
26 23 24 25 fvmpt3i
28 27 eqeq1d
29 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
30 phllvec ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LVec}$
31 4 30 syl ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
32 3 lvecdrng ${⊢}{W}\in \mathrm{LVec}\to {F}\in \mathrm{DivRing}$
33 31 32 syl ${⊢}{\phi }\to {F}\in \mathrm{DivRing}$
34 29 5 33 cphsubrglem ${⊢}{\phi }\to \left({F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\wedge {\mathrm{Base}}_{{F}}={K}\cap ℂ\wedge {\mathrm{Base}}_{{F}}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$
35 34 simp2d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={K}\cap ℂ$
36 inss2 ${⊢}{K}\cap ℂ\subseteq ℂ$
37 35 36 eqsstrdi ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}\subseteq ℂ$
38 37 adantr ${⊢}\left({\phi }\wedge {y}\in {V}\right)\to {\mathrm{Base}}_{{F}}\subseteq ℂ$
39 3 6 2 29 ipcl
40 39 3anidm23
41 4 40 sylan
42 38 41 sseldd
43 42 sqrtcld
44 sqeq0
45 43 44 syl
46 42 sqsqrtd
47 1 2 3 4 5 phclm ${⊢}{\phi }\to {W}\in \mathrm{CMod}$
48 3 clm0 ${⊢}{W}\in \mathrm{CMod}\to 0={0}_{{F}}$
49 47 48 syl ${⊢}{\phi }\to 0={0}_{{F}}$
50 49 adantr ${⊢}\left({\phi }\wedge {y}\in {V}\right)\to 0={0}_{{F}}$
51 46 50 eqeq12d
52 45 51 bitr3d
53 eqid ${⊢}{0}_{{F}}={0}_{{F}}$
54 3 6 2 53 13 ipeq0
55 4 54 sylan
56 28 52 55 3bitrd
57 4 adantr ${⊢}\left({\phi }\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {W}\in \mathrm{PreHil}$
58 34 simp1d ${⊢}{\phi }\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}$
59 58 adantr ${⊢}\left({\phi }\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}$
60 3anass ${⊢}\left({x}\in {\mathrm{Base}}_{{F}}\wedge {x}\in ℝ\wedge 0\le {x}\right)↔\left({x}\in {\mathrm{Base}}_{{F}}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)$
61 simpr2 ${⊢}\left({\phi }\wedge \left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to {x}\in ℝ$
62 61 recnd ${⊢}\left({\phi }\wedge \left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to {x}\in ℂ$
63 62 sqrtcld ${⊢}\left({\phi }\wedge \left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to \sqrt{{x}}\in ℂ$
64 7 63 jca ${⊢}\left({\phi }\wedge \left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to \left(\sqrt{{x}}\in {K}\wedge \sqrt{{x}}\in ℂ\right)$
65 64 ex ${⊢}{\phi }\to \left(\left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\to \left(\sqrt{{x}}\in {K}\wedge \sqrt{{x}}\in ℂ\right)\right)$
66 35 eleq2d ${⊢}{\phi }\to \left({x}\in {\mathrm{Base}}_{{F}}↔{x}\in \left({K}\cap ℂ\right)\right)$
67 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
68 elin ${⊢}{x}\in \left({K}\cap ℂ\right)↔\left({x}\in {K}\wedge {x}\in ℂ\right)$
69 68 rbaib ${⊢}{x}\in ℂ\to \left({x}\in \left({K}\cap ℂ\right)↔{x}\in {K}\right)$
70 67 69 syl ${⊢}{x}\in ℝ\to \left({x}\in \left({K}\cap ℂ\right)↔{x}\in {K}\right)$
71 66 70 sylan9bb ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({x}\in {\mathrm{Base}}_{{F}}↔{x}\in {K}\right)$
72 71 adantrr ${⊢}\left({\phi }\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)\to \left({x}\in {\mathrm{Base}}_{{F}}↔{x}\in {K}\right)$
73 72 ex ${⊢}{\phi }\to \left(\left({x}\in ℝ\wedge 0\le {x}\right)\to \left({x}\in {\mathrm{Base}}_{{F}}↔{x}\in {K}\right)\right)$
74 73 pm5.32rd ${⊢}{\phi }\to \left(\left({x}\in {\mathrm{Base}}_{{F}}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)↔\left({x}\in {K}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)\right)$
75 3anass ${⊢}\left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)↔\left({x}\in {K}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)$
76 74 75 syl6bbr ${⊢}{\phi }\to \left(\left({x}\in {\mathrm{Base}}_{{F}}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)↔\left({x}\in {K}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)$
77 35 eleq2d ${⊢}{\phi }\to \left(\sqrt{{x}}\in {\mathrm{Base}}_{{F}}↔\sqrt{{x}}\in \left({K}\cap ℂ\right)\right)$
78 elin ${⊢}\sqrt{{x}}\in \left({K}\cap ℂ\right)↔\left(\sqrt{{x}}\in {K}\wedge \sqrt{{x}}\in ℂ\right)$
79 77 78 syl6bb ${⊢}{\phi }\to \left(\sqrt{{x}}\in {\mathrm{Base}}_{{F}}↔\left(\sqrt{{x}}\in {K}\wedge \sqrt{{x}}\in ℂ\right)\right)$
80 65 76 79 3imtr4d ${⊢}{\phi }\to \left(\left({x}\in {\mathrm{Base}}_{{F}}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)\to \sqrt{{x}}\in {\mathrm{Base}}_{{F}}\right)$
81 60 80 syl5bi ${⊢}{\phi }\to \left(\left({x}\in {\mathrm{Base}}_{{F}}\wedge {x}\in ℝ\wedge 0\le {x}\right)\to \sqrt{{x}}\in {\mathrm{Base}}_{{F}}\right)$
82 81 imp ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{F}}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to \sqrt{{x}}\in {\mathrm{Base}}_{{F}}$
83 82 adantlr ${⊢}\left(\left({\phi }\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\wedge \left({x}\in {\mathrm{Base}}_{{F}}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to \sqrt{{x}}\in {\mathrm{Base}}_{{F}}$
85 simprl ${⊢}\left({\phi }\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {y}\in {V}$
86 simprr ${⊢}\left({\phi }\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {z}\in {V}$
87 1 2 3 57 59 6 83 84 29 12 85 86 tcphcphlem1
88 2 12 grpsubcl ${⊢}\left({W}\in \mathrm{Grp}\wedge {y}\in {V}\wedge {z}\in {V}\right)\to {y}{-}_{{W}}{z}\in {V}$
89 88 3expb ${⊢}\left({W}\in \mathrm{Grp}\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {y}{-}_{{W}}{z}\in {V}$
90 17 89 sylan ${⊢}\left({\phi }\wedge \left({y}\in {V}\wedge {z}\in {V}\right)\right)\to {y}{-}_{{W}}{z}\in {V}$
91 oveq12
92 91 anidms
93 92 fveq2d
94 93 24 25 fvmpt3i
95 90 94 syl
96 oveq12
97 96 anidms
98 97 fveq2d
99 98 24 25 fvmpt3i
100 26 99 oveqan12d
102 87 95 101 3brtr4d
103 11 2 12 13 17 20 56 102 tngngpd ${⊢}{\phi }\to {G}\in \mathrm{NrmGrp}$
104 phllmod ${⊢}{G}\in \mathrm{PreHil}\to {G}\in \mathrm{LMod}$
105 10 104 syl ${⊢}{\phi }\to {G}\in \mathrm{LMod}$
106 cnnrg ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{NrmRing}$
107 34 simp3d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
108 eqid ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}$
109 108 subrgnrg ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{NrmRing}\wedge {\mathrm{Base}}_{{F}}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\in \mathrm{NrmRing}$
110 106 107 109 sylancr ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\in \mathrm{NrmRing}$
111 58 110 eqeltrd ${⊢}{\phi }\to {F}\in \mathrm{NrmRing}$
112 103 105 111 3jca ${⊢}{\phi }\to \left({G}\in \mathrm{NrmGrp}\wedge {G}\in \mathrm{LMod}\wedge {F}\in \mathrm{NrmRing}\right)$
113 4 adantr ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to {W}\in \mathrm{PreHil}$
114 58 adantr ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}$
115 82 adantlr ${⊢}\left(\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\wedge \left({x}\in {\mathrm{Base}}_{{F}}\wedge {x}\in ℝ\wedge 0\le {x}\right)\right)\to \sqrt{{x}}\in {\mathrm{Base}}_{{F}}$
117 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
118 simprl ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to {y}\in {\mathrm{Base}}_{{F}}$
119 simprr ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to {z}\in {V}$
120 1 2 3 113 114 6 115 116 29 117 118 119 tcphcphlem2
121 2 3 117 29 lmodvscl ${⊢}\left({W}\in \mathrm{LMod}\wedge {y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\to {y}{\cdot }_{{W}}{z}\in {V}$
122 121 3expb ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to {y}{\cdot }_{{W}}{z}\in {V}$
123 15 122 sylan ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to {y}{\cdot }_{{W}}{z}\in {V}$
124 eqid ${⊢}\mathrm{norm}\left({G}\right)=\mathrm{norm}\left({G}\right)$
125 1 124 2 6 tcphnmval
126 17 123 125 syl2an2r
127 114 fveq2d ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to \mathrm{norm}\left({F}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)$
128 127 fveq1d ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to \mathrm{norm}\left({F}\right)\left({y}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)\left({y}\right)$
129 subrgsubg ${⊢}{\mathrm{Base}}_{{F}}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to {\mathrm{Base}}_{{F}}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
130 107 129 syl ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
131 cnfldnm ${⊢}\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$
132 eqid ${⊢}\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)$
133 108 131 132 subgnm2 ${⊢}\left({\mathrm{Base}}_{{F}}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge {y}\in {\mathrm{Base}}_{{F}}\right)\to \mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)\left({y}\right)=\left|{y}\right|$
134 130 118 133 syl2an2r ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to \mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)\left({y}\right)=\left|{y}\right|$
135 128 134 eqtrd ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to \mathrm{norm}\left({F}\right)\left({y}\right)=\left|{y}\right|$
136 1 124 2 6 tcphnmval
137 17 119 136 syl2an2r
138 135 137 oveq12d
139 120 126 138 3eqtr4d ${⊢}\left({\phi }\wedge \left({y}\in {\mathrm{Base}}_{{F}}\wedge {z}\in {V}\right)\right)\to \mathrm{norm}\left({G}\right)\left({y}{\cdot }_{{W}}{z}\right)=\mathrm{norm}\left({F}\right)\left({y}\right)\mathrm{norm}\left({G}\right)\left({z}\right)$
140 139 ralrimivva ${⊢}{\phi }\to \forall {y}\in {\mathrm{Base}}_{{F}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\mathrm{norm}\left({G}\right)\left({y}{\cdot }_{{W}}{z}\right)=\mathrm{norm}\left({F}\right)\left({y}\right)\mathrm{norm}\left({G}\right)\left({z}\right)$
141 1 2 tcphbas ${⊢}{V}={\mathrm{Base}}_{{G}}$
142 1 117 tcphvsca ${⊢}{\cdot }_{{W}}={\cdot }_{{G}}$
143 1 3 tcphsca ${⊢}{F}=\mathrm{Scalar}\left({G}\right)$
144 eqid ${⊢}\mathrm{norm}\left({F}\right)=\mathrm{norm}\left({F}\right)$
145 141 124 142 143 29 144 isnlm ${⊢}{G}\in \mathrm{NrmMod}↔\left(\left({G}\in \mathrm{NrmGrp}\wedge {G}\in \mathrm{LMod}\wedge {F}\in \mathrm{NrmRing}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{F}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\mathrm{norm}\left({G}\right)\left({y}{\cdot }_{{W}}{z}\right)=\mathrm{norm}\left({F}\right)\left({y}\right)\mathrm{norm}\left({G}\right)\left({z}\right)\right)$
146 112 140 145 sylanbrc ${⊢}{\phi }\to {G}\in \mathrm{NrmMod}$
147 10 146 58 3jca ${⊢}{\phi }\to \left({G}\in \mathrm{PreHil}\wedge {G}\in \mathrm{NrmMod}\wedge {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)$
148 elin ${⊢}{x}\in \left({\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right)↔\left({x}\in {\mathrm{Base}}_{{F}}\wedge {x}\in \left[0,\mathrm{+\infty }\right)\right)$
149 elrege0 ${⊢}{x}\in \left[0,\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge 0\le {x}\right)$
150 149 anbi2i ${⊢}\left({x}\in {\mathrm{Base}}_{{F}}\wedge {x}\in \left[0,\mathrm{+\infty }\right)\right)↔\left({x}\in {\mathrm{Base}}_{{F}}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)$
151 148 150 bitri ${⊢}{x}\in \left({\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right)↔\left({x}\in {\mathrm{Base}}_{{F}}\wedge \left({x}\in ℝ\wedge 0\le {x}\right)\right)$
152 151 80 syl5bi ${⊢}{\phi }\to \left({x}\in \left({\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right)\to \sqrt{{x}}\in {\mathrm{Base}}_{{F}}\right)$
153 152 ralrimiv ${⊢}{\phi }\to \forall {x}\in \left({\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}\sqrt{{x}}\in {\mathrm{Base}}_{{F}}$
154 sqrtf ${⊢}\surd :ℂ⟶ℂ$
155 ffun ${⊢}\surd :ℂ⟶ℂ\to \mathrm{Fun}\surd$
156 154 155 ax-mp ${⊢}\mathrm{Fun}\surd$
157 inss1 ${⊢}{\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\subseteq {\mathrm{Base}}_{{F}}$
158 157 37 sstrid ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\subseteq ℂ$
159 154 fdmi ${⊢}\mathrm{dom}\surd =ℂ$
160 158 159 sseqtrrdi ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\subseteq \mathrm{dom}\surd$
161 funimass4 ${⊢}\left(\mathrm{Fun}\surd \wedge {\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\subseteq \mathrm{dom}\surd \right)\to \left(\surd \left[{\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq {\mathrm{Base}}_{{F}}↔\forall {x}\in \left({\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}\sqrt{{x}}\in {\mathrm{Base}}_{{F}}\right)$
162 156 160 161 sylancr ${⊢}{\phi }\to \left(\surd \left[{\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq {\mathrm{Base}}_{{F}}↔\forall {x}\in \left({\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}\sqrt{{x}}\in {\mathrm{Base}}_{{F}}\right)$
163 153 162 mpbird ${⊢}{\phi }\to \surd \left[{\mathrm{Base}}_{{F}}\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq {\mathrm{Base}}_{{F}}$
164 43 fmpttd
165 1 2 6 tcphval
166 cnex ${⊢}ℂ\in \mathrm{V}$
167 165 2 166 tngnm
168 17 164 167 syl2anc
169 168 eqcomd
170 1 6 tcphip
171 141 170 124 143 29 iscph
172 147 163 169 171 syl3anbrc ${⊢}{\phi }\to {G}\in \mathrm{CPreHil}$