Metamath Proof Explorer

Theorem nmopcoi

Description: Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmoptri.1 
|- S e. BndLinOp
nmoptri.2 
|- T e. BndLinOp
Assertion nmopcoi 
|- ( normop ` ( S o. T ) ) <_ ( ( normop ` S ) x. ( normop ` T ) )

Proof

Step Hyp Ref Expression
1 nmoptri.1 
 |-  S e. BndLinOp
2 nmoptri.2 
 |-  T e. BndLinOp
3 bdopln 
 |-  ( S e. BndLinOp -> S e. LinOp )
4 1 3 ax-mp 
 |-  S e. LinOp
5 bdopln 
 |-  ( T e. BndLinOp -> T e. LinOp )
6 2 5 ax-mp 
 |-  T e. LinOp
7 4 6 lnopcoi 
 |-  ( S o. T ) e. LinOp
8 7 lnopfi 
 |-  ( S o. T ) : ~H --> ~H
9 nmopre 
 |-  ( S e. BndLinOp -> ( normop ` S ) e. RR )
10 1 9 ax-mp 
 |-  ( normop ` S ) e. RR
11 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
12 2 11 ax-mp 
 |-  ( normop ` T ) e. RR
13 10 12 remulcli 
 |-  ( ( normop ` S ) x. ( normop ` T ) ) e. RR
14 13 rexri 
 |-  ( ( normop ` S ) x. ( normop ` T ) ) e. RR*
15 nmopub 
 |-  ( ( ( S o. T ) : ~H --> ~H /\ ( ( normop ` S ) x. ( normop ` T ) ) e. RR* ) -> ( ( normop ` ( S o. T ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) ) ) )
16 8 14 15 mp2an 
 |-  ( ( normop ` ( S o. T ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) ) )
17 0le0 
 |-  0 <_ 0
18 17 a1i 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> 0 <_ 0 )
19 4 6 lnopco0i 
 |-  ( ( normop ` T ) = 0 -> ( normop ` ( S o. T ) ) = 0 )
20 7 nmlnop0iHIL 
 |-  ( ( normop ` ( S o. T ) ) = 0 <-> ( S o. T ) = 0hop )
21 19 20 sylib 
 |-  ( ( normop ` T ) = 0 -> ( S o. T ) = 0hop )
22 fveq1 
 |-  ( ( S o. T ) = 0hop -> ( ( S o. T ) ` x ) = ( 0hop ` x ) )
23 22 fveq2d 
 |-  ( ( S o. T ) = 0hop -> ( normh ` ( ( S o. T ) ` x ) ) = ( normh ` ( 0hop ` x ) ) )
24 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
25 24 fveq2d 
 |-  ( x e. ~H -> ( normh ` ( 0hop ` x ) ) = ( normh ` 0h ) )
26 norm0 
 |-  ( normh ` 0h ) = 0
27 25 26 eqtrdi 
 |-  ( x e. ~H -> ( normh ` ( 0hop ` x ) ) = 0 )
28 23 27 sylan9eq 
 |-  ( ( ( S o. T ) = 0hop /\ x e. ~H ) -> ( normh ` ( ( S o. T ) ` x ) ) = 0 )
29 21 28 sylan 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( normh ` ( ( S o. T ) ` x ) ) = 0 )
30 oveq2 
 |-  ( ( normop ` T ) = 0 -> ( ( normop ` S ) x. ( normop ` T ) ) = ( ( normop ` S ) x. 0 ) )
31 10 recni 
 |-  ( normop ` S ) e. CC
32 31 mul01i 
 |-  ( ( normop ` S ) x. 0 ) = 0
33 30 32 eqtrdi 
 |-  ( ( normop ` T ) = 0 -> ( ( normop ` S ) x. ( normop ` T ) ) = 0 )
34 33 adantr 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( ( normop ` S ) x. ( normop ` T ) ) = 0 )
35 18 29 34 3brtr4d 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) )
36 35 adantrr 
 |-  ( ( ( normop ` T ) = 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) )
