Theorem nmoofval

Description: The operator norm function. (Contributed by NM, 6-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoofval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	nmoofval.2	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
	nmoofval.3	$$⊢L={norm}_{CV}\left(U\right)$$
	nmoofval.4	$$⊢M={norm}_{CV}\left(W\right)$$
	nmoofval.6	$$⊢N=U{normOp}_{\mathrm{OLD}}W$$
Assertion	nmoofval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to N=\left(t\in \left(Y^X\right)⟼sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmoofval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nmoofval.2	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
3		nmoofval.3	$$⊢L={norm}_{CV}\left(U\right)$$
4		nmoofval.4	$$⊢M={norm}_{CV}\left(W\right)$$
5		nmoofval.6	$$⊢N=U{normOp}_{\mathrm{OLD}}W$$
6		fveq2	$$⊢u=U\to \mathrm{BaseSet}\left(u\right)=\mathrm{BaseSet}\left(U\right)$$
7	6 1	eqtr4di	$$⊢u=U\to \mathrm{BaseSet}\left(u\right)=X$$
8	7	oveq2d	$$⊢u=U\to {\mathrm{BaseSet}\left(w\right)}^{\mathrm{BaseSet}\left(u\right)}={\mathrm{BaseSet}\left(w\right)}^X$$
9		fveq2	$$⊢u=U\to {norm}_{CV}\left(u\right)={norm}_{CV}\left(U\right)$$
10	9 3	eqtr4di	$$⊢u=U\to {norm}_{CV}\left(u\right)=L$$
11	10	fveq1d	$$⊢u=U\to {norm}_{CV}\left(u\right)\left(z\right)=L\left(z\right)$$
12	11	breq1d	$$⊢u=U\to \left({norm}_{CV}\left(u\right)\left(z\right)\le 1\leftrightarrow L\left(z\right)\le 1\right)$$
13	12	anbi1d	$$⊢u=U\to \left(\left({norm}_{CV}\left(u\right)\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\leftrightarrow \left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right)$$
14	7 13	rexeqbidv	$$⊢u=U\to \left(\exists z\in \mathrm{BaseSet}\left(u\right)\left({norm}_{CV}\left(u\right)\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\leftrightarrow \exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right)$$
15	14	abbidv	$$⊢u=U\to \left\{x|\exists z\in \mathrm{BaseSet}\left(u\right)\left({norm}_{CV}\left(u\right)\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\}=\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\}$$
16	15	supeq1d	$$⊢u=U\to sup\left(\left\{x|\exists z\in \mathrm{BaseSet}\left(u\right)\left({norm}_{CV}\left(u\right)\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)$$
17	8 16	mpteq12dv	$$⊢u=U\to \left(t\in \left({\mathrm{BaseSet}\left(w\right)}^{\mathrm{BaseSet}\left(u\right)}\right)⟼sup\left(\left\{x|\exists z\in \mathrm{BaseSet}\left(u\right)\left({norm}_{CV}\left(u\right)\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)=\left(t\in \left({\mathrm{BaseSet}\left(w\right)}^X\right)⟼sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$
18		fveq2	$$⊢w=W\to \mathrm{BaseSet}\left(w\right)=\mathrm{BaseSet}\left(W\right)$$
19	18 2	eqtr4di	$$⊢w=W\to \mathrm{BaseSet}\left(w\right)=Y$$
20	19	oveq1d	$$⊢w=W\to {\mathrm{BaseSet}\left(w\right)}^X=Y^X$$
21		fveq2	$$⊢w=W\to {norm}_{CV}\left(w\right)={norm}_{CV}\left(W\right)$$
22	21 4	eqtr4di	$$⊢w=W\to {norm}_{CV}\left(w\right)=M$$
23	22	fveq1d	$$⊢w=W\to {norm}_{CV}\left(w\right)\left(t\left(z\right)\right)=M\left(t\left(z\right)\right)$$
24	23	eqeq2d	$$⊢w=W\to \left(x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\leftrightarrow x=M\left(t\left(z\right)\right)\right)$$
25	24	anbi2d	$$⊢w=W\to \left(\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\leftrightarrow \left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right)$$
26	25	rexbidv	$$⊢w=W\to \left(\exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\leftrightarrow \exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right)$$
27	26	abbidv	$$⊢w=W\to \left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\}=\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right\}$$
28	27	supeq1d	$$⊢w=W\to sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)$$
29	20 28	mpteq12dv	$$⊢w=W\to \left(t\in \left({\mathrm{BaseSet}\left(w\right)}^X\right)⟼sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)=\left(t\in \left(Y^X\right)⟼sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$
30		df-nmoo	$$⊢{normOp}_{\mathrm{OLD}}=\left(u\in \mathrm{NrmCVec},w\in \mathrm{NrmCVec}⟼\left(t\in \left({\mathrm{BaseSet}\left(w\right)}^{\mathrm{BaseSet}\left(u\right)}\right)⟼sup\left(\left\{x|\exists z\in \mathrm{BaseSet}\left(u\right)\left({norm}_{CV}\left(u\right)\left(z\right)\le 1\wedge x={norm}_{CV}\left(w\right)\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)$$
31		ovex	$$⊢Y^X\in \mathrm{V}$$
32	31	mptex	$$⊢\left(t\in \left(Y^X\right)⟼sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\in \mathrm{V}$$
33	17 29 30 32	ovmpo	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to U{normOp}_{\mathrm{OLD}}W=\left(t\in \left(Y^X\right)⟼sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$
34	5 33	eqtrid	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to N=\left(t\in \left(Y^X\right)⟼sup\left(\left\{x|\exists z\in X\left(L\left(z\right)\le 1\wedge x=M\left(t\left(z\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$