This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmopcoadji

Description: The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of Beran p. 106. (Contributed by NM, 8-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopcoadj.1 
|- T e. BndLinOp
Assertion nmopcoadji 
|- ( normop ` ( ( adjh ` T ) o. T ) ) = ( ( normop ` T ) ^ 2 )

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 
 |-  T e. BndLinOp
2 adjbdlnb 
 |-  ( T e. BndLinOp <-> ( adjh ` T ) e. BndLinOp )
3 1 2 mpbi 
 |-  ( adjh ` T ) e. BndLinOp
4 bdopf 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( adjh ` T ) : ~H --> ~H )
5 3 4 ax-mp 
 |-  ( adjh ` T ) : ~H --> ~H
6 bdopf 
 |-  ( T e. BndLinOp -> T : ~H --> ~H )
7 1 6 ax-mp 
 |-  T : ~H --> ~H
8 5 7 hocofi 
 |-  ( ( adjh ` T ) o. T ) : ~H --> ~H
9 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
10 1 9 ax-mp 
 |-  ( normop ` T ) e. RR
11 10 resqcli 
 |-  ( ( normop ` T ) ^ 2 ) e. RR
12 rexr 
 |-  ( ( ( normop ` T ) ^ 2 ) e. RR -> ( ( normop ` T ) ^ 2 ) e. RR* )
13 11 12 ax-mp 
 |-  ( ( normop ` T ) ^ 2 ) e. RR*
14 nmopub 
 |-  ( ( ( ( adjh ` T ) o. T ) : ~H --> ~H /\ ( ( normop ` T ) ^ 2 ) e. RR* ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) <_ ( ( normop ` T ) ^ 2 ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( ( normop ` T ) ^ 2 ) ) ) )
15 8 13 14 mp2an 
 |-  ( ( normop ` ( ( adjh ` T ) o. T ) ) <_ ( ( normop ` T ) ^ 2 ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( ( normop ` T ) ^ 2 ) ) )
16 5 7 hocoi 
 |-  ( x e. ~H -> ( ( ( adjh ` T ) o. T ) ` x ) = ( ( adjh ` T ) ` ( T ` x ) ) )
17 16 fveq2d 
 |-  ( x e. ~H -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) = ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) )
18 17 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) = ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) )
19 7 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
20 5 ffvelcdmi 
 |-  ( ( T ` x ) e. ~H -> ( ( adjh ` T ) ` ( T ` x ) ) e. ~H )
21 normcl 
 |-  ( ( ( adjh ` T ) ` ( T ` x ) ) e. ~H -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. RR )
22 19 20 21 3syl 
 |-  ( x e. ~H -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. RR )
23 22 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. RR )
24 nmopre 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( normop ` ( adjh ` T ) ) e. RR )
25 3 24 ax-mp 
 |-  ( normop ` ( adjh ` T ) ) e. RR
26 normcl 
 |-  ( ( T ` x ) e. ~H -> ( normh ` ( T ` x ) ) e. RR )
27 19 26 syl 
 |-  ( x e. ~H -> ( normh ` ( T ` x ) ) e. RR )
28 remulcl 
 |-  ( ( ( normop ` ( adjh ` T ) ) e. RR /\ ( normh ` ( T ` x ) ) e. RR ) -> ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) e. RR )
29 25 27 28 sylancr 
 |-  ( x e. ~H -> ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) e. RR )
30 29 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) e. RR )
31 25 10 remulcli 
 |-  ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) e. RR
32 31 a1i 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) e. RR )
33 3 nmbdoplbi 
 |-  ( ( T ` x ) e. ~H -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) )
34 19 33 syl 
 |-  ( x e. ~H -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) )
35 34 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) )
36 27 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) e. RR )
37 10 a1i 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normop ` T ) e. RR )
38 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
39 remulcl 
 |-  ( ( ( normop ` T ) e. RR /\ ( normh ` x ) e. RR ) -> ( ( normop ` T ) x. ( normh ` x ) ) e. RR )
40 10 38 39 sylancr 
 |-  ( x e. ~H -> ( ( normop ` T ) x. ( normh ` x ) ) e. RR )
