Metamath Proof Explorer

Theorem nmoub3i

Description: An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 
|- X = ( BaseSet ` U )
nmoubi.y 
|- Y = ( BaseSet ` W )
nmoubi.l 
|- L = ( normCV ` U )
nmoubi.m 
|- M = ( normCV ` W )
nmoubi.3 
|- N = ( U normOpOLD W )
nmoubi.u 
|- U e. NrmCVec
nmoubi.w 
|- W e. NrmCVec
Assertion nmoub3i 
|- ( ( T : X --> Y /\ A e. RR /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 nmoubi.1 
 |-  X = ( BaseSet ` U )
2 nmoubi.y 
 |-  Y = ( BaseSet ` W )
3 nmoubi.l 
 |-  L = ( normCV ` U )
4 nmoubi.m 
 |-  M = ( normCV ` W )
5 nmoubi.3 
 |-  N = ( U normOpOLD W )
6 nmoubi.u 
 |-  U e. NrmCVec
7 nmoubi.w 
 |-  W e. NrmCVec
8 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> ( L ` x ) e. RR )
9 6 8 mpan 
 |-  ( x e. X -> ( L ` x ) e. RR )
10 remulcl 
 |-  ( ( A e. RR /\ ( L ` x ) e. RR ) -> ( A x. ( L ` x ) ) e. RR )
11 9 10 sylan2 
 |-  ( ( A e. RR /\ x e. X ) -> ( A x. ( L ` x ) ) e. RR )
12 11 adantr 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( A x. ( L ` x ) ) e. RR )
13 recn 
 |-  ( A e. RR -> A e. CC )
14 13 abscld 
 |-  ( A e. RR -> ( abs ` A ) e. RR )
15 remulcl 
 |-  ( ( ( abs ` A ) e. RR /\ ( L ` x ) e. RR ) -> ( ( abs ` A ) x. ( L ` x ) ) e. RR )
16 14 9 15 syl2an 
 |-  ( ( A e. RR /\ x e. X ) -> ( ( abs ` A ) x. ( L ` x ) ) e. RR )
17 16 adantr 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( ( abs ` A ) x. ( L ` x ) ) e. RR )
18 14 ad2antrr 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( abs ` A ) e. RR )
19 simpl 
 |-  ( ( A e. RR /\ x e. X ) -> A e. RR )
20 14 adantr 
 |-  ( ( A e. RR /\ x e. X ) -> ( abs ` A ) e. RR )
21 1 3 nvge0 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> 0 <_ ( L ` x ) )
22 6 21 mpan 
 |-  ( x e. X -> 0 <_ ( L ` x ) )
23 9 22 jca 
 |-  ( x e. X -> ( ( L ` x ) e. RR /\ 0 <_ ( L ` x ) ) )
24 23 adantl 
 |-  ( ( A e. RR /\ x e. X ) -> ( ( L ` x ) e. RR /\ 0 <_ ( L ` x ) ) )
25 leabs 
 |-  ( A e. RR -> A <_ ( abs ` A ) )
26 25 adantr 
 |-  ( ( A e. RR /\ x e. X ) -> A <_ ( abs ` A ) )
27 lemul1a 
 |-  ( ( ( A e. RR /\ ( abs ` A ) e. RR /\ ( ( L ` x ) e. RR /\ 0 <_ ( L ` x ) ) ) /\ A <_ ( abs ` A ) ) -> ( A x. ( L ` x ) ) <_ ( ( abs ` A ) x. ( L ` x ) ) )
28 19 20 24 26 27 syl31anc 
 |-  ( ( A e. RR /\ x e. X ) -> ( A x. ( L ` x ) ) <_ ( ( abs ` A ) x. ( L ` x ) ) )
29 28 adantr 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( A x. ( L ` x ) ) <_ ( ( abs ` A ) x. ( L ` x ) ) )
30 9 adantl 
 |-  ( ( A e. RR /\ x e. X ) -> ( L ` x ) e. RR )
31 1red 
 |-  ( ( A e. RR /\ x e. X ) -> 1 e. RR )
32 13 absge0d 
 |-  ( A e. RR -> 0 <_ ( abs ` A ) )
