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 )