41 40 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` x ) ) e. RR )
42 1 nmbdoplbi 
 |-  ( x e. ~H -> ( normh ` ( T ` x ) ) <_ ( ( normop ` T ) x. ( normh ` x ) ) )
43 42 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( ( normop ` T ) x. ( normh ` x ) ) )
44 1re 
 |-  1 e. RR
45 nmopge0 
 |-  ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )
46 1 6 45 mp2b 
 |-  0 <_ ( normop ` T )
47 10 46 pm3.2i 
 |-  ( ( normop ` T ) e. RR /\ 0 <_ ( normop ` T ) )
48 lemul2a 
 |-  ( ( ( ( normh ` x ) e. RR /\ 1 e. RR /\ ( ( normop ` T ) e. RR /\ 0 <_ ( normop ` T ) ) ) /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` x ) ) <_ ( ( normop ` T ) x. 1 ) )
49 47 48 mp3anl3 
 |-  ( ( ( ( normh ` x ) e. RR /\ 1 e. RR ) /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` x ) ) <_ ( ( normop ` T ) x. 1 ) )
50 44 49 mpanl2 
 |-  ( ( ( normh ` x ) e. RR /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` x ) ) <_ ( ( normop ` T ) x. 1 ) )
51 38 50 sylan 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` x ) ) <_ ( ( normop ` T ) x. 1 ) )
52 10 recni 
 |-  ( normop ` T ) e. CC
53 52 mulridi 
 |-  ( ( normop ` T ) x. 1 ) = ( normop ` T )
54 51 53 breqtrdi 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` T ) x. ( normh ` x ) ) <_ ( normop ` T ) )
55 36 41 37 43 54 letrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )
56 nmopge0 
 |-  ( ( adjh ` T ) : ~H --> ~H -> 0 <_ ( normop ` ( adjh ` T ) ) )
57 3 4 56 mp2b 
 |-  0 <_ ( normop ` ( adjh ` T ) )
58 25 57 pm3.2i 
 |-  ( ( normop ` ( adjh ` T ) ) e. RR /\ 0 <_ ( normop ` ( adjh ` T ) ) )
59 lemul2a 
 |-  ( ( ( ( normh ` ( T ` x ) ) e. RR /\ ( normop ` T ) e. RR /\ ( ( normop ` ( adjh ` T ) ) e. RR /\ 0 <_ ( normop ` ( adjh ` T ) ) ) ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) )
60 58 59 mp3anl3 
 |-  ( ( ( ( normh ` ( T ` x ) ) e. RR /\ ( normop ` T ) e. RR ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) )
61 36 37 55 60 syl21anc 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( adjh ` T ) ) x. ( normh ` ( T ` x ) ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) )
62 23 30 32 35 61 letrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) )
63 18 62 eqbrtrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) )
64 1 nmopadji 
 |-  ( normop ` ( adjh ` T ) ) = ( normop ` T )
65 64 oveq1i 
 |-  ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) = ( ( normop ` T ) x. ( normop ` T ) )
66 52 sqvali 
 |-  ( ( normop ` T ) ^ 2 ) = ( ( normop ` T ) x. ( normop ` T ) )
67 65 66 eqtr4i 
 |-  ( ( normop ` ( adjh ` T ) ) x. ( normop ` T ) ) = ( ( normop ` T ) ^ 2 )
68 63 67 breqtrdi 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( ( normop ` T ) ^ 2 ) )
69 68 ex 
 |-  ( x e. ~H -> ( ( normh ` x ) <_ 1 -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( ( normop ` T ) ^ 2 ) ) )
70 15 69 mprgbir 
 |-  ( normop ` ( ( adjh ` T ) o. T ) ) <_ ( ( normop ` T ) ^ 2 )
71 nmopge0 
 |-  ( ( ( adjh ` T ) o. T ) : ~H --> ~H -> 0 <_ ( normop ` ( ( adjh ` T ) o. T ) ) )
72 8 71 ax-mp 
 |-  0 <_ ( normop ` ( ( adjh ` T ) o. T ) )
73 3 1 bdopcoi 
 |-  ( ( adjh ` T ) o. T ) e. BndLinOp
74 nmopre 
 |-  ( ( ( adjh ` T ) o. T ) e. BndLinOp -> ( normop ` ( ( adjh ` T ) o. T ) ) e. RR )
