# Metamath Proof Explorer

## Theorem nmoo0

Description: The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoo0.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
nmoo0.0 ${⊢}{Z}={U}{0}_{\mathrm{op}}{W}$
Assertion nmoo0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {N}\left({Z}\right)=0$

### Proof

Step Hyp Ref Expression
1 nmoo0.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
2 nmoo0.0 ${⊢}{Z}={U}{0}_{\mathrm{op}}{W}$
3 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
4 eqid ${⊢}\mathrm{BaseSet}\left({W}\right)=\mathrm{BaseSet}\left({W}\right)$
5 3 4 2 0oo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)$
6 eqid ${⊢}{norm}_{CV}\left({U}\right)={norm}_{CV}\left({U}\right)$
7 eqid ${⊢}{norm}_{CV}\left({W}\right)={norm}_{CV}\left({W}\right)$
8 3 4 6 7 1 nmooval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {Z}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)\right)\to {N}\left({Z}\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({Z}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
9 5 8 mpd3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {N}\left({Z}\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({Z}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
10 df-sn ${⊢}\left\{0\right\}=\left\{{x}|{x}=0\right\}$
11 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
12 3 11 nvzcl ${⊢}{U}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({U}\right)\in \mathrm{BaseSet}\left({U}\right)$
13 11 6 nvz0 ${⊢}{U}\in \mathrm{NrmCVec}\to {norm}_{CV}\left({U}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)=0$
14 0le1 ${⊢}0\le 1$
15 13 14 eqbrtrdi ${⊢}{U}\in \mathrm{NrmCVec}\to {norm}_{CV}\left({U}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)\le 1$
16 fveq2 ${⊢}{z}={0}_{\mathrm{vec}}\left({U}\right)\to {norm}_{CV}\left({U}\right)\left({z}\right)={norm}_{CV}\left({U}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)$
17 16 breq1d ${⊢}{z}={0}_{\mathrm{vec}}\left({U}\right)\to \left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1↔{norm}_{CV}\left({U}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)\le 1\right)$
18 17 rspcev ${⊢}\left({0}_{\mathrm{vec}}\left({U}\right)\in \mathrm{BaseSet}\left({U}\right)\wedge {norm}_{CV}\left({U}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)\le 1\right)\to \exists {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{norm}_{CV}\left({U}\right)\left({z}\right)\le 1$
19 12 15 18 syl2anc ${⊢}{U}\in \mathrm{NrmCVec}\to \exists {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{norm}_{CV}\left({U}\right)\left({z}\right)\le 1$
20 19 biantrurd ${⊢}{U}\in \mathrm{NrmCVec}\to \left({x}=0↔\left(\exists {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}=0\right)\right)$
21 20 adantr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({x}=0↔\left(\exists {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}=0\right)\right)$
22 eqid ${⊢}{0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
23 3 22 2 0oval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {Z}\left({z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
24 23 3expa ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {Z}\left({z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
25 24 fveq2d ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {norm}_{CV}\left({W}\right)\left({Z}\left({z}\right)\right)={norm}_{CV}\left({W}\right)\left({0}_{\mathrm{vec}}\left({W}\right)\right)$
26 22 7 nvz0 ${⊢}{W}\in \mathrm{NrmCVec}\to {norm}_{CV}\left({W}\right)\left({0}_{\mathrm{vec}}\left({W}\right)\right)=0$
27 26 ad2antlr ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {norm}_{CV}\left({W}\right)\left({0}_{\mathrm{vec}}\left({W}\right)\right)=0$
28 25 27 eqtrd ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {norm}_{CV}\left({W}\right)\left({Z}\left({z}\right)\right)=0$
29 28 eqeq2d ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({x}={norm}_{CV}\left({W}\right)\left({Z}\left({z}\right)\right)↔{x}=0\right)$
30 29 anbi2d ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left(\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({Z}\left({z}\right)\right)\right)↔\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}=0\right)\right)$
31 30 rexbidva ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\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({Z}\left({z}\right)\right)\right)↔\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}=0\right)\right)$
32 r19.41v ${⊢}\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}=0\right)↔\left(\exists {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}=0\right)$
33 31 32 syl6rbb ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left(\left(\exists {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}=0\right)↔\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({Z}\left({z}\right)\right)\right)\right)$
34 21 33 bitrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({x}=0↔\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({Z}\left({z}\right)\right)\right)\right)$
35 34 abbidv ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left\{{x}|{x}=0\right\}=\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({Z}\left({z}\right)\right)\right)\right\}$
36 10 35 syl5req ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\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({Z}\left({z}\right)\right)\right)\right\}=\left\{0\right\}$
37 36 supeq1d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\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({Z}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{0\right\},{ℝ}^{*},<\right)$
38 9 37 eqtrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {N}\left({Z}\right)=sup\left(\left\{0\right\},{ℝ}^{*},<\right)$
39 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
40 0xr ${⊢}0\in {ℝ}^{*}$
41 supsn ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$
42 39 40 41 mp2an ${⊢}sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$
43 38 42 syl6eq ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {N}\left({Z}\right)=0$