| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nmoxr.1 |
|- X = ( BaseSet ` U ) |
| 2 |
|
nmoxr.2 |
|- Y = ( BaseSet ` W ) |
| 3 |
|
nmoxr.3 |
|- N = ( U normOpOLD W ) |
| 4 |
|
0xr |
|- 0 e. RR* |
| 5 |
4
|
a1i |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> 0 e. RR* ) |
| 6 |
|
simp2 |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> W e. NrmCVec ) |
| 7 |
|
eqid |
|- ( 0vec ` U ) = ( 0vec ` U ) |
| 8 |
1 7
|
nvzcl |
|- ( U e. NrmCVec -> ( 0vec ` U ) e. X ) |
| 9 |
|
ffvelcdm |
|- ( ( T : X --> Y /\ ( 0vec ` U ) e. X ) -> ( T ` ( 0vec ` U ) ) e. Y ) |
| 10 |
8 9
|
sylan2 |
|- ( ( T : X --> Y /\ U e. NrmCVec ) -> ( T ` ( 0vec ` U ) ) e. Y ) |
| 11 |
10
|
ancoms |
|- ( ( U e. NrmCVec /\ T : X --> Y ) -> ( T ` ( 0vec ` U ) ) e. Y ) |
| 12 |
11
|
3adant2 |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( T ` ( 0vec ` U ) ) e. Y ) |
| 13 |
|
eqid |
|- ( normCV ` W ) = ( normCV ` W ) |
| 14 |
2 13
|
nvcl |
|- ( ( W e. NrmCVec /\ ( T ` ( 0vec ` U ) ) e. Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. RR ) |
| 15 |
6 12 14
|
syl2anc |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. RR ) |
| 16 |
15
|
rexrd |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. RR* ) |
| 17 |
1 2 3
|
nmoxr |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) e. RR* ) |
| 18 |
2 13
|
nvge0 |
|- ( ( W e. NrmCVec /\ ( T ` ( 0vec ` U ) ) e. Y ) -> 0 <_ ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) ) |
| 19 |
6 12 18
|
syl2anc |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> 0 <_ ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) ) |
| 20 |
2 13
|
nmosetre |
|- ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR ) |
| 21 |
|
ressxr |
|- RR C_ RR* |
| 22 |
20 21
|
sstrdi |
|- ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR* ) |
| 23 |
|
eqid |
|- ( normCV ` U ) = ( normCV ` U ) |
| 24 |
1 7 23
|
nmosetn0 |
|- ( U e. NrmCVec -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } ) |
| 25 |
|
supxrub |
|- ( ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR* /\ ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) ) |
| 26 |
22 24 25
|
syl2an |
|- ( ( ( W e. NrmCVec /\ T : X --> Y ) /\ U e. NrmCVec ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) ) |
| 27 |
26
|
3impa |
|- ( ( W e. NrmCVec /\ T : X --> Y /\ U e. NrmCVec ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) ) |
| 28 |
27
|
3comr |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) ) |
| 29 |
1 2 23 13 3
|
nmooval |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) ) |
| 30 |
28 29
|
breqtrrd |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ ( N ` T ) ) |
| 31 |
5 16 17 19 30
|
xrletrd |
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> 0 <_ ( N ` T ) ) |