75 73 74 ax-mp 
 |-  ( normop ` ( ( adjh ` T ) o. T ) ) e. RR
76 75 sqrtcli 
 |-  ( 0 <_ ( normop ` ( ( adjh ` T ) o. T ) ) -> ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) e. RR )
77 rexr 
 |-  ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) e. RR -> ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) e. RR* )
78 72 76 77 mp2b 
 |-  ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) e. RR*
79 nmopub 
 |-  ( ( T : ~H --> ~H /\ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) e. RR* ) -> ( ( normop ` T ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ) ) )
80 7 78 79 mp2an 
 |-  ( ( normop ` T ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ) )
81 19 20 syl 
 |-  ( x e. ~H -> ( ( adjh ` T ) ` ( T ` x ) ) e. ~H )
82 hicl 
 |-  ( ( ( ( adjh ` T ) ` ( T ` x ) ) e. ~H /\ x e. ~H ) -> ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) e. CC )
83 81 82 mpancom 
 |-  ( x e. ~H -> ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) e. CC )
84 83 abscld 
 |-  ( x e. ~H -> ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) e. RR )
85 84 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) e. RR )
86 22 38 remulcld 
 |-  ( x e. ~H -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) e. RR )
87 86 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) e. RR )
88 75 a1i 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normop ` ( ( adjh ` T ) o. T ) ) e. RR )
89 bcs 
 |-  ( ( ( ( adjh ` T ) ` ( T ` x ) ) e. ~H /\ x e. ~H ) -> ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) <_ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) )
90 81 89 mpancom 
 |-  ( x e. ~H -> ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) <_ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) )
91 90 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) <_ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) )
92 5 7 hococli 
 |-  ( x e. ~H -> ( ( ( adjh ` T ) o. T ) ` x ) e. ~H )
93 normcl 
 |-  ( ( ( ( adjh ` T ) o. T ) ` x ) e. ~H -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) e. RR )
94 92 93 syl 
 |-  ( x e. ~H -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) e. RR )
95 94 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) e. RR )
96 38 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` x ) e. RR )
97 normge0 
 |-  ( ( ( adjh ` T ) ` ( T ` x ) ) e. ~H -> 0 <_ ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) )
98 19 20 97 3syl 
 |-  ( x e. ~H -> 0 <_ ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) )
99 22 98 jca 
 |-  ( x e. ~H -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. RR /\ 0 <_ ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) ) )
100 99 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. RR /\ 0 <_ ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) ) )
101 simpr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` x ) <_ 1 )
102 lemul2a 
 |-  ( ( ( ( normh ` x ) e. RR /\ 1 e. RR /\ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. RR /\ 0 <_ ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) ) ) /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) <_ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. 1 ) )
103 44 102 mp3anl2 
 |-  ( ( ( ( normh ` x ) e. RR /\ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. RR /\ 0 <_ ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) ) ) /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) <_ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. 1 ) )
104 96 100 101 103 syl21anc 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) <_ ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. 1 ) )
105 22 recnd 
 |-  ( x e. ~H -> ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) e. CC )
106 105 mulridd 
 |-  ( x e. ~H -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. 1 ) = ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) )
107 106 17 eqtr4d 
 |-  ( x e. ~H -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. 1 ) = ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) )
108 107 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. 1 ) = ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) )
109 104 108 breqtrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) <_ ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) )
110 remulcl 
 |-  ( ( ( normop ` ( ( adjh ` T ) o. T ) ) e. RR /\ ( normh ` x ) e. RR ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) e. RR )
111 75 38 110 sylancr 
 |-  ( x e. ~H -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) e. RR )
112 111 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) e. RR )
113 73 nmbdoplbi 
 |-  ( x e. ~H -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) )
114 113 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) )
115 75 72 pm3.2i 
 |-  ( ( normop ` ( ( adjh ` T ) o. T ) ) e. RR /\ 0 <_ ( normop ` ( ( adjh ` T ) o. T ) ) )
116 lemul2a 
 |-  ( ( ( ( normh ` x ) e. RR /\ 1 e. RR /\ ( ( normop ` ( ( adjh ` T ) o. T ) ) e. RR /\ 0 <_ ( normop ` ( ( adjh ` T ) o. T ) ) ) ) /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) <_ ( ( normop ` ( ( adjh ` T ) o. T ) ) x. 1 ) )
