Metamath Proof Explorer

Theorem nmopleid

Description: A nonzero, bounded Hermitian operator divided by its norm is less than or equal to the identity operator. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopleid 
|- ( ( T e. HrmOp /\ ( normop ` T ) e. RR /\ T =/= 0hop ) -> ( ( 1 / ( normop ` T ) ) .op T ) <_op Iop )

Proof

Step Hyp Ref Expression
1 hmoplin 
 |-  ( T e. HrmOp -> T e. LinOp )
2 nmlnopne0 
 |-  ( T e. LinOp -> ( ( normop ` T ) =/= 0 <-> T =/= 0hop ) )
3 2 biimpar 
 |-  ( ( T e. LinOp /\ T =/= 0hop ) -> ( normop ` T ) =/= 0 )
4 1 3 sylan 
 |-  ( ( T e. HrmOp /\ T =/= 0hop ) -> ( normop ` T ) =/= 0 )
5 4 adantlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ T =/= 0hop ) -> ( normop ` T ) =/= 0 )
6 rereccl 
 |-  ( ( ( normop ` T ) e. RR /\ ( normop ` T ) =/= 0 ) -> ( 1 / ( normop ` T ) ) e. RR )
7 6 adantll 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> ( 1 / ( normop ` T ) ) e. RR )
8 simpll 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> T e. HrmOp )
9 idhmop 
 |-  Iop e. HrmOp
10 hmopm 
 |-  ( ( ( normop ` T ) e. RR /\ Iop e. HrmOp ) -> ( ( normop ` T ) .op Iop ) e. HrmOp )
11 9 10 mpan2 
 |-  ( ( normop ` T ) e. RR -> ( ( normop ` T ) .op Iop ) e. HrmOp )
12 11 ad2antlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> ( ( normop ` T ) .op Iop ) e. HrmOp )
13 simplr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> ( normop ` T ) e. RR )
14 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
15 nmopgt0 
 |-  ( T : ~H --> ~H -> ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) ) )
16 15 biimpa 
 |-  ( ( T : ~H --> ~H /\ ( normop ` T ) =/= 0 ) -> 0 < ( normop ` T ) )
17 14 16 sylan 
 |-  ( ( T e. HrmOp /\ ( normop ` T ) =/= 0 ) -> 0 < ( normop ` T ) )
18 17 adantlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> 0 < ( normop ` T ) )
19 13 18 recgt0d 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> 0 < ( 1 / ( normop ` T ) ) )
20 0re 
 |-  0 e. RR
21 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / ( normop ` T ) ) e. RR ) -> ( 0 < ( 1 / ( normop ` T ) ) -> 0 <_ ( 1 / ( normop ` T ) ) ) )
22 20 6 21 sylancr 
 |-  ( ( ( normop ` T ) e. RR /\ ( normop ` T ) =/= 0 ) -> ( 0 < ( 1 / ( normop ` T ) ) -> 0 <_ ( 1 / ( normop ` T ) ) ) )
23 22 adantll 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> ( 0 < ( 1 / ( normop ` T ) ) -> 0 <_ ( 1 / ( normop ` T ) ) ) )
24 19 23 mpd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> 0 <_ ( 1 / ( normop ` T ) ) )
25 leopnmid 
 |-  ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) -> T <_op ( ( normop ` T ) .op Iop ) )
26 25 adantr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> T <_op ( ( normop ` T ) .op Iop ) )
27 leopmul2i 
 |-  ( ( ( ( 1 / ( normop ` T ) ) e. RR /\ T e. HrmOp /\ ( ( normop ` T ) .op Iop ) e. HrmOp ) /\ ( 0 <_ ( 1 / ( normop ` T ) ) /\ T <_op ( ( normop ` T ) .op Iop ) ) ) -> ( ( 1 / ( normop ` T ) ) .op T ) <_op ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) )
28 7 8 12 24 26 27 syl32anc 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> ( ( 1 / ( normop ` T ) ) .op T ) <_op ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) )
29 recn 
 |-  ( ( normop ` T ) e. RR -> ( normop ` T ) e. CC )
30 reccl 
 |-  ( ( ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( 1 / ( normop ` T ) ) e. CC )
31 simpl 
 |-  ( ( ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( normop ` T ) e. CC )
32 hoif 
 |-  Iop : ~H -1-1-onto-> ~H
33 f1of 
 |-  ( Iop : ~H -1-1-onto-> ~H -> Iop : ~H --> ~H )
34 32 33 ax-mp 
 |-  Iop : ~H --> ~H
35 homulass 
 |-  ( ( ( 1 / ( normop ` T ) ) e. CC /\ ( normop ` T ) e. CC /\ Iop : ~H --> ~H ) -> ( ( ( 1 / ( normop ` T ) ) x. ( normop ` T ) ) .op Iop ) = ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) )
36 34 35 mp3an3 
 |-  ( ( ( 1 / ( normop ` T ) ) e. CC /\ ( normop ` T ) e. CC ) -> ( ( ( 1 / ( normop ` T ) ) x. ( normop ` T ) ) .op Iop ) = ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) )
37 30 31 36 syl2anc 
 |-  ( ( ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( ( 1 / ( normop ` T ) ) x. ( normop ` T ) ) .op Iop ) = ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) )
38 recid2 
 |-  ( ( ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( 1 / ( normop ` T ) ) x. ( normop ` T ) ) = 1 )
39 38 oveq1d 
 |-  ( ( ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( ( 1 / ( normop ` T ) ) x. ( normop ` T ) ) .op Iop ) = ( 1 .op Iop ) )
40 37 39 eqtr3d 
 |-  ( ( ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) = ( 1 .op Iop ) )
41 homullid 
 |-  ( Iop : ~H --> ~H -> ( 1 .op Iop ) = Iop )
42 34 41 ax-mp 
 |-  ( 1 .op Iop ) = Iop
43 40 42 eqtrdi 
 |-  ( ( ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) = Iop )
44 29 43 sylan 
 |-  ( ( ( normop ` T ) e. RR /\ ( normop ` T ) =/= 0 ) -> ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) = Iop )
45 44 adantll 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> ( ( 1 / ( normop ` T ) ) .op ( ( normop ` T ) .op Iop ) ) = Iop )
46 28 45 breqtrd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ ( normop ` T ) =/= 0 ) -> ( ( 1 / ( normop ` T ) ) .op T ) <_op Iop )
47 5 46 syldan 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ T =/= 0hop ) -> ( ( 1 / ( normop ` T ) ) .op T ) <_op Iop )
48 47 3impa 
 |-  ( ( T e. HrmOp /\ ( normop ` T ) e. RR /\ T =/= 0hop ) -> ( ( 1 / ( normop ` T ) ) .op T ) <_op Iop )