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 ⊢normop⁡0hop=0

Proof

Step Hyp Ref Expression
1 ho0f ⊢0hop:ℋ⟶ℋ
2 nmopval ⊢0hop:ℋ⟶ℋ→normop⁡0hop=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡0hop⁡yℝ*<
3 1 2 ax-mp ⊢normop⁡0hop=supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡0hop⁡yℝ*<
4 ho0val ⊢y∈ℋ→0hop⁡y=0ℎ
5 4 fveq2d ⊢y∈ℋ→normℎ⁡0hop⁡y=normℎ⁡0ℎ
6 norm0 ⊢normℎ⁡0ℎ=0
7 5 6 eqtrdi ⊢y∈ℋ→normℎ⁡0hop⁡y=0
8 7 eqeq2d ⊢y∈ℋ→x=normℎ⁡0hop⁡y↔x=0
9 8 anbi2d ⊢y∈ℋ→normℎ⁡y≤1∧x=normℎ⁡0hop⁡y↔normℎ⁡y≤1∧x=0
10 9 rexbiia ⊢∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡0hop⁡y↔∃y∈ℋnormℎ⁡y≤1∧x=0
11 ax-hv0cl ⊢0ℎ∈ℋ
12 0le1 ⊢0≤1
13 fveq2 ⊢y=0ℎ→normℎ⁡y=normℎ⁡0ℎ
14 13 6 eqtrdi ⊢y=0ℎ→normℎ⁡y=0
15 14 breq1d ⊢y=0ℎ→normℎ⁡y≤1↔0≤1
16 15 rspcev ⊢0ℎ∈ℋ∧0≤1→∃y∈ℋnormℎ⁡y≤1
17 11 12 16 mp2an ⊢∃y∈ℋnormℎ⁡y≤1
18 r19.41v ⊢∃y∈ℋnormℎ⁡y≤1∧x=0↔∃y∈ℋnormℎ⁡y≤1∧x=0
19 17 18 mpbiran ⊢∃y∈ℋnormℎ⁡y≤1∧x=0↔x=0
20 10 19 bitri ⊢∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡0hop⁡y↔x=0
21 20 abbii ⊢x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡0hop⁡y=x|x=0
22 df-sn ⊢0=x|x=0
23 21 22 eqtr4i ⊢x|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡0hop⁡y=0
24 23 supeq1i ⊢supx|∃y∈ℋnormℎ⁡y≤1∧x=normℎ⁡0hop⁡yℝ*<=sup0ℝ*<
25 xrltso ⊢<Orℝ*
26 0xr ⊢0∈ℝ*
27 supsn ⊢<Orℝ*∧0∈ℝ*→sup0ℝ*<=0
28 25 26 27 mp2an ⊢sup0ℝ*<=0
29 3 24 28 3eqtri ⊢normop⁡0hop=0