Metamath Proof Explorer

Theorem leopnmid

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

Ref Expression
Assertion leopnmid 
|- ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) -> T <_op ( ( normop ` T ) .op Iop ) )

Proof

Step Hyp Ref Expression
1 hmopre 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
2 1 adantlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
3 1 recnd 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. CC )
4 3 abscld 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( abs ` ( ( T ` x ) .ih x ) ) e. RR )
5 4 adantlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( abs ` ( ( T ` x ) .ih x ) ) e. RR )
6 idhmop 
 |-  Iop e. HrmOp
7 hmopm 
 |-  ( ( ( normop ` T ) e. RR /\ Iop e. HrmOp ) -> ( ( normop ` T ) .op Iop ) e. HrmOp )
8 6 7 mpan2 
 |-  ( ( normop ` T ) e. RR -> ( ( normop ` T ) .op Iop ) e. HrmOp )
9 hmopre 
 |-  ( ( ( ( normop ` T ) .op Iop ) e. HrmOp /\ x e. ~H ) -> ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) e. RR )
10 8 9 sylan 
 |-  ( ( ( normop ` T ) e. RR /\ x e. ~H ) -> ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) e. RR )
11 10 adantll 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) e. RR )
12 1 leabsd 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) <_ ( abs ` ( ( T ` x ) .ih x ) ) )
13 12 adantlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( T ` x ) .ih x ) <_ ( abs ` ( ( T ` x ) .ih x ) ) )
14 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
15 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
16 normcl 
 |-  ( ( T ` x ) e. ~H -> ( normh ` ( T ` x ) ) e. RR )
17 15 16 syl 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( normh ` ( T ` x ) ) e. RR )
18 14 17 sylan 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( normh ` ( T ` x ) ) e. RR )
19 18 adantlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( normh ` ( T ` x ) ) e. RR )
20 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
21 20 adantl 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( normh ` x ) e. RR )
22 19 21 remulcld 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( normh ` ( T ` x ) ) x. ( normh ` x ) ) e. RR )
23 14 15 sylan 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( T ` x ) e. ~H )
24 bcs 
 |-  ( ( ( T ` x ) e. ~H /\ x e. ~H ) -> ( abs ` ( ( T ` x ) .ih x ) ) <_ ( ( normh ` ( T ` x ) ) x. ( normh ` x ) ) )
25 23 24 sylancom 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( abs ` ( ( T ` x ) .ih x ) ) <_ ( ( normh ` ( T ` x ) ) x. ( normh ` x ) ) )
26 25 adantlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( abs ` ( ( T ` x ) .ih x ) ) <_ ( ( normh ` ( T ` x ) ) x. ( normh ` x ) ) )
27 remulcl 
 |-  ( ( ( normop ` T ) e. RR /\ ( normh ` x ) e. RR ) -> ( ( normop ` T ) x. ( normh ` x ) ) e. RR )
28 20 27 sylan2 
 |-  ( ( ( normop ` T ) e. RR /\ x e. ~H ) -> ( ( normop ` T ) x. ( normh ` x ) ) e. RR )
29 28 adantll 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( normop ` T ) x. ( normh ` x ) ) e. RR )
30 normge0 
 |-  ( x e. ~H -> 0 <_ ( normh ` x ) )
31 20 30 jca 
 |-  ( x e. ~H -> ( ( normh ` x ) e. RR /\ 0 <_ ( normh ` x ) ) )
32 31 adantl 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( normh ` x ) e. RR /\ 0 <_ ( normh ` x ) ) )
33 hmoplin 
 |-  ( T e. HrmOp -> T e. LinOp )
34 elbdop2 
 |-  ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) )
35 34 biimpri 
 |-  ( ( T e. LinOp /\ ( normop ` T ) e. RR ) -> T e. BndLinOp )
36 33 35 sylan 
 |-  ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) -> T e. BndLinOp )
37 nmbdoplb 
 |-  ( ( T e. BndLinOp /\ x e. ~H ) -> ( normh ` ( T ` x ) ) <_ ( ( normop ` T ) x. ( normh ` x ) ) )
38 36 37 sylan 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( normh ` ( T ` x ) ) <_ ( ( normop ` T ) x. ( normh ` x ) ) )
39 lemul1a 
 |-  ( ( ( ( normh ` ( T ` x ) ) e. RR /\ ( ( normop ` T ) x. ( normh ` x ) ) e. RR /\ ( ( normh ` x ) e. RR /\ 0 <_ ( normh ` x ) ) ) /\ ( normh ` ( T ` x ) ) <_ ( ( normop ` T ) x. ( normh ` x ) ) ) -> ( ( normh ` ( T ` x ) ) x. ( normh ` x ) ) <_ ( ( ( normop ` T ) x. ( normh ` x ) ) x. ( normh ` x ) ) )
40 19 29 32 38 39 syl31anc 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( normh ` ( T ` x ) ) x. ( normh ` x ) ) <_ ( ( ( normop ` T ) x. ( normh ` x ) ) x. ( normh ` x ) ) )
41 recn 
 |-  ( ( normop ` T ) e. RR -> ( normop ` T ) e. CC )
42 41 ad2antlr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( normop ` T ) e. CC )
43 21 recnd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( normh ` x ) e. CC )
44 42 43 43 mulassd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( normop ` T ) x. ( normh ` x ) ) x. ( normh ` x ) ) = ( ( normop ` T ) x. ( ( normh ` x ) x. ( normh ` x ) ) ) )
45 simpr 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> x e. ~H )
46 ax-his3 
 |-  ( ( ( normop ` T ) e. CC /\ x e. ~H /\ x e. ~H ) -> ( ( ( normop ` T ) .h x ) .ih x ) = ( ( normop ` T ) x. ( x .ih x ) ) )
47 42 45 45 46 syl3anc 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( normop ` T ) .h x ) .ih x ) = ( ( normop ` T ) x. ( x .ih x ) ) )
48 20 recnd 
 |-  ( x e. ~H -> ( normh ` x ) e. CC )
49 48 sqvald 
 |-  ( x e. ~H -> ( ( normh ` x ) ^ 2 ) = ( ( normh ` x ) x. ( normh ` x ) ) )
50 normsq 
 |-  ( x e. ~H -> ( ( normh ` x ) ^ 2 ) = ( x .ih x ) )
51 49 50 eqtr3d 
 |-  ( x e. ~H -> ( ( normh ` x ) x. ( normh ` x ) ) = ( x .ih x ) )
52 51 oveq2d 
 |-  ( x e. ~H -> ( ( normop ` T ) x. ( ( normh ` x ) x. ( normh ` x ) ) ) = ( ( normop ` T ) x. ( x .ih x ) ) )
53 52 adantl 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( normop ` T ) x. ( ( normh ` x ) x. ( normh ` x ) ) ) = ( ( normop ` T ) x. ( x .ih x ) ) )
54 47 53 eqtr4d 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( normop ` T ) .h x ) .ih x ) = ( ( normop ` T ) x. ( ( normh ` x ) x. ( normh ` x ) ) ) )
55 44 54 eqtr4d 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( normop ` T ) x. ( normh ` x ) ) x. ( normh ` x ) ) = ( ( ( normop ` T ) .h x ) .ih x ) )
56 hoif 
 |-  Iop : ~H -1-1-onto-> ~H
57 f1of 
 |-  ( Iop : ~H -1-1-onto-> ~H -> Iop : ~H --> ~H )
58 56 57 mp1i 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> Iop : ~H --> ~H )
59 homval 
 |-  ( ( ( normop ` T ) e. CC /\ Iop : ~H --> ~H /\ x e. ~H ) -> ( ( ( normop ` T ) .op Iop ) ` x ) = ( ( normop ` T ) .h ( Iop ` x ) ) )
60 42 58 45 59 syl3anc 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( normop ` T ) .op Iop ) ` x ) = ( ( normop ` T ) .h ( Iop ` x ) ) )
61 hoival 
 |-  ( x e. ~H -> ( Iop ` x ) = x )
62 61 oveq2d 
 |-  ( x e. ~H -> ( ( normop ` T ) .h ( Iop ` x ) ) = ( ( normop ` T ) .h x ) )
63 62 adantl 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( normop ` T ) .h ( Iop ` x ) ) = ( ( normop ` T ) .h x ) )
64 60 63 eqtrd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( normop ` T ) .op Iop ) ` x ) = ( ( normop ` T ) .h x ) )
65 64 oveq1d 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) = ( ( ( normop ` T ) .h x ) .ih x ) )
66 55 65 eqtr4d 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( ( normop ` T ) x. ( normh ` x ) ) x. ( normh ` x ) ) = ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) )
67 40 66 breqtrd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( normh ` ( T ` x ) ) x. ( normh ` x ) ) <_ ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) )
68 5 22 11 26 67 letrd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( abs ` ( ( T ` x ) .ih x ) ) <_ ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) )
69 2 5 11 13 68 letrd 
 |-  ( ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) /\ x e. ~H ) -> ( ( T ` x ) .ih x ) <_ ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) )
70 69 ralrimiva 
 |-  ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) -> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) )
71 leop2 
 |-  ( ( T e. HrmOp /\ ( ( normop ` T ) .op Iop ) e. HrmOp ) -> ( T <_op ( ( normop ` T ) .op Iop ) <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) ) )
72 8 71 sylan2 
 |-  ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) -> ( T <_op ( ( normop ` T ) .op Iop ) <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( ( ( normop ` T ) .op Iop ) ` x ) .ih x ) ) )
73 70 72 mpbird 
 |-  ( ( T e. HrmOp /\ ( normop ` T ) e. RR ) -> T <_op ( ( normop ` T ) .op Iop ) )