Metamath Proof Explorer

Theorem nmopadjlem

Description: Lemma for nmopadji . (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopadjle.1 
|- T e. BndLinOp
Assertion nmopadjlem 
|- ( normop ` ( adjh ` T ) ) <_ ( normop ` T )

Proof

Step Hyp Ref Expression
1 nmopadjle.1 
 |-  T e. BndLinOp
2 adjbdln 
 |-  ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )
3 bdopf 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( adjh ` T ) : ~H --> ~H )
4 1 2 3 mp2b 
 |-  ( adjh ` T ) : ~H --> ~H
5 bdopf 
 |-  ( T e. BndLinOp -> T : ~H --> ~H )
6 nmopxr 
 |-  ( T : ~H --> ~H -> ( normop ` T ) e. RR* )
7 1 5 6 mp2b 
 |-  ( normop ` T ) e. RR*
8 nmopub 
 |-  ( ( ( adjh ` T ) : ~H --> ~H /\ ( normop ` T ) e. RR* ) -> ( ( normop ` ( adjh ` T ) ) <_ ( normop ` T ) <-> A. y e. ~H ( ( normh ` y ) <_ 1 -> ( normh ` ( ( adjh ` T ) ` y ) ) <_ ( normop ` T ) ) ) )
9 4 7 8 mp2an 
 |-  ( ( normop ` ( adjh ` T ) ) <_ ( normop ` T ) <-> A. y e. ~H ( ( normh ` y ) <_ 1 -> ( normh ` ( ( adjh ` T ) ` y ) ) <_ ( normop ` T ) ) )
10 4 ffvelcdmi 
 |-  ( y e. ~H -> ( ( adjh ` T ) ` y ) e. ~H )
11 normcl 
 |-  ( ( ( adjh ` T ) ` y ) e. ~H -> ( normh ` ( ( adjh ` T ) ` y ) ) e. RR )
12 10 11 syl 
 |-  ( y e. ~H -> ( normh ` ( ( adjh ` T ) ` y ) ) e. RR )
13 12 adantr 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( adjh ` T ) ` y ) ) e. RR )
14 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
15 1 14 ax-mp 
 |-  ( normop ` T ) e. RR
16 normcl 
 |-  ( y e. ~H -> ( normh ` y ) e. RR )
17 remulcl 
 |-  ( ( ( normop ` T ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( normop ` T ) x. ( normh ` y ) ) e. RR )
18 15 16 17 sylancr 
 |-  ( y e. ~H -> ( ( normop ` T ) x. ( normh ` y ) ) e. RR )
19 18 adantr 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` y ) ) e. RR )
20 1re 
 |-  1 e. RR
21 15 20 remulcli 
 |-  ( ( normop ` T ) x. 1 ) e. RR
22 21 a1i 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( ( normop ` T ) x. 1 ) e. RR )
23 1 nmopadjlei 
 |-  ( y e. ~H -> ( normh ` ( ( adjh ` T ) ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
24 23 adantr 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( adjh ` T ) ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
25 nmopge0 
 |-  ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )
26 1 5 25 mp2b 
 |-  0 <_ ( normop ` T )
27 15 26 pm3.2i 
 |-  ( ( normop ` T ) e. RR /\ 0 <_ ( normop ` T ) )
28 lemul2a 
 |-  ( ( ( ( normh ` y ) e. RR /\ 1 e. RR /\ ( ( normop ` T ) e. RR /\ 0 <_ ( normop ` T ) ) ) /\ ( normh ` y ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` y ) ) <_ ( ( normop ` T ) x. 1 ) )
29 27 28 mp3anl3 
 |-  ( ( ( ( normh ` y ) e. RR /\ 1 e. RR ) /\ ( normh ` y ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` y ) ) <_ ( ( normop ` T ) x. 1 ) )
30 20 29 mpanl2 
 |-  ( ( ( normh ` y ) e. RR /\ ( normh ` y ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` y ) ) <_ ( ( normop ` T ) x. 1 ) )
31 16 30 sylan 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` y ) ) <_ ( ( normop ` T ) x. 1 ) )
32 13 19 22 24 31 letrd 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( adjh ` T ) ` y ) ) <_ ( ( normop ` T ) x. 1 ) )
33 15 recni 
 |-  ( normop ` T ) e. CC
34 33 mulridi 
 |-  ( ( normop ` T ) x. 1 ) = ( normop ` T )
35 32 34 breqtrdi 
 |-  ( ( y e. ~H /\ ( normh ` y ) <_ 1 ) -> ( normh ` ( ( adjh ` T ) ` y ) ) <_ ( normop ` T ) )
36 35 ex 
 |-  ( y e. ~H -> ( ( normh ` y ) <_ 1 -> ( normh ` ( ( adjh ` T ) ` y ) ) <_ ( normop ` T ) ) )
37 9 36 mprgbir 
 |-  ( normop ` ( adjh ` T ) ) <_ ( normop ` T )