37 df-ne 
 |-  ( ( normop ` T ) =/= 0 <-> -. ( normop ` T ) = 0 )
38 8 ffvelcdmi 
 |-  ( x e. ~H -> ( ( S o. T ) ` x ) e. ~H )
39 normcl 
 |-  ( ( ( S o. T ) ` x ) e. ~H -> ( normh ` ( ( S o. T ) ` x ) ) e. RR )
40 38 39 syl 
 |-  ( x e. ~H -> ( normh ` ( ( S o. T ) ` x ) ) e. RR )
41 40 recnd 
 |-  ( x e. ~H -> ( normh ` ( ( S o. T ) ` x ) ) e. CC )
42 12 recni 
 |-  ( normop ` T ) e. CC
43 divrec2 
 |-  ( ( ( normh ` ( ( S o. T ) ` x ) ) e. CC /\ ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
44 42 43 mp3an2 
 |-  ( ( ( normh ` ( ( S o. T ) ` x ) ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
45 41 44 sylan 
 |-  ( ( x e. ~H /\ ( normop ` T ) =/= 0 ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
46 45 ancoms 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
47 12 rerecclzi 
 |-  ( ( normop ` T ) =/= 0 -> ( 1 / ( normop ` T ) ) e. RR )
48 bdopf 
 |-  ( T e. BndLinOp -> T : ~H --> ~H )
49 2 48 ax-mp 
 |-  T : ~H --> ~H
50 nmopgt0 
 |-  ( T : ~H --> ~H -> ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) ) )
51 49 50 ax-mp 
 |-  ( ( normop ` T ) =/= 0 <-> 0 < ( normop ` T ) )
52 12 recgt0i 
 |-  ( 0 < ( normop ` T ) -> 0 < ( 1 / ( normop ` T ) ) )
53 51 52 sylbi 
 |-  ( ( normop ` T ) =/= 0 -> 0 < ( 1 / ( normop ` T ) ) )
54 0re 
 |-  0 e. RR
55 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / ( normop ` T ) ) e. RR ) -> ( 0 < ( 1 / ( normop ` T ) ) -> 0 <_ ( 1 / ( normop ` T ) ) ) )
56 54 55 mpan 
 |-  ( ( 1 / ( normop ` T ) ) e. RR -> ( 0 < ( 1 / ( normop ` T ) ) -> 0 <_ ( 1 / ( normop ` T ) ) ) )
57 47 53 56 sylc 
 |-  ( ( normop ` T ) =/= 0 -> 0 <_ ( 1 / ( normop ` T ) ) )
58 47 57 absidd 
 |-  ( ( normop ` T ) =/= 0 -> ( abs ` ( 1 / ( normop ` T ) ) ) = ( 1 / ( normop ` T ) ) )
59 58 adantr 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( abs ` ( 1 / ( normop ` T ) ) ) = ( 1 / ( normop ` T ) ) )
60 59 oveq1d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
61 46 60 eqtr4d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
62 42 recclzi 
 |-  ( ( normop ` T ) =/= 0 -> ( 1 / ( normop ` T ) ) e. CC )
63 norm-iii 
 |-  ( ( ( 1 / ( normop ` T ) ) e. CC /\ ( ( S o. T ) ` x ) e. ~H ) -> ( normh ` ( ( 1 / ( normop ` T ) ) .h ( ( S o. T ) ` x ) ) ) = ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
64 62 38 63 syl2an 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( normh ` ( ( 1 / ( normop ` T ) ) .h ( ( S o. T ) ` x ) ) ) = ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( ( S o. T ) ` x ) ) ) )
65 61 64 eqtr4d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( normh ` ( ( 1 / ( normop ` T ) ) .h ( ( S o. T ) ` x ) ) ) )
66 49 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
67 4 lnopmuli 
 |-  ( ( ( 1 / ( normop ` T ) ) e. CC /\ ( T ` x ) e. ~H ) -> ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) = ( ( 1 / ( normop ` T ) ) .h ( S ` ( T ` x ) ) ) )
