# 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 ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}$

### Proof

Step Hyp Ref Expression
1 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
2 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
3 0le1 ${⊢}0\le 1$
4 2 3 eqbrtri ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)\le 1$
5 eqid ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)$
6 4 5 pm3.2i ${⊢}\left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\right)$
7 fveq2 ${⊢}{y}={0}_{ℎ}\to {norm}_{ℎ}\left({y}\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
8 7 breq1d ${⊢}{y}={0}_{ℎ}\to \left({norm}_{ℎ}\left({y}\right)\le 1↔{norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\right)$
9 2fveq3 ${⊢}{y}={0}_{ℎ}\to {norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)$
10 9 eqeq2d ${⊢}{y}={0}_{ℎ}\to \left({norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)↔{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\right)$
11 8 10 anbi12d ${⊢}{y}={0}_{ℎ}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\right)\right)$
12 11 rspcev ${⊢}\left({0}_{ℎ}\in ℋ\wedge \left({norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\right)\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
13 1 6 12 mp2an ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
14 fvex ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in \mathrm{V}$
15 eqeq1 ${⊢}{x}={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\to \left({x}={norm}_{ℎ}\left({T}\left({y}\right)\right)↔{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
16 15 anbi2d ${⊢}{x}={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
17 16 rexbidv ${⊢}{x}={norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
18 14 17 elab ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
19 13 18 mpbir ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}$