Metamath Proof Explorer

Theorem nmophmi

Description: The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmophm.1 
|- T e. BndLinOp
Assertion nmophmi 
|- ( A e. CC -> ( normop ` ( A .op T ) ) = ( ( abs ` A ) x. ( normop ` T ) ) )

Proof

Step Hyp Ref Expression
1 nmophm.1 
 |-  T e. BndLinOp
2 bdopf 
 |-  ( T e. BndLinOp -> T : ~H --> ~H )
3 1 2 ax-mp 
 |-  T : ~H --> ~H
4 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
5 3 4 mp3an2 
 |-  ( ( A e. CC /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
6 5 fveq2d 
 |-  ( ( A e. CC /\ x e. ~H ) -> ( normh ` ( ( A .op T ) ` x ) ) = ( normh ` ( A .h ( T ` x ) ) ) )
7 3 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
8 norm-iii 
 |-  ( ( A e. CC /\ ( T ` x ) e. ~H ) -> ( normh ` ( A .h ( T ` x ) ) ) = ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) )
9 7 8 sylan2 
 |-  ( ( A e. CC /\ x e. ~H ) -> ( normh ` ( A .h ( T ` x ) ) ) = ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) )
10 6 9 eqtrd 
 |-  ( ( A e. CC /\ x e. ~H ) -> ( normh ` ( ( A .op T ) ` x ) ) = ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) )
11 10 adantr 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( A .op T ) ` x ) ) = ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) )
12 normcl 
 |-  ( ( T ` x ) e. ~H -> ( normh ` ( T ` x ) ) e. RR )
13 7 12 syl 
 |-  ( x e. ~H -> ( normh ` ( T ` x ) ) e. RR )
14 13 ad2antlr 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) e. RR )
15 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
16 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
17 15 16 jca 
 |-  ( A e. CC -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
18 17 ad2antrr 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
19 nmoplb 
 |-  ( ( T : ~H --> ~H /\ x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )
20 3 19 mp3an1 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )
21 20 adantll 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )
22 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
23 1 22 ax-mp 
 |-  ( normop ` T ) e. RR
24 lemul2a 
 |-  ( ( ( ( normh ` ( T ` x ) ) e. RR /\ ( normop ` T ) e. RR /\ ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) )
25 23 24 mp3anl2 
 |-  ( ( ( ( normh ` ( T ` x ) ) e. RR /\ ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) )
26 14 18 21 25 syl21anc 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) )
27 11 26 eqbrtrd 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) )
28 27 ex 
 |-  ( ( A e. CC /\ x e. ~H ) -> ( ( normh ` x ) <_ 1 -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) ) )
29 28 ralrimiva 
 |-  ( A e. CC -> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) ) )
30 homulcl 
 |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
31 3 30 mpan2 
 |-  ( A e. CC -> ( A .op T ) : ~H --> ~H )
32 remulcl 
 |-  ( ( ( abs ` A ) e. RR /\ ( normop ` T ) e. RR ) -> ( ( abs ` A ) x. ( normop ` T ) ) e. RR )
33 15 23 32 sylancl 
 |-  ( A e. CC -> ( ( abs ` A ) x. ( normop ` T ) ) e. RR )
34 33 rexrd 
 |-  ( A e. CC -> ( ( abs ` A ) x. ( normop ` T ) ) e. RR* )
35 nmopub 
 |-  ( ( ( A .op T ) : ~H --> ~H /\ ( ( abs ` A ) x. ( normop ` T ) ) e. RR* ) -> ( ( normop ` ( A .op T ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) ) ) )
