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_{ℋ} \land T : ℋ ⟶ ℋ) \to {norm}_{op} (T) = 0$

Proof

Step	Hyp	Ref	Expression
1		df-ch0	$⊢ 0_{ℋ} = \{0_{ℎ}\}$
2	1	eqeq2i	$⊢ ℋ = 0_{ℋ} \leftrightarrow ℋ = \{0_{ℎ}\}$
3		feq3	$⊢ ℋ = \{0_{ℎ}\} \to (T : ℋ ⟶ ℋ \leftrightarrow T : ℋ ⟶ \{0_{ℎ}\})$
4	2 3	sylbi	$⊢ ℋ = 0_{ℋ} \to (T : ℋ ⟶ ℋ \leftrightarrow T : ℋ ⟶ \{0_{ℎ}\})$
5		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
6	5	elexi	$⊢ 0_{ℎ} \in V$
7	6	fconst2	$⊢ T : ℋ ⟶ \{0_{ℎ}\} \leftrightarrow T = ℋ \times \{0_{ℎ}\}$
8		df0op2	$⊢ 0_{hop} = ℋ \times 0_{ℋ}$
9	1	xpeq2i	$⊢ ℋ \times 0_{ℋ} = ℋ \times \{0_{ℎ}\}$
10	8 9	eqtri	$⊢ 0_{hop} = ℋ \times \{0_{ℎ}\}$
11	10	eqeq2i	$⊢ T = 0_{hop} \leftrightarrow T = ℋ \times \{0_{ℎ}\}$
12	7 11	bitr4i	$⊢ T : ℋ ⟶ \{0_{ℎ}\} \leftrightarrow T = 0_{hop}$
13	4 12	bitrdi	$⊢ ℋ = 0_{ℋ} \to (T : ℋ ⟶ ℋ \leftrightarrow T = 0_{hop})$
14	13	biimpa	$⊢ (ℋ = 0_{ℋ} \land T : ℋ ⟶ ℋ) \to T = 0_{hop}$
15	14	fveq2d	$⊢ (ℋ = 0_{ℋ} \land T : ℋ ⟶ ℋ) \to {norm}_{op} (T) = {norm}_{op} (0_{hop})$
16		nmop0	$⊢ {norm}_{op} (0_{hop}) = 0$
17	15 16	eqtrdi	$⊢ (ℋ = 0_{ℋ} \land T : ℋ ⟶ ℋ) \to {norm}_{op} (T) = 0$