Metamath Proof Explorer

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}\phantom{\rule{.4em}{0ex}}\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 syl6eqr ${⊢}{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 syl6eqr ${⊢}{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↔{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)↔\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)\phantom{\rule{.4em}{0ex}}\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)↔\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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 syl6eqr ${⊢}{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 syl6eqr ${⊢}{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)↔{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)↔\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}\phantom{\rule{.4em}{0ex}}\left({L}\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({w}\right)\left({t}\left({z}\right)\right)\right)↔\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\left({L}\left({z}\right)\le 1\wedge {x}={M}\left({t}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$
34 5 33 syl5eq ${⊢}\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}\phantom{\rule{.4em}{0ex}}\left({L}\left({z}\right)\le 1\wedge {x}={M}\left({t}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$