| 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 2 3 4 5 6 7
|
nmoub3i |
|- ( ( T : X --> Y /\ A e. RR /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ ( abs ` A ) ) |
| 9 |
8
|
3adant2r |
|- ( ( T : X --> Y /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ ( abs ` A ) ) |
| 10 |
|
absid |
|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A ) |
| 11 |
10
|
3ad2ant2 |
|- ( ( T : X --> Y /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( abs ` A ) = A ) |
| 12 |
9 11
|
breqtrd |
|- ( ( T : X --> Y /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ A ) |