This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )