# Metamath Proof Explorer

## Theorem nmopsetn0

Description: The set in the supremum of the operator norm definition df-nmop is nonempty. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopsetn0
`|- ( normh ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) }`

### Proof

Step Hyp Ref Expression
1 ax-hv0cl
` |-  0h e. ~H`
2 norm0
` |-  ( normh ` 0h ) = 0`
3 0le1
` |-  0 <_ 1`
4 2 3 eqbrtri
` |-  ( normh ` 0h ) <_ 1`
5 eqid
` |-  ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` 0h ) )`
6 4 5 pm3.2i
` |-  ( ( normh ` 0h ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` 0h ) ) )`
7 fveq2
` |-  ( y = 0h -> ( normh ` y ) = ( normh ` 0h ) )`
8 7 breq1d
` |-  ( y = 0h -> ( ( normh ` y ) <_ 1 <-> ( normh ` 0h ) <_ 1 ) )`
9 2fveq3
` |-  ( y = 0h -> ( normh ` ( T ` y ) ) = ( normh ` ( T ` 0h ) ) )`
10 9 eqeq2d
` |-  ( y = 0h -> ( ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) <-> ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` 0h ) ) ) )`
11 8 10 anbi12d
` |-  ( y = 0h -> ( ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) ) <-> ( ( normh ` 0h ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` 0h ) ) ) ) )`
12 11 rspcev
` |-  ( ( 0h e. ~H /\ ( ( normh ` 0h ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` 0h ) ) ) ) -> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) ) )`
13 1 6 12 mp2an
` |-  E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) )`
14 fvex
` |-  ( normh ` ( T ` 0h ) ) e. _V`
15 eqeq1
` |-  ( x = ( normh ` ( T ` 0h ) ) -> ( x = ( normh ` ( T ` y ) ) <-> ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) ) )`
16 15 anbi2d
` |-  ( x = ( normh ` ( T ` 0h ) ) -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) ) ) )`
17 16 rexbidv
` |-  ( x = ( normh ` ( T ` 0h ) ) -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) ) ) )`
18 14 17 elab
` |-  ( ( normh ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` 0h ) ) = ( normh ` ( T ` y ) ) ) )`
19 13 18 mpbir
` |-  ( normh ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) }`