Theorem cnlnadjlem7

Description: Lemma for cnlnadji . Helper lemma to show that F is continuous. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnlnadjlem.1	|- T e. LinOp
	cnlnadjlem.2	|- T e. ContOp
	cnlnadjlem.3	|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
	cnlnadjlem.4	|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
	cnlnadjlem.5	|- F = ( y e. ~H |-> B )
Assertion	cnlnadjlem7	|- ( A e. ~H -> ( normh ` ( F ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	|- T e. LinOp
2		cnlnadjlem.2	|- T e. ContOp
3		cnlnadjlem.3	|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
4		cnlnadjlem.4	|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
5		cnlnadjlem.5	|- F = ( y e. ~H |-> B )
6		breq1	|- ( ( normh ` ( F ` A ) ) = 0 -> ( ( normh ` ( F ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) <-> 0 <_ ( ( normop ` T ) x. ( normh ` A ) ) ) )
7	1 2 3 4 5	cnlnadjlem4	|- ( A e. ~H -> ( F ` A ) e. ~H )
8	1	lnopfi	|- T : ~H --> ~H
9	8	ffvelcdmi	|- ( ( F ` A ) e. ~H -> ( T ` ( F ` A ) ) e. ~H )
10	7 9	syl	|- ( A e. ~H -> ( T ` ( F ` A ) ) e. ~H )
11		hicl	|- ( ( ( T ` ( F ` A ) ) e. ~H /\ A e. ~H ) -> ( ( T ` ( F ` A ) ) .ih A ) e. CC )
12	10 11	mpancom	|- ( A e. ~H -> ( ( T ` ( F ` A ) ) .ih A ) e. CC )
13	12	abscld	|- ( A e. ~H -> ( abs ` ( ( T ` ( F ` A ) ) .ih A ) ) e. RR )
14		normcl	|- ( ( T ` ( F ` A ) ) e. ~H -> ( normh ` ( T ` ( F ` A ) ) ) e. RR )
15	10 14	syl	|- ( A e. ~H -> ( normh ` ( T ` ( F ` A ) ) ) e. RR )
16		normcl	|- ( A e. ~H -> ( normh ` A ) e. RR )
17	15 16	remulcld	|- ( A e. ~H -> ( ( normh ` ( T ` ( F ` A ) ) ) x. ( normh ` A ) ) e. RR )
18	1 2	nmcopexi	|- ( normop ` T ) e. RR
19		normcl	|- ( ( F ` A ) e. ~H -> ( normh ` ( F ` A ) ) e. RR )
20	7 19	syl	|- ( A e. ~H -> ( normh ` ( F ` A ) ) e. RR )
21		remulcl	|- ( ( ( normop ` T ) e. RR /\ ( normh ` ( F ` A ) ) e. RR ) -> ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) e. RR )
22	18 20 21	sylancr	|- ( A e. ~H -> ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) e. RR )
23	22 16	remulcld	|- ( A e. ~H -> ( ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) x. ( normh ` A ) ) e. RR )
24		bcs	|- ( ( ( T ` ( F ` A ) ) e. ~H /\ A e. ~H ) -> ( abs ` ( ( T ` ( F ` A ) ) .ih A ) ) <_ ( ( normh ` ( T ` ( F ` A ) ) ) x. ( normh ` A ) ) )
25	10 24	mpancom	|- ( A e. ~H -> ( abs ` ( ( T ` ( F ` A ) ) .ih A ) ) <_ ( ( normh ` ( T ` ( F ` A ) ) ) x. ( normh ` A ) ) )
26		normge0	|- ( A e. ~H -> 0 <_ ( normh ` A ) )
27	1 2	nmcoplbi	|- ( ( F ` A ) e. ~H -> ( normh ` ( T ` ( F ` A ) ) ) <_ ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) )
28	7 27	syl	|- ( A e. ~H -> ( normh ` ( T ` ( F ` A ) ) ) <_ ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) )
29	15 22 16 26 28	lemul1ad	|- ( A e. ~H -> ( ( normh ` ( T ` ( F ` A ) ) ) x. ( normh ` A ) ) <_ ( ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) x. ( normh ` A ) ) )
30	13 17 23 25 29	letrd	|- ( A e. ~H -> ( abs ` ( ( T ` ( F ` A ) ) .ih A ) ) <_ ( ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) x. ( normh ` A ) ) )
31	1 2 3 4 5	cnlnadjlem5	|- ( ( A e. ~H /\ ( F ` A ) e. ~H ) -> ( ( T ` ( F ` A ) ) .ih A ) = ( ( F ` A ) .ih ( F ` A ) ) )
32	7 31	mpdan	|- ( A e. ~H -> ( ( T ` ( F ` A ) ) .ih A ) = ( ( F ` A ) .ih ( F ` A ) ) )
33	32	fveq2d	|- ( A e. ~H -> ( abs ` ( ( T ` ( F ` A ) ) .ih A ) ) = ( abs ` ( ( F ` A ) .ih ( F ` A ) ) ) )
34		hiidrcl	|- ( ( F ` A ) e. ~H -> ( ( F ` A ) .ih ( F ` A ) ) e. RR )
35	7 34	syl	|- ( A e. ~H -> ( ( F ` A ) .ih ( F ` A ) ) e. RR )
36		hiidge0	|- ( ( F ` A ) e. ~H -> 0 <_ ( ( F ` A ) .ih ( F ` A ) ) )
37	7 36	syl	|- ( A e. ~H -> 0 <_ ( ( F ` A ) .ih ( F ` A ) ) )
38	35 37	absidd	|- ( A e. ~H -> ( abs ` ( ( F ` A ) .ih ( F ` A ) ) ) = ( ( F ` A ) .ih ( F ` A ) ) )
39		normsq	|- ( ( F ` A ) e. ~H -> ( ( normh ` ( F ` A ) ) ^ 2 ) = ( ( F ` A ) .ih ( F ` A ) ) )
40	7 39	syl	|- ( A e. ~H -> ( ( normh ` ( F ` A ) ) ^ 2 ) = ( ( F ` A ) .ih ( F ` A ) ) )
41	20	recnd	|- ( A e. ~H -> ( normh ` ( F ` A ) ) e. CC )
42	41	sqvald	|- ( A e. ~H -> ( ( normh ` ( F ` A ) ) ^ 2 ) = ( ( normh ` ( F ` A ) ) x. ( normh ` ( F ` A ) ) ) )
43	40 42	eqtr3d	|- ( A e. ~H -> ( ( F ` A ) .ih ( F ` A ) ) = ( ( normh ` ( F ` A ) ) x. ( normh ` ( F ` A ) ) ) )
44	33 38 43	3eqtrd	|- ( A e. ~H -> ( abs ` ( ( T ` ( F ` A ) ) .ih A ) ) = ( ( normh ` ( F ` A ) ) x. ( normh ` ( F ` A ) ) ) )
45	16	recnd	|- ( A e. ~H -> ( normh ` A ) e. CC )
46	18	recni	|- ( normop ` T ) e. CC
47		mul32	|- ( ( ( normop ` T ) e. CC /\ ( normh ` ( F ` A ) ) e. CC /\ ( normh ` A ) e. CC ) -> ( ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) x. ( normh ` A ) ) = ( ( ( normop ` T ) x. ( normh ` A ) ) x. ( normh ` ( F ` A ) ) ) )
48	46 47	mp3an1	|- ( ( ( normh ` ( F ` A ) ) e. CC /\ ( normh ` A ) e. CC ) -> ( ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) x. ( normh ` A ) ) = ( ( ( normop ` T ) x. ( normh ` A ) ) x. ( normh ` ( F ` A ) ) ) )
49	41 45 48	syl2anc	|- ( A e. ~H -> ( ( ( normop ` T ) x. ( normh ` ( F ` A ) ) ) x. ( normh ` A ) ) = ( ( ( normop ` T ) x. ( normh ` A ) ) x. ( normh ` ( F ` A ) ) ) )
50	30 44 49	3brtr3d	|- ( A e. ~H -> ( ( normh ` ( F ` A ) ) x. ( normh ` ( F ` A ) ) ) <_ ( ( ( normop ` T ) x. ( normh ` A ) ) x. ( normh ` ( F ` A ) ) ) )
51	50	adantr	|- ( ( A e. ~H /\ ( normh ` ( F ` A ) ) =/= 0 ) -> ( ( normh ` ( F ` A ) ) x. ( normh ` ( F ` A ) ) ) <_ ( ( ( normop ` T ) x. ( normh ` A ) ) x. ( normh ` ( F ` A ) ) ) )
52	20	adantr	|- ( ( A e. ~H /\ ( normh ` ( F ` A ) ) =/= 0 ) -> ( normh ` ( F ` A ) ) e. RR )
53		remulcl	|- ( ( ( normop ` T ) e. RR /\ ( normh ` A ) e. RR ) -> ( ( normop ` T ) x. ( normh ` A ) ) e. RR )
54	18 16 53	sylancr	|- ( A e. ~H -> ( ( normop ` T ) x. ( normh ` A ) ) e. RR )
55	54	adantr	|- ( ( A e. ~H /\ ( normh ` ( F ` A ) ) =/= 0 ) -> ( ( normop ` T ) x. ( normh ` A ) ) e. RR )
56		normge0	|- ( ( F ` A ) e. ~H -> 0 <_ ( normh ` ( F ` A ) ) )
57		0re	|- 0 e. RR
58		leltne	|- ( ( 0 e. RR /\ ( normh ` ( F ` A ) ) e. RR /\ 0 <_ ( normh ` ( F ` A ) ) ) -> ( 0 < ( normh ` ( F ` A ) ) <-> ( normh ` ( F ` A ) ) =/= 0 ) )
59	57 58	mp3an1	|- ( ( ( normh ` ( F ` A ) ) e. RR /\ 0 <_ ( normh ` ( F ` A ) ) ) -> ( 0 < ( normh ` ( F ` A ) ) <-> ( normh ` ( F ` A ) ) =/= 0 ) )
60	19 56 59	syl2anc	|- ( ( F ` A ) e. ~H -> ( 0 < ( normh ` ( F ` A ) ) <-> ( normh ` ( F ` A ) ) =/= 0 ) )
61	60	biimpar	|- ( ( ( F ` A ) e. ~H /\ ( normh ` ( F ` A ) ) =/= 0 ) -> 0 < ( normh ` ( F ` A ) ) )
62	7 61	sylan	|- ( ( A e. ~H /\ ( normh ` ( F ` A ) ) =/= 0 ) -> 0 < ( normh ` ( F ` A ) ) )
63		lemul1	|- ( ( ( normh ` ( F ` A ) ) e. RR /\ ( ( normop ` T ) x. ( normh ` A ) ) e. RR /\ ( ( normh ` ( F ` A ) ) e. RR /\ 0 < ( normh ` ( F ` A ) ) ) ) -> ( ( normh ` ( F ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) <-> ( ( normh ` ( F ` A ) ) x. ( normh ` ( F ` A ) ) ) <_ ( ( ( normop ` T ) x. ( normh ` A ) ) x. ( normh ` ( F ` A ) ) ) ) )
64	52 55 52 62 63	syl112anc	|- ( ( A e. ~H /\ ( normh ` ( F ` A ) ) =/= 0 ) -> ( ( normh ` ( F ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) <-> ( ( normh ` ( F ` A ) ) x. ( normh ` ( F ` A ) ) ) <_ ( ( ( normop ` T ) x. ( normh ` A ) ) x. ( normh ` ( F ` A ) ) ) ) )
65	51 64	mpbird	|- ( ( A e. ~H /\ ( normh ` ( F ` A ) ) =/= 0 ) -> ( normh ` ( F ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
66		nmopge0	|- ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )
67	8 66	ax-mp	|- 0 <_ ( normop ` T )
68		mulge0	|- ( ( ( ( normop ` T ) e. RR /\ 0 <_ ( normop ` T ) ) /\ ( ( normh ` A ) e. RR /\ 0 <_ ( normh ` A ) ) ) -> 0 <_ ( ( normop ` T ) x. ( normh ` A ) ) )
69	18 67 68	mpanl12	|- ( ( ( normh ` A ) e. RR /\ 0 <_ ( normh ` A ) ) -> 0 <_ ( ( normop ` T ) x. ( normh ` A ) ) )
70	16 26 69	syl2anc	|- ( A e. ~H -> 0 <_ ( ( normop ` T ) x. ( normh ` A ) ) )
71	6 65 70	pm2.61ne	|- ( A e. ~H -> ( normh ` ( F ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )