# Metamath Proof Explorer

## Theorem nmooval

Description: The operator norm function. (Contributed by NM, 27-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 nmooval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\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)$

### 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 2 fvexi ${⊢}{Y}\in \mathrm{V}$
7 1 fvexi ${⊢}{X}\in \mathrm{V}$
8 6 7 elmap ${⊢}{T}\in \left({{Y}}^{{X}}\right)↔{T}:{X}⟶{Y}$
9 1 2 3 4 5 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)$
10 9 fveq1d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {N}\left({T}\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)\left({T}\right)$
11 fveq1 ${⊢}{t}={T}\to {t}\left({z}\right)={T}\left({z}\right)$
12 11 fveq2d ${⊢}{t}={T}\to {M}\left({t}\left({z}\right)\right)={M}\left({T}\left({z}\right)\right)$
13 12 eqeq2d ${⊢}{t}={T}\to \left({x}={M}\left({t}\left({z}\right)\right)↔{x}={M}\left({T}\left({z}\right)\right)\right)$
14 13 anbi2d ${⊢}{t}={T}\to \left(\left({L}\left({z}\right)\le 1\wedge {x}={M}\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)$
15 14 rexbidv ${⊢}{t}={T}\to \left(\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)↔\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)$
16 15 abbidv ${⊢}{t}={T}\to \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\}=\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\}$
17 16 supeq1d ${⊢}{t}={T}\to 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)=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)$
18 eqid ${⊢}\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)=\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)$
19 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
20 19 supex ${⊢}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)\in \mathrm{V}$
21 17 18 20 fvmpt ${⊢}{T}\in \left({{Y}}^{{X}}\right)\to \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)\left({T}\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)$
22 10 21 sylan9eq ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {T}\in \left({{Y}}^{{X}}\right)\right)\to {N}\left({T}\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)$
23 8 22 sylan2br ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\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)$
24 23 3impa ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\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)$