This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } , ℝ* , < ) )
3 1 2 ax-mp ⊢ ( normop ‘ 0hop ) = sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } , ℝ* , < )
4 ho0val ⊢ ( 𝑦 ∈ ℋ → ( 0hop ‘ 𝑦 ) = 0ℎ )
5 4 fveq2d ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) = ( normℎ ‘ 0ℎ ) )
6 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
7 5 6 eqtrdi ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) = 0 )
8 7 eqeq2d ⊢ ( 𝑦 ∈ ℋ → ( 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ↔ 𝑥 = 0 ) )
9 8 anbi2d ⊢ ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ) )
10 9 rexbiia ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) )
11 ax-hv0cl ⊢ 0ℎ ∈ ℋ
12 0le1 ⊢ 0 ≤ 1
13 fveq2 ⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ 0ℎ ) )
14 13 6 eqtrdi ⊢ ( 𝑦 = 0ℎ → ( normℎ ‘ 𝑦 ) = 0 )
15 14 breq1d ⊢ ( 𝑦 = 0ℎ → ( ( normℎ ‘ 𝑦 ) ≤ 1 ↔ 0 ≤ 1 ) )
16 15 rspcev ⊢ ( ( 0ℎ ∈ ℋ ∧ 0 ≤ 1 ) → ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1 )
17 11 12 16 mp2an ⊢ ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1
18 r19.41v ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ ( ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) )
19 17 18 mpbiran ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = 0 ) ↔ 𝑥 = 0 )
20 10 19 bitri ⊢ ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) ↔ 𝑥 = 0 )
21 20 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } = { 𝑥 ∣ 𝑥 = 0 }
22 df-sn ⊢ { 0 } = { 𝑥 ∣ 𝑥 = 0 }
23 21 22 eqtr4i ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } = { 0 }
24 23 supeq1i ⊢ sup ( { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 0hop ‘ 𝑦 ) ) ) } , ℝ* , < ) = sup ( { 0 } , ℝ* , < )
25 xrltso ⊢ < Or ℝ*
26 0xr ⊢ 0 ∈ ℝ*
27 supsn ⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
28 25 26 27 mp2an ⊢ sup ( { 0 } , ℝ* , < ) = 0
29 3 24 28 3eqtri ⊢ ( normop ‘ 0hop ) = 0