Theorem ipcau2 23033

Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.)

Hypotheses

Ref	Expression
tchval.n	|- G = (toCHil ` W )
tchcph.v	|- V = ( Base ` W )
tchcph.f	|- F = (Scalar ` W )
tchcph.1	|- ( ph -> W e. PreHil )
tchcph.2	|- ( ph -> F = (ℂfld ↾s K ) )
tchcph.h	|- ., = ( .i ` W )
tchcph.3	|- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqr ` x ) e. K )
tchcph.4	|- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
tchcph.k	|- K = ( Base ` F )
ipcau2.n	|- N = ( norm ` G )
ipcau2.c	|- C = ( ( Y ., X ) / ( Y ., Y ) )
ipcau2.3	|- ( ph -> X e. V )
ipcau2.4	|- ( ph -> Y e. V )

Assertion

Ref	Expression
ipcau2	|- ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )

Distinct variable groups:   x, .,   x, F   x, G   x, V   x, C   ph, x   x, W   x, X   x, Y

Allowed substitution hints:   K( x)   N( x)

Proof of Theorem ipcau2

Step	Hyp	Ref	Expression
1		oveq2 6658	. . . . . . 7 |- ( Y = ( 0g ` W ) -> ( X ., Y ) = ( X ., ( 0g ` W ) ) )
2	1	oveq1d 6665	. . . . . 6 |- ( Y = ( 0g ` W ) -> ( ( X ., Y ) x. ( Y ., X ) ) = ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) )
3	2	breq1d 4663	. . . . 5 |- ( Y = ( 0g ` W ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) <-> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) ) )
4		tchval.n	. . . . . . . . . . . . 13 |- G = (toCHil ` W )
5		tchcph.v	. . . . . . . . . . . . 13 |- V = ( Base ` W )
6		tchcph.f	. . . . . . . . . . . . 13 |- F = (Scalar ` W )
7		tchcph.1	. . . . . . . . . . . . 13 |- ( ph -> W e. PreHil )
8		tchcph.2	. . . . . . . . . . . . 13 |- ( ph -> F = (ℂfld ↾s K ) )
9	4, 5, 6, 7, 8	tchclm 23031	. . . . . . . . . . . 12 |- ( ph -> W e. CMod )
10		tchcph.k	. . . . . . . . . . . . 13 |- K = ( Base ` F )
11	6, 10	clmsscn 22879	. . . . . . . . . . . 12 |- ( W e. CMod -> K C_ CC )
12	9, 11	syl 17	. . . . . . . . . . 11 |- ( ph -> K C_ CC )
13		ipcau2.3	. . . . . . . . . . . 12 |- ( ph -> X e. V )
14		ipcau2.4	. . . . . . . . . . . 12 |- ( ph -> Y e. V )
15		tchcph.h	. . . . . . . . . . . . 13 |- ., = ( .i ` W )
16	6, 15, 5, 10	ipcl 19978	. . . . . . . . . . . 12 |- ( ( W e. PreHil /\ X e. V /\ Y e. V ) -> ( X ., Y ) e. K )
17	7, 13, 14, 16	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> ( X ., Y ) e. K )
18	12, 17	sseldd 3604	. . . . . . . . . 10 |- ( ph -> ( X ., Y ) e. CC )
19	18	adantr 481	. . . . . . . . 9 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., Y ) e. CC )
20	6, 15, 5, 10	ipcl 19978	. . . . . . . . . . . 12 |- ( ( W e. PreHil /\ Y e. V /\ X e. V ) -> ( Y ., X ) e. K )
21	7, 14, 13, 20	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> ( Y ., X ) e. K )
22	12, 21	sseldd 3604	. . . . . . . . . 10 |- ( ph -> ( Y ., X ) e. CC )
23	22	adantr 481	. . . . . . . . 9 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., X ) e. CC )
24	4, 5, 6, 7, 8, 15	tchcphlem3 23032	. . . . . . . . . . . 12 |- ( ( ph /\ Y e. V ) -> ( Y ., Y ) e. RR )
25	14, 24	mpdan 702	. . . . . . . . . . 11 |- ( ph -> ( Y ., Y ) e. RR )
26	25	recnd 10068	. . . . . . . . . 10 |- ( ph -> ( Y ., Y ) e. CC )
27	26	adantr 481	. . . . . . . . 9 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) e. CC )
28	6	clm0 22872	. . . . . . . . . . . . . 14 |- ( W e. CMod -> 0 = ( 0g ` F ) )
29	9, 28	syl 17	. . . . . . . . . . . . 13 |- ( ph -> 0 = ( 0g ` F ) )
30	29	eqeq2d 2632	. . . . . . . . . . . 12 |- ( ph -> ( ( Y ., Y ) = 0 <-> ( Y ., Y ) = ( 0g ` F ) ) )
31		eqid 2622	. . . . . . . . . . . . . 14 |- ( 0g ` F ) = ( 0g ` F )
32		eqid 2622	. . . . . . . . . . . . . 14 |- ( 0g ` W ) = ( 0g ` W )
33	6, 15, 5, 31, 32	ipeq0 19983	. . . . . . . . . . . . 13 |- ( ( W e. PreHil /\ Y e. V ) -> ( ( Y ., Y ) = ( 0g ` F ) <-> Y = ( 0g ` W ) ) )
34	7, 14, 33	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> ( ( Y ., Y ) = ( 0g ` F ) <-> Y = ( 0g ` W ) ) )
35	30, 34	bitrd 268	. . . . . . . . . . 11 |- ( ph -> ( ( Y ., Y ) = 0 <-> Y = ( 0g ` W ) ) )
36	35	necon3bid 2838	. . . . . . . . . 10 |- ( ph -> ( ( Y ., Y ) =/= 0 <-> Y =/= ( 0g ` W ) ) )
37	36	biimpar 502	. . . . . . . . 9 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) =/= 0 )
38	19, 23, 27, 37	divassd 10836	. . . . . . . 8 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) = ( ( X ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) ) )
39		ipcau2.c	. . . . . . . . 9 |- C = ( ( Y ., X ) / ( Y ., Y ) )
40	39	oveq2i 6661	. . . . . . . 8 |- ( ( X ., Y ) x. C ) = ( ( X ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) )
41	38, 40	syl6eqr 2674	. . . . . . 7 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) = ( ( X ., Y ) x. C ) )
42		phllmod 19975	. . . . . . . . . . . . 13 |- ( W e. PreHil -> W e. LMod )
43	7, 42	syl 17	. . . . . . . . . . . 12 |- ( ph -> W e. LMod )
44	43	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> W e. LMod )
45	13	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> X e. V )
46	39	fveq2i 6194	. . . . . . . . . . . . . . 15 |- ( * ` C ) = ( * ` ( ( Y ., X ) / ( Y ., Y ) ) )
47	23, 27, 37	cjdivd 13963	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( ( Y ., X ) / ( Y ., Y ) ) ) = ( ( * ` ( Y ., X ) ) / ( * ` ( Y ., Y ) ) ) )
48	46, 47	syl5eq 2668	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) = ( ( * ` ( Y ., X ) ) / ( * ` ( Y ., Y ) ) ) )
49	8	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( *r ` F ) = ( *r ` (ℂfld ↾s K ) ) )
50		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Base ` F ) e. _V
51	10, 50	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . . 22 |- K e. _V
52		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 |- (ℂfld ↾s K ) = (ℂfld ↾s K )
53		cnfldcj 19753	. . . . . . . . . . . . . . . . . . . . . . 23 |- * = ( *r ` ℂfld )
54	52, 53	ressstarv 16007	. . . . . . . . . . . . . . . . . . . . . 22 |- ( K e. _V -> * = ( *r ` (ℂfld ↾s K ) ) )
55	51, 54	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- * = ( *r ` (ℂfld ↾s K ) )
56	49, 55	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( *r ` F ) = * )
57	56	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( *r ` F ) ` ( X ., Y ) ) = ( * ` ( X ., Y ) ) )
58		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 |- ( *r ` F ) = ( *r ` F )
59	6, 15, 5, 58	ipcj 19979	. . . . . . . . . . . . . . . . . . . 20 |- ( ( W e. PreHil /\ X e. V /\ Y e. V ) -> ( ( *r ` F ) ` ( X ., Y ) ) = ( Y ., X ) )
60	7, 13, 14, 59	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( *r ` F ) ` ( X ., Y ) ) = ( Y ., X ) )
61	57, 60	eqtr3d 2658	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( * ` ( X ., Y ) ) = ( Y ., X ) )
62	61	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( X ., Y ) ) = ( Y ., X ) )
63	62	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( * ` ( X ., Y ) ) ) = ( * ` ( Y ., X ) ) )
64	19	cjcjd 13939	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( * ` ( X ., Y ) ) ) = ( X ., Y ) )
65	63, 64	eqtr3d 2658	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( Y ., X ) ) = ( X ., Y ) )
66	25	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) e. RR )
67	66	cjred 13966	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` ( Y ., Y ) ) = ( Y ., Y ) )
68	65, 67	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` ( Y ., X ) ) / ( * ` ( Y ., Y ) ) ) = ( ( X ., Y ) / ( Y ., Y ) ) )
69	19, 27, 37	divrecd 10804	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) / ( Y ., Y ) ) = ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) )
70	48, 68, 69	3eqtrd 2660	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) = ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) )
71	9	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> W e. CMod )
72	17	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., Y ) e. K )
73	6, 15, 5, 10	ipcl 19978	. . . . . . . . . . . . . . . . 17 |- ( ( W e. PreHil /\ Y e. V /\ Y e. V ) -> ( Y ., Y ) e. K )
74	7, 14, 14, 73	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Y ., Y ) e. K )
75	74	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., Y ) e. K )
76	8	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> F = (ℂfld ↾s K ) )
77		phllvec 19974	. . . . . . . . . . . . . . . . . . 19 |- ( W e. PreHil -> W e. LVec )
78	7, 77	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> W e. LVec )
79	6	lvecdrng 19105	. . . . . . . . . . . . . . . . . 18 |- ( W e. LVec -> F e. DivRing )
80	78, 79	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> F e. DivRing )
81	80	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> F e. DivRing )
82	10, 76, 81	cphreccllem 22978	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ Y =/= ( 0g ` W ) ) /\ ( Y ., Y ) e. K /\ ( Y ., Y ) =/= 0 ) -> ( 1 / ( Y ., Y ) ) e. K )
83	75, 37, 82	mpd3an23 1426	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( 1 / ( Y ., Y ) ) e. K )
84	6, 10	clmmcl 22885	. . . . . . . . . . . . . 14 |- ( ( W e. CMod /\ ( X ., Y ) e. K /\ ( 1 / ( Y ., Y ) ) e. K ) -> ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) e. K )
85	71, 72, 83, 84	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. ( 1 / ( Y ., Y ) ) ) e. K )
86	70, 85	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) e. K )
87	14	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> Y e. V )
88		eqid 2622	. . . . . . . . . . . . 13 |- ( .s ` W ) = ( .s ` W )
89	5, 6, 88, 10	lmodvscl 18880	. . . . . . . . . . . 12 |- ( ( W e. LMod /\ ( * ` C ) e. K /\ Y e. V ) -> ( ( * ` C ) ( .s ` W ) Y ) e. V )
90	44, 86, 87, 89	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) ( .s ` W ) Y ) e. V )
91		eqid 2622	. . . . . . . . . . . 12 |- ( -g ` W ) = ( -g ` W )
92	5, 91	lmodvsubcl 18908	. . . . . . . . . . 11 |- ( ( W e. LMod /\ X e. V /\ ( ( * ` C ) ( .s ` W ) Y ) e. V ) -> ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) e. V )
93	44, 45, 90, 92	syl3anc 1326	. . . . . . . . . 10 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) e. V )
94		tchcph.4	. . . . . . . . . . . 12 |- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
95	94	ralrimiva 2966	. . . . . . . . . . 11 |- ( ph -> A. x e. V 0 <_ ( x ., x ) )
96	95	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> A. x e. V 0 <_ ( x ., x ) )
97		oveq12 6659	. . . . . . . . . . . . 13 |- ( ( x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) /\ x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) -> ( x ., x ) = ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) )
98	97	anidms 677	. . . . . . . . . . . 12 |- ( x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) -> ( x ., x ) = ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) )
99	98	breq2d 4665	. . . . . . . . . . 11 |- ( x = ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) -> ( 0 <_ ( x ., x ) <-> 0 <_ ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) ) )
100	99	rspcv 3305	. . . . . . . . . 10 |- ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) e. V -> ( A. x e. V 0 <_ ( x ., x ) -> 0 <_ ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) ) )
101	93, 96, 100	sylc 65	. . . . . . . . 9 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 <_ ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) )
102		eqid 2622	. . . . . . . . . . 11 |- ( -g ` F ) = ( -g ` F )
103		eqid 2622	. . . . . . . . . . 11 |- ( +g ` F ) = ( +g ` F )
104	7	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> W e. PreHil )
105	6, 15, 5, 91, 102, 103, 104, 45, 90, 45, 90	ip2subdi 19989	. . . . . . . . . 10 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( ( X ., X ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) ) ( -g ` F ) ( ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) ) ) )
106	76	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( +g ` F ) = ( +g ` (ℂfld ↾s K ) ) )
107		cnfldadd 19751	. . . . . . . . . . . . . . 15 |- + = ( +g ` ℂfld )
108	52, 107	ressplusg 15993	. . . . . . . . . . . . . 14 |- ( K e. _V -> + = ( +g ` (ℂfld ↾s K ) ) )
109	51, 108	ax-mp 5	. . . . . . . . . . . . 13 |- + = ( +g ` (ℂfld ↾s K ) )
110	106, 109	syl6eqr 2674	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( +g ` F ) = + )
111		eqidd 2623	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) = ( X ., X ) )
112		eqid 2622	. . . . . . . . . . . . . . 15 |- ( .r ` F ) = ( .r ` F )
113	6, 15, 5, 10, 88, 112	ipass 19990	. . . . . . . . . . . . . 14 |- ( ( W e. PreHil /\ ( ( * ` C ) e. K /\ Y e. V /\ ( ( * ` C ) ( .s ` W ) Y ) e. V ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( * ` C ) ( .r ` F ) ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) ) )
114	104, 86, 87, 90, 113	syl13anc 1328	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( * ` C ) ( .r ` F ) ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) ) )
115	76	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( .r ` F ) = ( .r ` (ℂfld ↾s K ) ) )
116		cnfldmul 19752	. . . . . . . . . . . . . . . . 17 |- x. = ( .r ` ℂfld )
117	52, 116	ressmulr 16006	. . . . . . . . . . . . . . . 16 |- ( K e. _V -> x. = ( .r ` (ℂfld ↾s K ) ) )
118	51, 117	ax-mp 5	. . . . . . . . . . . . . . 15 |- x. = ( .r ` (ℂfld ↾s K ) )
119	115, 118	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( .r ` F ) = x. )
120		eqidd 2623	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( * ` C ) = ( * ` C ) )
121	23, 27, 37	divrecd 10804	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., X ) / ( Y ., Y ) ) = ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) )
122	39, 121	syl5eq 2668	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> C = ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) )
123	21	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., X ) e. K )
124	6, 10	clmmcl 22885	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. CMod /\ ( Y ., X ) e. K /\ ( 1 / ( Y ., Y ) ) e. K ) -> ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) e. K )
125	71, 123, 83, 124	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., X ) x. ( 1 / ( Y ., Y ) ) ) e. K )
126	122, 125	eqeltrd 2701	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> C e. K )
127	6, 15, 5, 10, 88, 112, 58	ipassr2 19992	. . . . . . . . . . . . . . . 16 |- ( ( W e. PreHil /\ ( Y e. V /\ Y e. V /\ C e. K ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( Y ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
128	104, 87, 87, 126, 127	syl13anc 1328	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( Y ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
129	119	oveqd 6667	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( ( Y ., Y ) x. C ) )
130	39	oveq2i 6661	. . . . . . . . . . . . . . . . 17 |- ( ( Y ., Y ) x. C ) = ( ( Y ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) )
131	23, 27, 37	divcan2d 10803	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) x. ( ( Y ., X ) / ( Y ., Y ) ) ) = ( Y ., X ) )
132	130, 131	syl5eq 2668	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) x. C ) = ( Y ., X ) )
133	129, 132	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( Y ., Y ) ( .r ` F ) C ) = ( Y ., X ) )
134	56	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( *r ` F ) = * )
135	134	fveq1d 6193	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( *r ` F ) ` C ) = ( * ` C ) )
136	135	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) = ( ( * ` C ) ( .s ` W ) Y ) )
137	136	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) = ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) )
138	128, 133, 137	3eqtr3rd 2665	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( Y ., X ) )
139	119, 120, 138	oveq123d 6671	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) ( .r ` F ) ( Y ., ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( * ` C ) x. ( Y ., X ) ) )
140	114, 139	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( * ` C ) x. ( Y ., X ) ) )
141	110, 111, 140	oveq123d 6671	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., X ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) )
142	6, 15, 5, 10, 88, 112, 58	ipassr2 19992	. . . . . . . . . . . . . 14 |- ( ( W e. PreHil /\ ( X e. V /\ Y e. V /\ C e. K ) ) -> ( ( X ., Y ) ( .r ` F ) C ) = ( X ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
143	104, 45, 87, 126, 142	syl13anc 1328	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) ( .r ` F ) C ) = ( X ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) )
144	119	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) ( .r ` F ) C ) = ( ( X ., Y ) x. C ) )
145	136	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., ( ( ( *r ` F ) ` C ) ( .s ` W ) Y ) ) = ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) )
146	143, 144, 145	3eqtr3rd 2665	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) = ( ( X ., Y ) x. C ) )
147	6, 15, 5, 10, 88, 112	ipass 19990	. . . . . . . . . . . . . 14 |- ( ( W e. PreHil /\ ( ( * ` C ) e. K /\ Y e. V /\ X e. V ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) = ( ( * ` C ) ( .r ` F ) ( Y ., X ) ) )
148	104, 86, 87, 45, 147	syl13anc 1328	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) = ( ( * ` C ) ( .r ` F ) ( Y ., X ) ) )
149	119	oveqd 6667	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) ( .r ` F ) ( Y ., X ) ) = ( ( * ` C ) x. ( Y ., X ) ) )
150	148, 149	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) = ( ( * ` C ) x. ( Y ., X ) ) )
151	110, 146, 150	oveq123d 6671	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) ) = ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) )
152	141, 151	oveq12d 6668	. . . . . . . . . 10 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., ( ( * ` C ) ( .s ` W ) Y ) ) ) ( -g ` F ) ( ( X ., ( ( * ` C ) ( .s ` W ) Y ) ) ( +g ` F ) ( ( ( * ` C ) ( .s ` W ) Y ) ., X ) ) ) = ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) )
153	6, 15, 5, 10	ipcl 19978	. . . . . . . . . . . . . 14 |- ( ( W e. PreHil /\ X e. V /\ X e. V ) -> ( X ., X ) e. K )
154	104, 45, 45, 153	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) e. K )
155	6, 10	clmmcl 22885	. . . . . . . . . . . . . 14 |- ( ( W e. CMod /\ ( * ` C ) e. K /\ ( Y ., X ) e. K ) -> ( ( * ` C ) x. ( Y ., X ) ) e. K )
156	71, 86, 123, 155	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) x. ( Y ., X ) ) e. K )
157	6, 10	clmacl 22884	. . . . . . . . . . . . 13 |- ( ( W e. CMod /\ ( X ., X ) e. K /\ ( ( * ` C ) x. ( Y ., X ) ) e. K ) -> ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
158	71, 154, 156, 157	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
159	6, 10	clmmcl 22885	. . . . . . . . . . . . . 14 |- ( ( W e. CMod /\ ( X ., Y ) e. K /\ C e. K ) -> ( ( X ., Y ) x. C ) e. K )
160	71, 72, 126, 159	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) e. K )
161	6, 10	clmacl 22884	. . . . . . . . . . . . 13 |- ( ( W e. CMod /\ ( ( X ., Y ) x. C ) e. K /\ ( ( * ` C ) x. ( Y ., X ) ) e. K ) -> ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
162	71, 160, 156, 161	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K )
163	6, 10	clmsub 22880	. . . . . . . . . . . 12 |- ( ( W e. CMod /\ ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K /\ ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) e. K ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) - ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) )
164	71, 158, 162, 163	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) - ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) )
165	4, 5, 6, 7, 8, 15	tchcphlem3 23032	. . . . . . . . . . . . . . 15 |- ( ( ph /\ X e. V ) -> ( X ., X ) e. RR )
166	13, 165	mpdan 702	. . . . . . . . . . . . . 14 |- ( ph -> ( X ., X ) e. RR )
167	166	recnd 10068	. . . . . . . . . . . . 13 |- ( ph -> ( X ., X ) e. CC )
168	167	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) e. CC )
169	18	absvalsqd 14181	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) = ( ( X ., Y ) x. ( * ` ( X ., Y ) ) ) )
170	61	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( X ., Y ) x. ( * ` ( X ., Y ) ) ) = ( ( X ., Y ) x. ( Y ., X ) ) )
171	169, 170	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) = ( ( X ., Y ) x. ( Y ., X ) ) )
172	18	abscld 14175	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( abs ` ( X ., Y ) ) e. RR )
173	172	resqcld 13035	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) e. RR )
174	171, 173	eqeltrrd 2702	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( X ., Y ) x. ( Y ., X ) ) e. RR )
175	174	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. ( Y ., X ) ) e. RR )
176	175, 66, 37	redivcld 10853	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) e. RR )
177	41, 176	eqeltrrd 2702	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) e. RR )
178	177	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) e. CC )
179	71, 11	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> K C_ CC )
180	179, 156	sseldd 3604	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( * ` C ) x. ( Y ., X ) ) e. CC )
181	168, 178, 180	pnpcan2d 10430	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) - ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
182	164, 181	eqtr3d 2658	. . . . . . . . . 10 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., X ) + ( ( * ` C ) x. ( Y ., X ) ) ) ( -g ` F ) ( ( ( X ., Y ) x. C ) + ( ( * ` C ) x. ( Y ., X ) ) ) ) = ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
183	105, 152, 182	3eqtrd 2660	. . . . . . . . 9 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ., ( X ( -g ` W ) ( ( * ` C ) ( .s ` W ) Y ) ) ) = ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
184	101, 183	breqtrd 4679	. . . . . . . 8 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 <_ ( ( X ., X ) - ( ( X ., Y ) x. C ) ) )
185	166	adantr 481	. . . . . . . . 9 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( X ., X ) e. RR )
186	185, 177	subge0d 10617	. . . . . . . 8 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( 0 <_ ( ( X ., X ) - ( ( X ., Y ) x. C ) ) <-> ( ( X ., Y ) x. C ) <_ ( X ., X ) ) )
187	184, 186	mpbid 222	. . . . . . 7 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. C ) <_ ( X ., X ) )
188	41, 187	eqbrtrd 4675	. . . . . 6 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) <_ ( X ., X ) )
189		oveq12 6659	. . . . . . . . . . . . 13 |- ( ( x = Y /\ x = Y ) -> ( x ., x ) = ( Y ., Y ) )
190	189	anidms 677	. . . . . . . . . . . 12 |- ( x = Y -> ( x ., x ) = ( Y ., Y ) )
191	190	breq2d 4665	. . . . . . . . . . 11 |- ( x = Y -> ( 0 <_ ( x ., x ) <-> 0 <_ ( Y ., Y ) ) )
192	191	rspcv 3305	. . . . . . . . . 10 |- ( Y e. V -> ( A. x e. V 0 <_ ( x ., x ) -> 0 <_ ( Y ., Y ) ) )
193	14, 95, 192	sylc 65	. . . . . . . . 9 |- ( ph -> 0 <_ ( Y ., Y ) )
194	193	adantr 481	. . . . . . . 8 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 <_ ( Y ., Y ) )
195	66, 194, 37	ne0gt0d 10174	. . . . . . 7 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> 0 < ( Y ., Y ) )
196		ledivmul2 10902	. . . . . . 7 |- ( ( ( ( X ., Y ) x. ( Y ., X ) ) e. RR /\ ( X ., X ) e. RR /\ ( ( Y ., Y ) e. RR /\ 0 < ( Y ., Y ) ) ) -> ( ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) <_ ( X ., X ) <-> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) ) )
197	175, 185, 66, 195, 196	syl112anc 1330	. . . . . 6 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( ( ( X ., Y ) x. ( Y ., X ) ) / ( Y ., Y ) ) <_ ( X ., X ) <-> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) ) )
198	188, 197	mpbid 222	. . . . 5 |- ( ( ph /\ Y =/= ( 0g ` W ) ) -> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) )
199	6, 15, 5, 31, 32	ip0r 19982	. . . . . . . . . 10 |- ( ( W e. PreHil /\ X e. V ) -> ( X ., ( 0g ` W ) ) = ( 0g ` F ) )
200	7, 13, 199	syl2anc 693	. . . . . . . . 9 |- ( ph -> ( X ., ( 0g ` W ) ) = ( 0g ` F ) )
201	200, 29	eqtr4d 2659	. . . . . . . 8 |- ( ph -> ( X ., ( 0g ` W ) ) = 0 )
202	201	oveq1d 6665	. . . . . . 7 |- ( ph -> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) = ( 0 x. ( Y ., X ) ) )
203	22	mul02d 10234	. . . . . . 7 |- ( ph -> ( 0 x. ( Y ., X ) ) = 0 )
204	202, 203	eqtrd 2656	. . . . . 6 |- ( ph -> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) = 0 )
205		oveq12 6659	. . . . . . . . . . 11 |- ( ( x = X /\ x = X ) -> ( x ., x ) = ( X ., X ) )
206	205	anidms 677	. . . . . . . . . 10 |- ( x = X -> ( x ., x ) = ( X ., X ) )
207	206	breq2d 4665	. . . . . . . . 9 |- ( x = X -> ( 0 <_ ( x ., x ) <-> 0 <_ ( X ., X ) ) )
208	207	rspcv 3305	. . . . . . . 8 |- ( X e. V -> ( A. x e. V 0 <_ ( x ., x ) -> 0 <_ ( X ., X ) ) )
209	13, 95, 208	sylc 65	. . . . . . 7 |- ( ph -> 0 <_ ( X ., X ) )
210	166, 25, 209, 193	mulge0d 10604	. . . . . 6 |- ( ph -> 0 <_ ( ( X ., X ) x. ( Y ., Y ) ) )
211	204, 210	eqbrtrd 4675	. . . . 5 |- ( ph -> ( ( X ., ( 0g ` W ) ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) )
212	3, 198, 211	pm2.61ne 2879	. . . 4 |- ( ph -> ( ( X ., Y ) x. ( Y ., X ) ) <_ ( ( X ., X ) x. ( Y ., Y ) ) )
213	166, 209	resqrtcld 14156	. . . . . . 7 |- ( ph -> ( sqr ` ( X ., X ) ) e. RR )
214	213	recnd 10068	. . . . . 6 |- ( ph -> ( sqr ` ( X ., X ) ) e. CC )
215	25, 193	resqrtcld 14156	. . . . . . 7 |- ( ph -> ( sqr ` ( Y ., Y ) ) e. RR )
216	215	recnd 10068	. . . . . 6 |- ( ph -> ( sqr ` ( Y ., Y ) ) e. CC )
217	214, 216	sqmuld 13020	. . . . 5 |- ( ph -> ( ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) ^ 2 ) = ( ( ( sqr ` ( X ., X ) ) ^ 2 ) x. ( ( sqr ` ( Y ., Y ) ) ^ 2 ) ) )
218	167	sqsqrtd 14178	. . . . . 6 |- ( ph -> ( ( sqr ` ( X ., X ) ) ^ 2 ) = ( X ., X ) )
219	26	sqsqrtd 14178	. . . . . 6 |- ( ph -> ( ( sqr ` ( Y ., Y ) ) ^ 2 ) = ( Y ., Y ) )
220	218, 219	oveq12d 6668	. . . . 5 |- ( ph -> ( ( ( sqr ` ( X ., X ) ) ^ 2 ) x. ( ( sqr ` ( Y ., Y ) ) ^ 2 ) ) = ( ( X ., X ) x. ( Y ., Y ) ) )
221	217, 220	eqtrd 2656	. . . 4 |- ( ph -> ( ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) ^ 2 ) = ( ( X ., X ) x. ( Y ., Y ) ) )
222	212, 171, 221	3brtr4d 4685	. . 3 |- ( ph -> ( ( abs ` ( X ., Y ) ) ^ 2 ) <_ ( ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) ^ 2 ) )
223	213, 215	remulcld 10070	. . . 4 |- ( ph -> ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) e. RR )
224	18	absge0d 14183	. . . 4 |- ( ph -> 0 <_ ( abs ` ( X ., Y ) ) )
225	166, 209	sqrtge0d 14159	. . . . 5 |- ( ph -> 0 <_ ( sqr ` ( X ., X ) ) )
226	25, 193	sqrtge0d 14159	. . . . 5 |- ( ph -> 0 <_ ( sqr ` ( Y ., Y ) ) )
227	213, 215, 225, 226	mulge0d 10604	. . . 4 |- ( ph -> 0 <_ ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) )
228	172, 223, 224, 227	le2sqd 13044	. . 3 |- ( ph -> ( ( abs ` ( X ., Y ) ) <_ ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) <-> ( ( abs ` ( X ., Y ) ) ^ 2 ) <_ ( ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) ^ 2 ) ) )
229	222, 228	mpbird 247	. 2 |- ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) )
230		lmodgrp 18870	. . . . 5 |- ( W e. LMod -> W e. Grp )
231	43, 230	syl 17	. . . 4 |- ( ph -> W e. Grp )
232		ipcau2.n	. . . . 5 |- N = ( norm ` G )
233	4, 232, 5, 15	tchnmval 23028	. . . 4 |- ( ( W e. Grp /\ X e. V ) -> ( N ` X ) = ( sqr ` ( X ., X ) ) )
234	231, 13, 233	syl2anc 693	. . 3 |- ( ph -> ( N ` X ) = ( sqr ` ( X ., X ) ) )
235	4, 232, 5, 15	tchnmval 23028	. . . 4 |- ( ( W e. Grp /\ Y e. V ) -> ( N ` Y ) = ( sqr ` ( Y ., Y ) ) )
236	231, 14, 235	syl2anc 693	. . 3 |- ( ph -> ( N ` Y ) = ( sqr ` ( Y ., Y ) ) )
237	234, 236	oveq12d 6668	. 2 |- ( ph -> ( ( N ` X ) x. ( N ` Y ) ) = ( ( sqr ` ( X ., X ) ) x. ( sqr ` ( Y ., Y ) ) ) )
238	229, 237	breqtrrd 4681	1 |- ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   C_ wss 3574   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   2c2 11070   ^cexp 12860   *ccj 13836   sqrcsqrt 13973   abscabs 13974   Basecbs 15857   ↾_s cress 15858   +g cplusg 15941   .rcmulr 15942   *rcstv 15943  Scalarcsca 15944   .scvsca 15945   .icip 15946   0gc0g 16100   Grpcgrp 17422   -gcsg 17424   DivRingcdr 18747   LModclmod 18863   LVecclvec 19102  ℂ_fldccnfld 19746   PreHilcphl 19969   normcnm 22381  CModcclm 22862  toCHilctch 22967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-0g 16102  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-grp 17425  df-minusg 17426  df-sbg 17427  df-subg 17591  df-ghm 17658  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-dvr 18683  df-rnghom 18715  df-drng 18749  df-subrg 18778  df-staf 18845  df-srng 18846  df-lmod 18865  df-lmhm 19022  df-lvec 19103  df-sra 19172  df-rgmod 19173  df-cnfld 19747  df-phl 19971  df-nm 22387  df-tng 22389  df-clm 22863  df-tch 22969

This theorem is referenced by:  tchcphlem1  23034  ipcau  23037