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

Metamath Proof Explorer

Theorem tcphcph

Proof