# Metamath Proof Explorer

## Theorem nmop0

Description: The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmop0 ${⊢}{norm}_{\mathrm{op}}\left({0}_{\mathrm{hop}}\right)=0$

### Proof

Step Hyp Ref Expression
1 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
2 nmopval ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({0}_{\mathrm{hop}}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
3 1 2 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({0}_{\mathrm{hop}}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
4 ho0val ${⊢}{y}\in ℋ\to {0}_{\mathrm{hop}}\left({y}\right)={0}_{ℎ}$
5 4 fveq2d ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
6 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
7 5 6 syl6eq ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)=0$
8 7 eqeq2d ${⊢}{y}\in ℋ\to \left({x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)↔{x}=0\right)$
9 8 anbi2d ${⊢}{y}\in ℋ\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=0\right)\right)$
10 9 rexbiia ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=0\right)$
11 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
12 0le1 ${⊢}0\le 1$
13 fveq2 ${⊢}{y}={0}_{ℎ}\to {norm}_{ℎ}\left({y}\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
14 13 6 syl6eq ${⊢}{y}={0}_{ℎ}\to {norm}_{ℎ}\left({y}\right)=0$
15 14 breq1d ${⊢}{y}={0}_{ℎ}\to \left({norm}_{ℎ}\left({y}\right)\le 1↔0\le 1\right)$
16 15 rspcev ${⊢}\left({0}_{ℎ}\in ℋ\wedge 0\le 1\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)\le 1$
17 11 12 16 mp2an ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)\le 1$
18 r19.41v ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=0\right)↔\left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=0\right)$
19 17 18 mpbiran ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=0\right)↔{x}=0$
20 10 19 bitri ${⊢}\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)↔{x}=0$
21 20 abbii ${⊢}\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)\right\}=\left\{{x}|{x}=0\right\}$
22 df-sn ${⊢}\left\{0\right\}=\left\{{x}|{x}=0\right\}$
23 21 22 eqtr4i ${⊢}\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)\right\}=\left\{0\right\}$
24 23 supeq1i ${⊢}sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{0\right\},{ℝ}^{*},<\right)$
25 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
26 0xr ${⊢}0\in {ℝ}^{*}$
27 supsn ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$
28 25 26 27 mp2an ${⊢}sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$
29 3 24 28 3eqtri ${⊢}{norm}_{\mathrm{op}}\left({0}_{\mathrm{hop}}\right)=0$