# 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 ) ) ) } )`