36 31 34 35 syl2anc 
 |-  ( A e. CC -> ( ( normop ` ( A .op T ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) ) ) )
37 29 36 mpbird 
 |-  ( A e. CC -> ( normop ` ( A .op T ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) )
38 fveq2 
 |-  ( A = 0 -> ( abs ` A ) = ( abs ` 0 ) )
39 abs0 
 |-  ( abs ` 0 ) = 0
40 38 39 eqtrdi 
 |-  ( A = 0 -> ( abs ` A ) = 0 )
41 40 oveq1d 
 |-  ( A = 0 -> ( ( abs ` A ) x. ( normop ` T ) ) = ( 0 x. ( normop ` T ) ) )
42 23 recni 
 |-  ( normop ` T ) e. CC
43 42 mul02i 
 |-  ( 0 x. ( normop ` T ) ) = 0
44 41 43 eqtrdi 
 |-  ( A = 0 -> ( ( abs ` A ) x. ( normop ` T ) ) = 0 )
45 44 adantl 
 |-  ( ( A e. CC /\ A = 0 ) -> ( ( abs ` A ) x. ( normop ` T ) ) = 0 )
46 nmopge0 
 |-  ( ( A .op T ) : ~H --> ~H -> 0 <_ ( normop ` ( A .op T ) ) )
47 31 46 syl 
 |-  ( A e. CC -> 0 <_ ( normop ` ( A .op T ) ) )
48 47 adantr 
 |-  ( ( A e. CC /\ A = 0 ) -> 0 <_ ( normop ` ( A .op T ) ) )
49 45 48 eqbrtrd 
 |-  ( ( A e. CC /\ A = 0 ) -> ( ( abs ` A ) x. ( normop ` T ) ) <_ ( normop ` ( A .op T ) ) )
50 nmoplb 
 |-  ( ( ( A .op T ) : ~H --> ~H /\ x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( normop ` ( A .op T ) ) )
51 31 50 syl3an1 
 |-  ( ( A e. CC /\ x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( normop ` ( A .op T ) ) )
52 51 3expa 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( A .op T ) ` x ) ) <_ ( normop ` ( A .op T ) ) )
53 11 52 eqbrtrrd 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( normop ` ( A .op T ) ) )
54 53 adantllr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( normop ` ( A .op T ) ) )
55 13 adantl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) -> ( normh ` ( T ` x ) ) e. RR )
56 nmopxr 
 |-  ( ( A .op T ) : ~H --> ~H -> ( normop ` ( A .op T ) ) e. RR* )
57 31 56 syl 
 |-  ( A e. CC -> ( normop ` ( A .op T ) ) e. RR* )
58 nmopgtmnf 
 |-  ( ( A .op T ) : ~H --> ~H -> -oo < ( normop ` ( A .op T ) ) )
59 31 58 syl 
 |-  ( A e. CC -> -oo < ( normop ` ( A .op T ) ) )
60 xrre 
 |-  ( ( ( ( normop ` ( A .op T ) ) e. RR* /\ ( ( abs ` A ) x. ( normop ` T ) ) e. RR ) /\ ( -oo < ( normop ` ( A .op T ) ) /\ ( normop ` ( A .op T ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) ) ) -> ( normop ` ( A .op T ) ) e. RR )
61 57 33 59 37 60 syl22anc 
 |-  ( A e. CC -> ( normop ` ( A .op T ) ) e. RR )
62 61 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) -> ( normop ` ( A .op T ) ) e. RR )
63 15 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) -> ( abs ` A ) e. RR )
64 absgt0 
 |-  ( A e. CC -> ( A =/= 0 <-> 0 < ( abs ` A ) ) )
65 64 biimpa 
 |-  ( ( A e. CC /\ A =/= 0 ) -> 0 < ( abs ` A ) )
66 65 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) -> 0 < ( abs ` A ) )
67 lemuldiv2 
 |-  ( ( ( normh ` ( T ` x ) ) e. RR /\ ( normop ` ( A .op T ) ) e. RR /\ ( ( abs ` A ) e. RR /\ 0 < ( abs ` A ) ) ) -> ( ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( normop ` ( A .op T ) ) <-> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) )
68 55 62 63 66 67 syl112anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) -> ( ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( normop ` ( A .op T ) ) <-> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) )
69 68 adantr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( ( abs ` A ) x. ( normh ` ( T ` x ) ) ) <_ ( normop ` ( A .op T ) ) <-> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) )
70 54 69 mpbid 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) )
71 70 ex 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. ~H ) -> ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) )
72 71 ralrimiva 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) )
73 61 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( normop ` ( A .op T ) ) e. RR )
74 15 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR )
75 abs00 
 |-  ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )
76 75 necon3bid 
 |-  ( A e. CC -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
77 76 biimpar 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 )
78 73 74 77 redivcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) e. RR )
79 78 rexrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) e. RR* )
80 nmopub 
 |-  ( ( T : ~H --> ~H /\ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) e. RR* ) -> ( ( normop ` T ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) ) )
81 3 79 80 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( normop ` T ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) ) )
82 72 81 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( normop ` T ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) )
83 23 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( normop ` T ) e. RR )
84 lemuldiv2 
 |-  ( ( ( normop ` T ) e. RR /\ ( normop ` ( A .op T ) ) e. RR /\ ( ( abs ` A ) e. RR /\ 0 < ( abs ` A ) ) ) -> ( ( ( abs ` A ) x. ( normop ` T ) ) <_ ( normop ` ( A .op T ) ) <-> ( normop ` T ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) )
85 83 73 74 65 84 syl112anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( abs ` A ) x. ( normop ` T ) ) <_ ( normop ` ( A .op T ) ) <-> ( normop ` T ) <_ ( ( normop ` ( A .op T ) ) / ( abs ` A ) ) ) )
86 82 85 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) x. ( normop ` T ) ) <_ ( normop ` ( A .op T ) ) )
87 49 86 pm2.61dane 
 |-  ( A e. CC -> ( ( abs ` A ) x. ( normop ` T ) ) <_ ( normop ` ( A .op T ) ) )
88 61 33 letri3d 
 |-  ( A e. CC -> ( ( normop ` ( A .op T ) ) = ( ( abs ` A ) x. ( normop ` T ) ) <-> ( ( normop ` ( A .op T ) ) <_ ( ( abs ` A ) x. ( normop ` T ) ) /\ ( ( abs ` A ) x. ( normop ` T ) ) <_ ( normop ` ( A .op T ) ) ) ) )
89 37 87 88 mpbir2and 
 |-  ( A e. CC -> ( normop ` ( A .op T ) ) = ( ( abs ` A ) x. ( normop ` T ) ) )