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

Proof

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