Theorem cnlnadjlem7 10006

Description: Lemma for cnlnadj 10009. Helper lemma to show that F is continuous.

Hypotheses

Ref	Expression
cnlnadjlem.1	|- T e. LinOp
cnlnadjlem.2	|- T e. ConOp
cnlnadjlem.3	|- G = {<.g, h>. | (g e. H~ /\ h = ((T` g) .ih y))}
cnlnadjlem.4	|- B = U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)}
cnlnadjlem.5	|- F = {<.y, u>. | (y e. H~ /\ u = B)}

Assertion

Ref	Expression
cnlnadjlem7	|- (A e. H~ -> (normh` (F` A)) <_ ((normop` T) x. (normh` A)))

Distinct variable groups:   g,h,u,v,w,y,A   u,B   w,F   v,G,w   T,g,h,u,v,w,y

Proof of Theorem cnlnadjlem7

Step	Hyp	Ref	Expression
1		breq1 2622	. 2 |- ((normh` (F` A)) = 0 -> ((normh` (F` A)) <_ ((normop` T) x. (normh` A)) <-> 0 <_ ((normop` T) x. (normh` A))))
2		cnlnadjlem.1	. . . . . . . . . 10 |- T e. LinOp
3		cnlnadjlem.2	. . . . . . . . . 10 |- T e. ConOp
4		cnlnadjlem.3	. . . . . . . . . 10 |- G = {<.g, h>. | (g e. H~ /\ h = ((T` g) .ih y))}
5		cnlnadjlem.4	. . . . . . . . . 10 |- B = U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)}
6		cnlnadjlem.5	. . . . . . . . . 10 |- F = {<.y, u>. | (y e. H~ /\ u = B)}
7	2, 3, 4, 5, 6	cnlnadjlem4 10003	. . . . . . . . 9 |- (A e. H~ -> (F` A) e. H~)
8	2	lnopf 9893	. . . . . . . . . 10 |- T:H~-->H~
9	8	ffvelrni 3815	. . . . . . . . 9 |- ((F` A) e. H~ -> (T` (F` A)) e. H~)
10	7, 9	syl 10	. . . . . . . 8 |- (A e. H~ -> (T` (F` A)) e. H~)
11		hiclt 8947	. . . . . . . 8 |- (((T` (F` A)) e. H~ /\ A e. H~) -> ((T` (F` A)) .ih A) e. CC)
12	10, 11	mpancom 705	. . . . . . 7 |- (A e. H~ -> ((T` (F` A)) .ih A) e. CC)
13		absclt 6833	. . . . . . 7 |- (((T` (F` A)) .ih A) e. CC -> (abs` ((T` (F` A)) .ih A)) e. RR)
14	12, 13	syl 10	. . . . . 6 |- (A e. H~ -> (abs` ((T` (F` A)) .ih A)) e. RR)
15		axmulrcl 5274	. . . . . . 7 |- (((normh` (T` (F` A))) e. RR /\ (normh` A) e. RR) -> ((normh` (T` (F` A))) x. (normh` A)) e. RR)
16		normclt 8991	. . . . . . . 8 |- ((T` (F` A)) e. H~ -> (normh` (T` (F` A))) e. RR)
17	10, 16	syl 10	. . . . . . 7 |- (A e. H~ -> (normh` (T` (F` A))) e. RR)
18		normclt 8991	. . . . . . 7 |- (A e. H~ -> (normh` A) e. RR)
19	15, 17, 18	sylanc 471	. . . . . 6 |- (A e. H~ -> ((normh` (T` (F` A))) x. (normh` A)) e. RR)
20		axmulrcl 5274	. . . . . . 7 |- ((((normop` T) x. (normh` (F` A))) e. RR /\ (normh` A) e. RR) -> (((normop` T) x. (normh` (F` A))) x. (normh` A)) e. RR)
21		normclt 8991	. . . . . . . . 9 |- ((F` A) e. H~ -> (normh` (F` A)) e. RR)
22	7, 21	syl 10	. . . . . . . 8 |- (A e. H~ -> (normh` (F` A)) e. RR)
23	2, 3	nmcopex 9957	. . . . . . . . 9 |- (normop` T) e. RR
24		axmulrcl 5274	. . . . . . . . 9 |- (((normop` T) e. RR /\ (normh` (F` A)) e. RR) -> ((normop` T) x. (normh` (F` A))) e. RR)
25	23, 24	mpan 695	. . . . . . . 8 |- ((normh` (F` A)) e. RR -> ((normop` T) x. (normh` (F` A))) e. RR)
26	22, 25	syl 10	. . . . . . 7 |- (A e. H~ -> ((normop` T) x. (normh` (F` A))) e. RR)
27	20, 26, 18	sylanc 471	. . . . . 6 |- (A e. H~ -> (((normop` T) x. (normh` (F` A))) x. (normh` A)) e. RR)
28		bcst 9048	. . . . . . 7 |- (((T` (F` A)) e. H~ /\ A e. H~) -> (abs` ((T` (F` A)) .ih A)) <_ ((normh` (T` (F` A))) x. (normh` A)))
29	10, 28	mpancom 705	. . . . . 6 |- (A e. H~ -> (abs` ((T` (F` A)) .ih A)) <_ ((normh` (T` (F` A))) x. (normh` A)))
30		lemul1itOLD 5838	. . . . . . 7 |- ((((normh` (T` (F` A))) e. RR /\ ((normop` T) x. (normh` (F` A))) e. RR /\ (normh` A) e. RR) /\ (0 <_ (normh` A) /\ (normh` (T` (F` A))) <_ ((normop` T) x. (normh` (F` A))))) -> ((normh` (T` (F` A))) x. (normh` A)) <_ (((normop` T) x. (normh` (F` A))) x. (normh` A)))
31	17, 26, 18	3jca 819	. . . . . . 7 |- (A e. H~ -> ((normh` (T` (F` A))) e. RR /\ ((normop` T) x. (normh` (F` A))) e. RR /\ (normh` A) e. RR))
32		normge0t 8992	. . . . . . . 8 |- (A e. H~ -> 0 <_ (normh` A))
33	2, 3	nmcoplb 9958	. . . . . . . . 9 |- ((F` A) e. H~ -> (normh` (T` (F` A))) <_ ((normop` T) x. (normh` (F` A))))
34	7, 33	syl 10	. . . . . . . 8 |- (A e. H~ -> (normh` (T` (F` A))) <_ ((normop` T) x. (normh` (F` A))))
35	32, 34	jca 288	. . . . . . 7 |- (A e. H~ -> (0 <_ (normh` A) /\ (normh` (T` (F` A))) <_ ((normop` T) x. (normh` (F` A)))))
36	30, 31, 35	sylanc 471	. . . . . 6 |- (A e. H~ -> ((normh` (T` (F` A))) x. (normh` A)) <_ (((normop` T) x. (normh` (F` A))) x. (normh` A)))
37	14, 19, 27, 29, 36	letrd 5526	. . . . 5 |- (A e. H~ -> (abs` ((T` (F` A)) .ih A)) <_ (((normop` T) x. (normh` (F` A))) x. (normh` A)))
38		normsqt 9001	. . . . . . 7 |- ((F` A) e. H~ -> ((normh` (F` A))^2) = ((F` A) .ih (F` A)))
39	7, 38	syl 10	. . . . . 6 |- (A e. H~ -> ((normh` (F` A))^2) = ((F` A) .ih (F` A)))
40	22	recnd 5315	. . . . . . 7 |- (A e. H~ -> (normh` (F` A)) e. CC)
41		sqvalt 6609	. . . . . . 7 |- ((normh` (F` A)) e. CC -> ((normh` (F` A))^2) = ((normh` (F` A)) x. (normh` (F` A))))
42	40, 41	syl 10	. . . . . 6 |- (A e. H~ -> ((normh` (F` A))^2) = ((normh` (F` A)) x. (normh` (F` A))))
43	2, 3, 4, 5, 6	cnlnadjlem5 10004	. . . . . . . . 9 |- ((A e. H~ /\ (F` A) e. H~) -> ((T` (F` A)) .ih A) = ((F` A) .ih (F` A)))
44	7, 43	mpdan 704	. . . . . . . 8 |- (A e. H~ -> ((T` (F` A)) .ih A) = ((F` A) .ih (F` A)))
45	44	fveq2d 3728	. . . . . . 7 |- (A e. H~ -> (abs` ((T` (F` A)) .ih A)) = (abs` ((F` A) .ih (F` A))))
46		absidt 6862	. . . . . . . 8 |- ((((F` A) .ih (F` A)) e. RR /\ 0 <_ ((F` A) .ih (F` A))) -> (abs` ((F` A) .ih (F` A))) = ((F` A) .ih (F` A)))
47		hiidrclt 8961	. . . . . . . . 9 |- ((F` A) e. H~ -> ((F` A) .ih (F` A)) e. RR)
48	7, 47	syl 10	. . . . . . . 8 |- (A e. H~ -> ((F` A) .ih (F` A)) e. RR)
49		hiidge0t 8964	. . . . . . . . 9 |- ((F` A) e. H~ -> 0 <_ ((F` A) .ih (F` A)))
50	7, 49	syl 10	. . . . . . . 8 |- (A e. H~ -> 0 <_ ((F` A) .ih (F` A)))
51	46, 48, 50	sylanc 471	. . . . . . 7 |- (A e. H~ -> (abs` ((F` A) .ih (F` A))) = ((F` A) .ih (F` A)))
52	45, 51	eqtr2d 1508	. . . . . 6 |- (A e. H~ -> ((F` A) .ih (F` A)) = (abs` ((T` (F` A)) .ih A)))
53	39, 42, 52	3eqtr3rd 1516	. . . . 5 |- (A e. H~ -> (abs` ((T` (F` A)) .ih A)) = ((normh` (F` A)) x. (normh` (F` A))))
54	23	recn 5314	. . . . . . 7 |- (normop` T) e. CC
55		mul23t 5419	. . . . . . 7 |- (((normop` T) e. CC /\ (normh` (F` A)) e. CC /\ (normh` A) e. CC) -> (((normop` T) x. (normh`