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

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 )