Metamath Proof Explorer


Theorem nmopub

Description: An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopub T:A*normopTAxnormx1normTxA

Proof

Step Hyp Ref Expression
1 nmopval T:normopT=supy|xnormx1y=normTx*<
2 1 adantr T:A*normopT=supy|xnormx1y=normTx*<
3 2 breq1d T:A*normopTAsupy|xnormx1y=normTx*<A
4 nmopsetretALT T:y|xnormx1y=normTx
5 ressxr *
6 4 5 sstrdi T:y|xnormx1y=normTx*
7 supxrleub y|xnormx1y=normTx*A*supy|xnormx1y=normTx*<Azy|xnormx1y=normTxzA
8 6 7 sylan T:A*supy|xnormx1y=normTx*<Azy|xnormx1y=normTxzA
9 ancom normx1y=normTxy=normTxnormx1
10 eqeq1 y=zy=normTxz=normTx
11 10 anbi1d y=zy=normTxnormx1z=normTxnormx1
12 9 11 syl5bb y=znormx1y=normTxz=normTxnormx1
13 12 rexbidv y=zxnormx1y=normTxxz=normTxnormx1
14 13 ralab zy|xnormx1y=normTxzAzxz=normTxnormx1zA
15 ralcom4 xzz=normTxnormx1zAzxz=normTxnormx1zA
16 impexp z=normTxnormx1zAz=normTxnormx1zA
17 16 albii zz=normTxnormx1zAzz=normTxnormx1zA
18 fvex normTxV
19 breq1 z=normTxzAnormTxA
20 19 imbi2d z=normTxnormx1zAnormx1normTxA
21 18 20 ceqsalv zz=normTxnormx1zAnormx1normTxA
22 17 21 bitri zz=normTxnormx1zAnormx1normTxA
23 22 ralbii xzz=normTxnormx1zAxnormx1normTxA
24 r19.23v xz=normTxnormx1zAxz=normTxnormx1zA
25 24 albii zxz=normTxnormx1zAzxz=normTxnormx1zA
26 15 23 25 3bitr3i xnormx1normTxAzxz=normTxnormx1zA
27 14 26 bitr4i zy|xnormx1y=normTxzAxnormx1normTxA
28 8 27 bitrdi T:A*supy|xnormx1y=normTx*<Axnormx1normTxA
29 3 28 bitrd T:A*normopTAxnormx1normTxA