Metamath Proof Explorer

Theorem nmosetre

Description: The set in the supremum of the operator norm definition df-nmoo is a set of reals. (Contributed by NM, 13-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmosetre.2 
|- Y = ( BaseSet ` W )
nmosetre.4 
|- N = ( normCV ` W )
Assertion nmosetre 
|- ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( M ` z ) <_ 1 /\ x = ( N ` ( T ` z ) ) ) } C_ RR )

Proof

Step Hyp Ref Expression
1 nmosetre.2 
 |-  Y = ( BaseSet ` W )
2 nmosetre.4 
 |-  N = ( normCV ` W )
3 ffvelcdm 
 |-  ( ( T : X --> Y /\ z e. X ) -> ( T ` z ) e. Y )
4 1 2 nvcl 
 |-  ( ( W e. NrmCVec /\ ( T ` z ) e. Y ) -> ( N ` ( T ` z ) ) e. RR )
5 3 4 sylan2 
 |-  ( ( W e. NrmCVec /\ ( T : X --> Y /\ z e. X ) ) -> ( N ` ( T ` z ) ) e. RR )
6 5 anassrs 
 |-  ( ( ( W e. NrmCVec /\ T : X --> Y ) /\ z e. X ) -> ( N ` ( T ` z ) ) e. RR )
7 eleq1 
 |-  ( x = ( N ` ( T ` z ) ) -> ( x e. RR <-> ( N ` ( T ` z ) ) e. RR ) )
8 6 7 imbitrrid 
 |-  ( x = ( N ` ( T ` z ) ) -> ( ( ( W e. NrmCVec /\ T : X --> Y ) /\ z e. X ) -> x e. RR ) )
9 8 impcom 
 |-  ( ( ( ( W e. NrmCVec /\ T : X --> Y ) /\ z e. X ) /\ x = ( N ` ( T ` z ) ) ) -> x e. RR )
10 9 adantrl 
 |-  ( ( ( ( W e. NrmCVec /\ T : X --> Y ) /\ z e. X ) /\ ( ( M ` z ) <_ 1 /\ x = ( N ` ( T ` z ) ) ) ) -> x e. RR )
11 10 rexlimdva2 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> ( E. z e. X ( ( M ` z ) <_ 1 /\ x = ( N ` ( T ` z ) ) ) -> x e. RR ) )
12 11 abssdv 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( M ` z ) <_ 1 /\ x = ( N ` ( T ` z ) ) ) } C_ RR )