68 62 66 67 syl2an 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) = ( ( 1 / ( normop ` T ) ) .h ( S ` ( T ` x ) ) ) )
69 bdopf 
 |-  ( S e. BndLinOp -> S : ~H --> ~H )
70 1 69 ax-mp 
 |-  S : ~H --> ~H
71 70 49 hocoi 
 |-  ( x e. ~H -> ( ( S o. T ) ` x ) = ( S ` ( T ` x ) ) )
72 71 oveq2d 
 |-  ( x e. ~H -> ( ( 1 / ( normop ` T ) ) .h ( ( S o. T ) ` x ) ) = ( ( 1 / ( normop ` T ) ) .h ( S ` ( T ` x ) ) ) )
73 72 adantl 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( 1 / ( normop ` T ) ) .h ( ( S o. T ) ` x ) ) = ( ( 1 / ( normop ` T ) ) .h ( S ` ( T ` x ) ) ) )
74 68 73 eqtr4d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) = ( ( 1 / ( normop ` T ) ) .h ( ( S o. T ) ` x ) ) )
75 74 fveq2d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( normh ` ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) ) = ( normh ` ( ( 1 / ( normop ` T ) ) .h ( ( S o. T ) ` x ) ) ) )
76 65 75 eqtr4d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( normh ` ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) ) )
77 76 adantrr 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) = ( normh ` ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) ) )
78 hvmulcl 
 |-  ( ( ( 1 / ( normop ` T ) ) e. CC /\ ( T ` x ) e. ~H ) -> ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) e. ~H )
79 62 66 78 syl2an 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) e. ~H )
80 79 adantrr 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) e. ~H )
81 norm-iii 
 |-  ( ( ( 1 / ( normop ` T ) ) e. CC /\ ( T ` x ) e. ~H ) -> ( normh ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) = ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( T ` x ) ) ) )
82 62 66 81 syl2an 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( normh ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) = ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( T ` x ) ) ) )
83 normcl 
 |-  ( ( T ` x ) e. ~H -> ( normh ` ( T ` x ) ) e. RR )
84 66 83 syl 
 |-  ( x e. ~H -> ( normh ` ( T ` x ) ) e. RR )
85 84 recnd 
 |-  ( x e. ~H -> ( normh ` ( T ` x ) ) e. CC )
86 divrec2 
 |-  ( ( ( normh ` ( T ` x ) ) e. CC /\ ( normop ` T ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( T ` x ) ) ) )
87 42 86 mp3an2 
 |-  ( ( ( normh ` ( T ` x ) ) e. CC /\ ( normop ` T ) =/= 0 ) -> ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( T ` x ) ) ) )
88 85 87 sylan 
 |-  ( ( x e. ~H /\ ( normop ` T ) =/= 0 ) -> ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( T ` x ) ) ) )
89 88 ancoms 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( T ` x ) ) ) )
90 59 oveq1d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( T ` x ) ) ) = ( ( 1 / ( normop ` T ) ) x. ( normh ` ( T ` x ) ) ) )
91 89 90 eqtr4d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) = ( ( abs ` ( 1 / ( normop ` T ) ) ) x. ( normh ` ( T ` x ) ) ) )
92 82 91 eqtr4d 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( normh ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) = ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) )
93 92 adantrr 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) = ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) )
94 nmoplb 
 |-  ( ( T : ~H --> ~H /\ x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )
95 49 94 mp3an1 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )
96 42 mullidi 
 |-  ( 1 x. ( normop ` T ) ) = ( normop ` T )
97 95 96 breqtrrdi 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( 1 x. ( normop ` T ) ) )
98 97 adantl 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( T ` x ) ) <_ ( 1 x. ( normop ` T ) ) )
99 84 adantr 
 |-  ( ( x e. ~H /\ ( normop ` T ) =/= 0 ) -> ( normh ` ( T ` x ) ) e. RR )
