# 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}=\mathrm{BaseSet}\left({U}\right)$
nmosetn0.5 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
nmosetn0.4 ${⊢}{M}={norm}_{CV}\left({U}\right)$
Assertion nmosetn0 ${⊢}{U}\in \mathrm{NrmCVec}\to {N}\left({T}\left({Z}\right)\right)\in \left\{{x}|\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {x}={N}\left({T}\left({y}\right)\right)\right)\right\}$

### Proof

Step Hyp Ref Expression
1 nmosetn0.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmosetn0.5 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
3 nmosetn0.4 ${⊢}{M}={norm}_{CV}\left({U}\right)$
4 1 2 nvzcl ${⊢}{U}\in \mathrm{NrmCVec}\to {Z}\in {X}$
5 2 3 nvz0 ${⊢}{U}\in \mathrm{NrmCVec}\to {M}\left({Z}\right)=0$
6 0le1 ${⊢}0\le 1$
7 5 6 eqbrtrdi ${⊢}{U}\in \mathrm{NrmCVec}\to {M}\left({Z}\right)\le 1$
8 eqid ${⊢}{N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({Z}\right)\right)$
9 7 8 jctir ${⊢}{U}\in \mathrm{NrmCVec}\to \left({M}\left({Z}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({Z}\right)\right)\right)$
10 fveq2 ${⊢}{y}={Z}\to {M}\left({y}\right)={M}\left({Z}\right)$
11 10 breq1d ${⊢}{y}={Z}\to \left({M}\left({y}\right)\le 1↔{M}\left({Z}\right)\le 1\right)$
12 2fveq3 ${⊢}{y}={Z}\to {N}\left({T}\left({y}\right)\right)={N}\left({T}\left({Z}\right)\right)$
13 12 eqeq2d ${⊢}{y}={Z}\to \left({N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)↔{N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({Z}\right)\right)\right)$
14 11 13 anbi12d ${⊢}{y}={Z}\to \left(\left({M}\left({y}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)\right)↔\left({M}\left({Z}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({Z}\right)\right)\right)\right)$
15 14 rspcev ${⊢}\left({Z}\in {X}\wedge \left({M}\left({Z}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({Z}\right)\right)\right)\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)\right)$
16 4 9 15 syl2anc ${⊢}{U}\in \mathrm{NrmCVec}\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)\right)$
17 fvex ${⊢}{N}\left({T}\left({Z}\right)\right)\in \mathrm{V}$
18 eqeq1 ${⊢}{x}={N}\left({T}\left({Z}\right)\right)\to \left({x}={N}\left({T}\left({y}\right)\right)↔{N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)\right)$
19 18 anbi2d ${⊢}{x}={N}\left({T}\left({Z}\right)\right)\to \left(\left({M}\left({y}\right)\le 1\wedge {x}={N}\left({T}\left({y}\right)\right)\right)↔\left({M}\left({y}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)\right)\right)$
20 19 rexbidv ${⊢}{x}={N}\left({T}\left({Z}\right)\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {x}={N}\left({T}\left({y}\right)\right)\right)↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)\right)\right)$
21 17 20 elab ${⊢}{N}\left({T}\left({Z}\right)\right)\in \left\{{x}|\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {x}={N}\left({T}\left({y}\right)\right)\right)\right\}↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {N}\left({T}\left({Z}\right)\right)={N}\left({T}\left({y}\right)\right)\right)$
22 16 21 sylibr ${⊢}{U}\in \mathrm{NrmCVec}\to {N}\left({T}\left({Z}\right)\right)\in \left\{{x}|\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({y}\right)\le 1\wedge {x}={N}\left({T}\left({y}\right)\right)\right)\right\}$