117 115 116 mp3anl3 
 |-  ( ( ( ( normh ` x ) e. RR /\ 1 e. RR ) /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) <_ ( ( normop ` ( ( adjh ` T ) o. T ) ) x. 1 ) )
118 44 117 mpanl2 
 |-  ( ( ( normh ` x ) e. RR /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) <_ ( ( normop ` ( ( adjh ` T ) o. T ) ) x. 1 ) )
119 38 118 sylan 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) <_ ( ( normop ` ( ( adjh ` T ) o. T ) ) x. 1 ) )
120 75 recni 
 |-  ( normop ` ( ( adjh ` T ) o. T ) ) e. CC
121 120 mulridi 
 |-  ( ( normop ` ( ( adjh ` T ) o. T ) ) x. 1 ) = ( normop ` ( ( adjh ` T ) o. T ) )
122 119 121 breqtrdi 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` ( ( adjh ` T ) o. T ) ) x. ( normh ` x ) ) <_ ( normop ` ( ( adjh ` T ) o. T ) ) )
123 95 112 88 114 122 letrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( ( adjh ` T ) o. T ) ` x ) ) <_ ( normop ` ( ( adjh ` T ) o. T ) ) )
124 87 95 88 109 123 letrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( ( adjh ` T ) ` ( T ` x ) ) ) x. ( normh ` x ) ) <_ ( normop ` ( ( adjh ` T ) o. T ) ) )
125 85 87 88 91 124 letrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) <_ ( normop ` ( ( adjh ` T ) o. T ) ) )
126 resqcl 
 |-  ( ( normh ` ( T ` x ) ) e. RR -> ( ( normh ` ( T ` x ) ) ^ 2 ) e. RR )
127 sqge0 
 |-  ( ( normh ` ( T ` x ) ) e. RR -> 0 <_ ( ( normh ` ( T ` x ) ) ^ 2 ) )
128 126 127 absidd 
 |-  ( ( normh ` ( T ` x ) ) e. RR -> ( abs ` ( ( normh ` ( T ` x ) ) ^ 2 ) ) = ( ( normh ` ( T ` x ) ) ^ 2 ) )
129 19 26 128 3syl 
 |-  ( x e. ~H -> ( abs ` ( ( normh ` ( T ` x ) ) ^ 2 ) ) = ( ( normh ` ( T ` x ) ) ^ 2 ) )
130 normsq 
 |-  ( ( T ` x ) e. ~H -> ( ( normh ` ( T ` x ) ) ^ 2 ) = ( ( T ` x ) .ih ( T ` x ) ) )
131 19 130 syl 
 |-  ( x e. ~H -> ( ( normh ` ( T ` x ) ) ^ 2 ) = ( ( T ` x ) .ih ( T ` x ) ) )
132 bdopadj 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( adjh ` T ) e. dom adjh )
133 3 132 ax-mp 
 |-  ( adjh ` T ) e. dom adjh
134 adj2 
 |-  ( ( ( adjh ` T ) e. dom adjh /\ ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) = ( ( T ` x ) .ih ( ( adjh ` ( adjh ` T ) ) ` x ) ) )
135 133 134 mp3an1 
 |-  ( ( ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) = ( ( T ` x ) .ih ( ( adjh ` ( adjh ` T ) ) ` x ) ) )
136 19 135 mpancom 
 |-  ( x e. ~H -> ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) = ( ( T ` x ) .ih ( ( adjh ` ( adjh ` T ) ) ` x ) ) )
137 bdopadj 
 |-  ( T e. BndLinOp -> T e. dom adjh )
138 adjadj 
 |-  ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) = T )
139 1 137 138 mp2b 
 |-  ( adjh ` ( adjh ` T ) ) = T
140 139 fveq1i 
 |-  ( ( adjh ` ( adjh ` T ) ) ` x ) = ( T ` x )
141 140 oveq2i 
 |-  ( ( T ` x ) .ih ( ( adjh ` ( adjh ` T ) ) ` x ) ) = ( ( T ` x ) .ih ( T ` x ) )
142 136 141 eqtr2di 
 |-  ( x e. ~H -> ( ( T ` x ) .ih ( T ` x ) ) = ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) )
143 131 142 eqtrd 
 |-  ( x e. ~H -> ( ( normh ` ( T ` x ) ) ^ 2 ) = ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) )
144 143 fveq2d 
 |-  ( x e. ~H -> ( abs ` ( ( normh ` ( T ` x ) ) ^ 2 ) ) = ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) )
145 129 144 eqtr3d 
 |-  ( x e. ~H -> ( ( normh ` ( T ` x ) ) ^ 2 ) = ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) )
146 145 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( T ` x ) ) ^ 2 ) = ( abs ` ( ( ( adjh ` T ) ` ( T ` x ) ) .ih x ) ) )
147 75 sqsqrti 
 |-  ( 0 <_ ( normop ` ( ( adjh ` T ) o. T ) ) -> ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) = ( normop ` ( ( adjh ` T ) o. T ) ) )
148 8 71 147 mp2b 
 |-  ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) = ( normop ` ( ( adjh ` T ) o. T ) )
149 148 a1i 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) = ( normop ` ( ( adjh ` T ) o. T ) ) )
150 125 146 149 3brtr4d 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( T ` x ) ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) )
151 normge0 
 |-  ( ( T ` x ) e. ~H -> 0 <_ ( normh ` ( T ` x ) ) )
152 19 151 syl 
 |-  ( x e. ~H -> 0 <_ ( normh ` ( T ` x ) ) )
153 8 71 76 mp2b 
 |-  ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) e. RR
154 75 sqrtge0i 
 |-  ( 0 <_ ( normop ` ( ( adjh ` T ) o. T ) ) -> 0 <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) )
155 8 71 154 mp2b 
 |-  0 <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) )
156 le2sq 
 |-  ( ( ( ( normh ` ( T ` x ) ) e. RR /\ 0 <_ ( normh ` ( T ` x ) ) ) /\ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) e. RR /\ 0 <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ) ) -> ( ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> ( ( normh ` ( T ` x ) ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) ) )
157 153 155 156 mpanr12 
 |-  ( ( ( normh ` ( T ` x ) ) e. RR /\ 0 <_ ( normh ` ( T ` x ) ) ) -> ( ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> ( ( normh ` ( T ` x ) ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) ) )
158 27 152 157 syl2anc 
 |-  ( x e. ~H -> ( ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> ( ( normh ` ( T ` x ) ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) ) )
159 158 adantr 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> ( ( normh ` ( T ` x ) ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) ) )
160 150 159 mpbird 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) )
161 160 ex 
 |-  ( x e. ~H -> ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ) )
162 80 161 mprgbir 
 |-  ( normop ` T ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) )
163 10 153 le2sqi 
 |-  ( ( 0 <_ ( normop ` T ) /\ 0 <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ) -> ( ( normop ` T ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> ( ( normop ` T ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) ) )
164 46 155 163 mp2an 
 |-  ( ( normop ` T ) <_ ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) <-> ( ( normop ` T ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 ) )
165 162 164 mpbi 
 |-  ( ( normop ` T ) ^ 2 ) <_ ( ( sqrt ` ( normop ` ( ( adjh ` T ) o. T ) ) ) ^ 2 )
166 165 148 breqtri 
 |-  ( ( normop ` T ) ^ 2 ) <_ ( normop ` ( ( adjh ` T ) o. T ) )
167 75 11 letri3i 
 |-  ( ( normop ` ( ( adjh ` T ) o. T ) ) = ( ( normop ` T ) ^ 2 ) <-> ( ( normop ` ( ( adjh ` T ) o. T ) ) <_ ( ( normop ` T ) ^ 2 ) /\ ( ( normop ` T ) ^ 2 ) <_ ( normop ` ( ( adjh ` T ) o. T ) ) ) )
168 70 166 167 mpbir2an 
 |-  ( normop ` ( ( adjh ` T ) o. T ) ) = ( ( normop ` T ) ^ 2 )