100 1red 
 |-  ( ( x e. ~H /\ ( normop ` T ) =/= 0 ) -> 1 e. RR )
101 12 a1i 
 |-  ( ( x e. ~H /\ ( normop ` T ) =/= 0 ) -> ( normop ` T ) e. RR )
102 51 biimpi 
 |-  ( ( normop ` T ) =/= 0 -> 0 < ( normop ` T ) )
103 102 adantl 
 |-  ( ( x e. ~H /\ ( normop ` T ) =/= 0 ) -> 0 < ( normop ` T ) )
104 ledivmul2 
 |-  ( ( ( normh ` ( T ` x ) ) e. RR /\ 1 e. RR /\ ( ( normop ` T ) e. RR /\ 0 < ( normop ` T ) ) ) -> ( ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) <_ 1 <-> ( normh ` ( T ` x ) ) <_ ( 1 x. ( normop ` T ) ) ) )
105 99 100 101 103 104 syl112anc 
 |-  ( ( x e. ~H /\ ( normop ` T ) =/= 0 ) -> ( ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) <_ 1 <-> ( normh ` ( T ` x ) ) <_ ( 1 x. ( normop ` T ) ) ) )
106 105 ancoms 
 |-  ( ( ( normop ` T ) =/= 0 /\ x e. ~H ) -> ( ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) <_ 1 <-> ( normh ` ( T ` x ) ) <_ ( 1 x. ( normop ` T ) ) ) )
107 106 adantrr 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) <_ 1 <-> ( normh ` ( T ` x ) ) <_ ( 1 x. ( normop ` T ) ) ) )
108 98 107 mpbird 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( normh ` ( T ` x ) ) / ( normop ` T ) ) <_ 1 )
109 93 108 eqbrtrd 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) <_ 1 )
110 nmoplb 
 |-  ( ( S : ~H --> ~H /\ ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) e. ~H /\ ( normh ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) <_ 1 ) -> ( normh ` ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) ) <_ ( normop ` S ) )
111 70 110 mp3an1 
 |-  ( ( ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) e. ~H /\ ( normh ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) <_ 1 ) -> ( normh ` ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) ) <_ ( normop ` S ) )
112 80 109 111 syl2anc 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( S ` ( ( 1 / ( normop ` T ) ) .h ( T ` x ) ) ) ) <_ ( normop ` S ) )
113 77 112 eqbrtrd 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) <_ ( normop ` S ) )
114 40 ad2antrl 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( S o. T ) ` x ) ) e. RR )
115 10 a1i 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normop ` S ) e. RR )
116 102 adantr 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> 0 < ( normop ` T ) )
117 116 12 jctil 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( normop ` T ) e. RR /\ 0 < ( normop ` T ) ) )
118 ledivmul2 
 |-  ( ( ( normh ` ( ( S o. T ) ` x ) ) e. RR /\ ( normop ` S ) e. RR /\ ( ( normop ` T ) e. RR /\ 0 < ( normop ` T ) ) ) -> ( ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) <_ ( normop ` S ) <-> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) ) )
119 114 115 117 118 syl3anc 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( ( ( normh ` ( ( S o. T ) ` x ) ) / ( normop ` T ) ) <_ ( normop ` S ) <-> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) ) )
120 113 119 mpbid 
 |-  ( ( ( normop ` T ) =/= 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) )
121 37 120 sylanbr 
 |-  ( ( -. ( normop ` T ) = 0 /\ ( x e. ~H /\ ( normh ` x ) <_ 1 ) ) -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) )
122 36 121 pm2.61ian 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) )
123 122 ex 
 |-  ( x e. ~H -> ( ( normh ` x ) <_ 1 -> ( normh ` ( ( S o. T ) ` x ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) ) )
124 16 123 mprgbir 
 |-  ( normop ` ( S o. T ) ) <_ ( ( normop ` S ) x. ( normop ` T ) )