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\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\leftrightarrow 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)\leftrightarrow 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)\leftrightarrow \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\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\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)\leftrightarrow 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)\leftrightarrow \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\left(M\left(y\right)\le 1\wedge x=N\left(T\left(y\right)\right)\right)\leftrightarrow \exists y\in X\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\left(M\left(y\right)\le 1\wedge x=N\left(T\left(y\right)\right)\right)\right\}\leftrightarrow \exists y\in X\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\left(M\left(y\right)\le 1\wedge x=N\left(T\left(y\right)\right)\right)\right\}$$