Metamath Proof Explorer

Theorem nmosetn0

Description: The set in the supremum of the operator norm definition df-nmoo is nonempty. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmosetn0.1 
|- X = ( BaseSet ` U )
nmosetn0.5 
|- Z = ( 0vec ` U )
nmosetn0.4 
|- M = ( normCV ` U )
Assertion nmosetn0 
|- ( U e. NrmCVec -> ( N ` ( T ` Z ) ) e. { x | E. y e. X ( ( M ` y ) <_ 1 /\ x = ( N ` ( T ` y ) ) ) } )

Proof

Step Hyp Ref Expression
1 nmosetn0.1 
 |-  X = ( BaseSet ` U )
2 nmosetn0.5 
 |-  Z = ( 0vec ` U )
3 nmosetn0.4 
 |-  M = ( normCV ` U )
4 1 2 nvzcl 
 |-  ( U e. NrmCVec -> Z e. X )
5 2 3 nvz0 
 |-  ( U e. NrmCVec -> ( M ` Z ) = 0 )
6 0le1 
 |-  0 <_ 1
7 5 6 eqbrtrdi 
 |-  ( U e. NrmCVec -> ( M ` Z ) <_ 1 )
8 eqid 
 |-  ( N ` ( T ` Z ) ) = ( N ` ( T ` Z ) )
9 7 8 jctir 
 |-  ( U e. NrmCVec -> ( ( M ` Z ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` Z ) ) ) )
10 fveq2 
 |-  ( y = Z -> ( M ` y ) = ( M ` Z ) )
11 10 breq1d 
 |-  ( y = Z -> ( ( M ` y ) <_ 1 <-> ( M ` Z ) <_ 1 ) )
12 2fveq3 
 |-  ( y = Z -> ( N ` ( T ` y ) ) = ( N ` ( T ` Z ) ) )
13 12 eqeq2d 
 |-  ( y = Z -> ( ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) <-> ( N ` ( T ` Z ) ) = ( N ` ( T ` Z ) ) ) )
14 11 13 anbi12d 
 |-  ( y = Z -> ( ( ( M ` y ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) ) <-> ( ( M ` Z ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` Z ) ) ) ) )
15 14 rspcev 
 |-  ( ( Z e. X /\ ( ( M ` Z ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` Z ) ) ) ) -> E. y e. X ( ( M ` y ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) ) )
16 4 9 15 syl2anc 
 |-  ( U e. NrmCVec -> E. y e. X ( ( M ` y ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) ) )
17 fvex 
 |-  ( N ` ( T ` Z ) ) e. _V
18 eqeq1 
 |-  ( x = ( N ` ( T ` Z ) ) -> ( x = ( N ` ( T ` y ) ) <-> ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) ) )
19 18 anbi2d 
 |-  ( x = ( N ` ( T ` Z ) ) -> ( ( ( M ` y ) <_ 1 /\ x = ( N ` ( T ` y ) ) ) <-> ( ( M ` y ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) ) ) )
20 19 rexbidv 
 |-  ( x = ( N ` ( T ` Z ) ) -> ( E. y e. X ( ( M ` y ) <_ 1 /\ x = ( N ` ( T ` y ) ) ) <-> E. y e. X ( ( M ` y ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) ) ) )
21 17 20 elab 
 |-  ( ( N ` ( T ` Z ) ) e. { x | E. y e. X ( ( M ` y ) <_ 1 /\ x = ( N ` ( T ` y ) ) ) } <-> E. y e. X ( ( M ` y ) <_ 1 /\ ( N ` ( T ` Z ) ) = ( N ` ( T ` y ) ) ) )
22 16 21 sylibr 
 |-  ( U e. NrmCVec -> ( N ` ( T ` Z ) ) e. { x | E. y e. X ( ( M ` y ) <_ 1 /\ x = ( N ` ( T ` y ) ) ) } )