Metamath Proof Explorer


Theorem nmop0h

Description: The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ~H =/= 0H in nmopun .) (Contributed by NM, 24-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmop0h ( ( ℋ = 0𝑇 : ℋ ⟶ ℋ ) → ( normop𝑇 ) = 0 )

Proof

Step Hyp Ref Expression
1 df-ch0 0 = { 0 }
2 1 eqeq2i ( ℋ = 0 ↔ ℋ = { 0 } )
3 feq3 ( ℋ = { 0 } → ( 𝑇 : ℋ ⟶ ℋ ↔ 𝑇 : ℋ ⟶ { 0 } ) )
4 2 3 sylbi ( ℋ = 0 → ( 𝑇 : ℋ ⟶ ℋ ↔ 𝑇 : ℋ ⟶ { 0 } ) )
5 ax-hv0cl 0 ∈ ℋ
6 5 elexi 0 ∈ V
7 6 fconst2 ( 𝑇 : ℋ ⟶ { 0 } ↔ 𝑇 = ( ℋ × { 0 } ) )
8 df0op2 0hop = ( ℋ × 0 )
9 1 xpeq2i ( ℋ × 0 ) = ( ℋ × { 0 } )
10 8 9 eqtri 0hop = ( ℋ × { 0 } )
11 10 eqeq2i ( 𝑇 = 0hop𝑇 = ( ℋ × { 0 } ) )
12 7 11 bitr4i ( 𝑇 : ℋ ⟶ { 0 } ↔ 𝑇 = 0hop )
13 4 12 bitrdi ( ℋ = 0 → ( 𝑇 : ℋ ⟶ ℋ ↔ 𝑇 = 0hop ) )
14 13 biimpa ( ( ℋ = 0𝑇 : ℋ ⟶ ℋ ) → 𝑇 = 0hop )
15 14 fveq2d ( ( ℋ = 0𝑇 : ℋ ⟶ ℋ ) → ( normop𝑇 ) = ( normop ‘ 0hop ) )
16 nmop0 ( normop ‘ 0hop ) = 0
17 15 16 eqtrdi ( ( ℋ = 0𝑇 : ℋ ⟶ ℋ ) → ( normop𝑇 ) = 0 )