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 = ( toCPreHil ` W )
	tcphcph.v	|- V = ( Base ` W )
	tcphcph.f	|- F = ( Scalar ` W )
	tcphcph.1	|- ( ph -> W e. PreHil )
	tcphcph.2	|- ( ph -> F = ( CCfld |`s K ) )
	tcphcph.h	|- ., = ( .i ` W )
	tcphcph.3	|- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
	tcphcph.4	|- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
Assertion	tcphcph	|- ( ph -> G e. CPreHil )

Proof

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