33 32 adantr 
 |-  ( ( A e. RR /\ x e. X ) -> 0 <_ ( abs ` A ) )
34 20 33 jca 
 |-  ( ( A e. RR /\ x e. X ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
35 30 31 34 3jca 
 |-  ( ( A e. RR /\ x e. X ) -> ( ( L ` x ) e. RR /\ 1 e. RR /\ ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) )
36 lemul2a 
 |-  ( ( ( ( L ` x ) e. RR /\ 1 e. RR /\ ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) /\ ( L ` x ) <_ 1 ) -> ( ( abs ` A ) x. ( L ` x ) ) <_ ( ( abs ` A ) x. 1 ) )
37 35 36 sylan 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( ( abs ` A ) x. ( L ` x ) ) <_ ( ( abs ` A ) x. 1 ) )
38 14 recnd 
 |-  ( A e. RR -> ( abs ` A ) e. CC )
39 38 mulid1d 
 |-  ( A e. RR -> ( ( abs ` A ) x. 1 ) = ( abs ` A ) )
40 39 ad2antrr 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( ( abs ` A ) x. 1 ) = ( abs ` A ) )
41 37 40 breqtrd 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( ( abs ` A ) x. ( L ` x ) ) <_ ( abs ` A ) )
42 12 17 18 29 41 letrd 
 |-  ( ( ( A e. RR /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( A x. ( L ` x ) ) <_ ( abs ` A ) )
43 42 adantlll 
 |-  ( ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( A x. ( L ` x ) ) <_ ( abs ` A ) )
44 ffvelrn 
 |-  ( ( T : X --> Y /\ x e. X ) -> ( T ` x ) e. Y )
45 2 4 nvcl 
 |-  ( ( W e. NrmCVec /\ ( T ` x ) e. Y ) -> ( M ` ( T ` x ) ) e. RR )
46 7 44 45 sylancr 
 |-  ( ( T : X --> Y /\ x e. X ) -> ( M ` ( T ` x ) ) e. RR )
47 46 adantlr 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) -> ( M ` ( T ` x ) ) e. RR )
48 11 adantll 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) -> ( A x. ( L ` x ) ) e. RR )
49 14 ad2antlr 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) -> ( abs ` A ) e. RR )
50 letr 
 |-  ( ( ( M ` ( T ` x ) ) e. RR /\ ( A x. ( L ` x ) ) e. RR /\ ( abs ` A ) e. RR ) -> ( ( ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) /\ ( A x. ( L ` x ) ) <_ ( abs ` A ) ) -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) )
51 47 48 49 50 syl3anc 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) -> ( ( ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) /\ ( A x. ( L ` x ) ) <_ ( abs ` A ) ) -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) )
52 51 adantr 
 |-  ( ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( ( ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) /\ ( A x. ( L ` x ) ) <_ ( abs ` A ) ) -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) )
53 43 52 mpan2d 
 |-  ( ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) /\ ( L ` x ) <_ 1 ) -> ( ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) )
54 53 ex 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) -> ( ( L ` x ) <_ 1 -> ( ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) ) )
55 54 com23 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ x e. X ) -> ( ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) -> ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) ) )
56 55 ralimdva 
 |-  ( ( T : X --> Y /\ A e. RR ) -> ( A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) -> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) ) )
57 56 imp 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) )
58 14 rexrd 
 |-  ( A e. RR -> ( abs ` A ) e. RR* )
59 1 2 3 4 5 6 7 nmoubi 
 |-  ( ( T : X --> Y /\ ( abs ` A ) e. RR* ) -> ( ( N ` T ) <_ ( abs ` A ) <-> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) ) )
60 58 59 sylan2 
 |-  ( ( T : X --> Y /\ A e. RR ) -> ( ( N ` T ) <_ ( abs ` A ) <-> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) ) )
61 60 biimpar 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ ( abs ` A ) ) ) -> ( N ` T ) <_ ( abs ` A ) )
62 57 61 syldan 
 |-  ( ( ( T : X --> Y /\ A e. RR ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ ( abs ` A ) )
63 62 3impa 
 |-  ( ( T : X --> Y /\ A e. RR /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ ( abs ` A ) )