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 TBndLinOp
Assertion nmopcoadji normopadjhTT=normopT2

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 TBndLinOp
2 adjbdlnb TBndLinOpadjhTBndLinOp
3 1 2 mpbi adjhTBndLinOp
4 bdopf adjhTBndLinOpadjhT:
5 3 4 ax-mp adjhT:
6 bdopf TBndLinOpT:
7 1 6 ax-mp T:
8 5 7 hocofi adjhTT:
9 nmopre TBndLinOpnormopT
10 1 9 ax-mp normopT
11 10 resqcli normopT2
12 rexr normopT2normopT2*
13 11 12 ax-mp normopT2*
14 nmopub adjhTT:normopT2*normopadjhTTnormopT2xnormx1normadjhTTxnormopT2
15 8 13 14 mp2an normopadjhTTnormopT2xnormx1normadjhTTxnormopT2
16 5 7 hocoi xadjhTTx=adjhTTx
17 16 fveq2d xnormadjhTTx=normadjhTTx
18 17 adantr xnormx1normadjhTTx=normadjhTTx
19 7 ffvelrni xTx
20 5 ffvelrni TxadjhTTx
21 normcl adjhTTxnormadjhTTx
22 19 20 21 3syl xnormadjhTTx
23 22 adantr xnormx1normadjhTTx
24 nmopre adjhTBndLinOpnormopadjhT
25 3 24 ax-mp normopadjhT
26 normcl TxnormTx
27 19 26 syl xnormTx
28 remulcl normopadjhTnormTxnormopadjhTnormTx
29 25 27 28 sylancr xnormopadjhTnormTx
30 29 adantr xnormx1normopadjhTnormTx
31 25 10 remulcli normopadjhTnormopT
32 31 a1i xnormx1normopadjhTnormopT
33 3 nmbdoplbi TxnormadjhTTxnormopadjhTnormTx
34 19 33 syl xnormadjhTTxnormopadjhTnormTx
35 34 adantr xnormx1normadjhTTxnormopadjhTnormTx
36 27 adantr xnormx1normTx
37 10 a1i xnormx1normopT
38 normcl xnormx
39 remulcl normopTnormxnormopTnormx
40 10 38 39 sylancr xnormopTnormx
41 40 adantr xnormx1normopTnormx
42 1 nmbdoplbi xnormTxnormopTnormx
43 42 adantr xnormx1normTxnormopTnormx
44 1re 1
45 nmopge0 T:0normopT
46 1 6 45 mp2b 0normopT
47 10 46 pm3.2i normopT0normopT
48 lemul2a normx1normopT0normopTnormx1normopTnormxnormopT1
49 47 48 mp3anl3 normx1normx1normopTnormxnormopT1
50 44 49 mpanl2 normxnormx1normopTnormxnormopT1
51 38 50 sylan xnormx1normopTnormxnormopT1
52 10 recni normopT
53 52 mulid1i normopT1=normopT
54 51 53 breqtrdi xnormx1normopTnormxnormopT
55 36 41 37 43 54 letrd xnormx1normTxnormopT
56 nmopge0 adjhT:0normopadjhT
57 3 4 56 mp2b 0normopadjhT
58 25 57 pm3.2i normopadjhT0normopadjhT
59 lemul2a normTxnormopTnormopadjhT0normopadjhTnormTxnormopTnormopadjhTnormTxnormopadjhTnormopT
60 58 59 mp3anl3 normTxnormopTnormTxnormopTnormopadjhTnormTxnormopadjhTnormopT
61 36 37 55 60 syl21anc xnormx1normopadjhTnormTxnormopadjhTnormopT
62 23 30 32 35 61 letrd xnormx1normadjhTTxnormopadjhTnormopT
63 18 62 eqbrtrd xnormx1normadjhTTxnormopadjhTnormopT
64 1 nmopadji normopadjhT=normopT
65 64 oveq1i normopadjhTnormopT=normopTnormopT
66 52 sqvali normopT2=normopTnormopT
67 65 66 eqtr4i normopadjhTnormopT=normopT2
68 63 67 breqtrdi xnormx1normadjhTTxnormopT2
69 68 ex xnormx1normadjhTTxnormopT2
70 15 69 mprgbir normopadjhTTnormopT2
71 nmopge0 adjhTT:0normopadjhTT
72 8 71 ax-mp 0normopadjhTT
73 3 1 bdopcoi adjhTTBndLinOp
74 nmopre adjhTTBndLinOpnormopadjhTT
75 73 74 ax-mp normopadjhTT
76 75 sqrtcli 0normopadjhTTnormopadjhTT
77 rexr normopadjhTTnormopadjhTT*
78 72 76 77 mp2b normopadjhTT*
79 nmopub T:normopadjhTT*normopTnormopadjhTTxnormx1normTxnormopadjhTT
80 7 78 79 mp2an normopTnormopadjhTTxnormx1normTxnormopadjhTT
81 19 20 syl xadjhTTx
82 hicl adjhTTxxadjhTTxihx
83 81 82 mpancom xadjhTTxihx
84 83 abscld xadjhTTxihx
85 84 adantr xnormx1adjhTTxihx
86 22 38 remulcld xnormadjhTTxnormx
87 86 adantr xnormx1normadjhTTxnormx
88 75 a1i xnormx1normopadjhTT
89 bcs adjhTTxxadjhTTxihxnormadjhTTxnormx
90 81 89 mpancom xadjhTTxihxnormadjhTTxnormx
91 90 adantr xnormx1adjhTTxihxnormadjhTTxnormx
92 5 7 hococli xadjhTTx
93 normcl adjhTTxnormadjhTTx
94 92 93 syl xnormadjhTTx
95 94 adantr xnormx1normadjhTTx
96 38 adantr xnormx1normx
97 normge0 adjhTTx0normadjhTTx
98 19 20 97 3syl x0normadjhTTx
99 22 98 jca xnormadjhTTx0normadjhTTx
100 99 adantr xnormx1normadjhTTx0normadjhTTx
101 simpr xnormx1normx1
102 lemul2a normx1normadjhTTx0normadjhTTxnormx1normadjhTTxnormxnormadjhTTx1
103 44 102 mp3anl2 normxnormadjhTTx0normadjhTTxnormx1normadjhTTxnormxnormadjhTTx1
104 96 100 101 103 syl21anc xnormx1normadjhTTxnormxnormadjhTTx1
105 22 recnd xnormadjhTTx
106 105 mulid1d xnormadjhTTx1=normadjhTTx
107 106 17 eqtr4d xnormadjhTTx1=normadjhTTx
108 107 adantr xnormx1normadjhTTx1=normadjhTTx
109 104 108 breqtrd xnormx1normadjhTTxnormxnormadjhTTx
110 remulcl normopadjhTTnormxnormopadjhTTnormx
111 75 38 110 sylancr xnormopadjhTTnormx
112 111 adantr xnormx1normopadjhTTnormx
113 73 nmbdoplbi xnormadjhTTxnormopadjhTTnormx
114 113 adantr xnormx1normadjhTTxnormopadjhTTnormx
115 75 72 pm3.2i normopadjhTT0normopadjhTT
116 lemul2a normx1normopadjhTT0normopadjhTTnormx1normopadjhTTnormxnormopadjhTT1
117 115 116 mp3anl3 normx1normx1normopadjhTTnormxnormopadjhTT1
118 44 117 mpanl2 normxnormx1normopadjhTTnormxnormopadjhTT1
119 38 118 sylan xnormx1normopadjhTTnormxnormopadjhTT1
120 75 recni normopadjhTT
121 120 mulid1i normopadjhTT1=normopadjhTT
122 119 121 breqtrdi xnormx1normopadjhTTnormxnormopadjhTT
123 95 112 88 114 122 letrd xnormx1normadjhTTxnormopadjhTT
124 87 95 88 109 123 letrd xnormx1normadjhTTxnormxnormopadjhTT
125 85 87 88 91 124 letrd xnormx1adjhTTxihxnormopadjhTT
126 resqcl normTxnormTx2
127 sqge0 normTx0normTx2
128 126 127 absidd normTxnormTx2=normTx2
129 19 26 128 3syl xnormTx2=normTx2
130 normsq TxnormTx2=TxihTx
131 19 130 syl xnormTx2=TxihTx
132 bdopadj adjhTBndLinOpadjhTdomadjh
133 3 132 ax-mp adjhTdomadjh
134 adj2 adjhTdomadjhTxxadjhTTxihx=TxihadjhadjhTx
135 133 134 mp3an1 TxxadjhTTxihx=TxihadjhadjhTx
136 19 135 mpancom xadjhTTxihx=TxihadjhadjhTx
137 bdopadj TBndLinOpTdomadjh
138 adjadj TdomadjhadjhadjhT=T
139 1 137 138 mp2b adjhadjhT=T
140 139 fveq1i adjhadjhTx=Tx
141 140 oveq2i TxihadjhadjhTx=TxihTx
142 136 141 eqtr2di xTxihTx=adjhTTxihx
143 131 142 eqtrd xnormTx2=adjhTTxihx
144 143 fveq2d xnormTx2=adjhTTxihx
145 129 144 eqtr3d xnormTx2=adjhTTxihx
146 145 adantr xnormx1normTx2=adjhTTxihx
147 75 sqsqrti 0normopadjhTTnormopadjhTT2=normopadjhTT
148 8 71 147 mp2b normopadjhTT2=normopadjhTT
149 148 a1i xnormx1normopadjhTT2=normopadjhTT
150 125 146 149 3brtr4d xnormx1normTx2normopadjhTT2
151 normge0 Tx0normTx
152 19 151 syl x0normTx
153 8 71 76 mp2b normopadjhTT
154 75 sqrtge0i 0normopadjhTT0normopadjhTT
155 8 71 154 mp2b 0normopadjhTT
156 le2sq normTx0normTxnormopadjhTT0normopadjhTTnormTxnormopadjhTTnormTx2normopadjhTT2
157 153 155 156 mpanr12 normTx0normTxnormTxnormopadjhTTnormTx2normopadjhTT2
158 27 152 157 syl2anc xnormTxnormopadjhTTnormTx2normopadjhTT2
159 158 adantr xnormx1normTxnormopadjhTTnormTx2normopadjhTT2
160 150 159 mpbird xnormx1normTxnormopadjhTT
161 160 ex xnormx1normTxnormopadjhTT
162 80 161 mprgbir normopTnormopadjhTT
163 10 153 le2sqi 0normopT0normopadjhTTnormopTnormopadjhTTnormopT2normopadjhTT2
164 46 155 163 mp2an normopTnormopadjhTTnormopT2normopadjhTT2
165 162 164 mpbi normopT2normopadjhTT2
166 165 148 breqtri normopT2normopadjhTT
167 75 11 letri3i normopadjhTT=normopT2normopadjhTTnormopT2normopT2normopadjhTT
168 70 166 167 mpbir2an normopadjhTT=normopT2