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	⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
	tcphcph.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	tcphcph.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	tcphcph.1	⊢ ( 𝜑 → 𝑊 ∈ PreHil )
	tcphcph.2	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
	tcphcph.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	tcphcph.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ 𝐾 )
	tcphcph.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
Assertion	tcphcph	⊢ ( 𝜑 → 𝐺 ∈ ℂPreHil )

Proof

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