# Metamath Proof Explorer

## Theorem hh0oi

Description: The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hhnmo.1 ${⊢}{U}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
hh0o.2 ${⊢}{Z}={U}{0}_{\mathrm{op}}{U}$
Assertion hh0oi ${⊢}{0}_{\mathrm{hop}}={Z}$

### Proof

Step Hyp Ref Expression
1 hhnmo.1 ${⊢}{U}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
2 hh0o.2 ${⊢}{Z}={U}{0}_{\mathrm{op}}{U}$
3 1 hhba ${⊢}ℋ=\mathrm{BaseSet}\left({U}\right)$
4 df-ch0 ${⊢}{0}_{ℋ}=\left\{{0}_{ℎ}\right\}$
5 1 hh0v ${⊢}{0}_{ℎ}={0}_{\mathrm{vec}}\left({U}\right)$
6 5 sneqi ${⊢}\left\{{0}_{ℎ}\right\}=\left\{{0}_{\mathrm{vec}}\left({U}\right)\right\}$
7 4 6 eqtri ${⊢}{0}_{ℋ}=\left\{{0}_{\mathrm{vec}}\left({U}\right)\right\}$
8 3 7 xpeq12i ${⊢}ℋ×{0}_{ℋ}=\mathrm{BaseSet}\left({U}\right)×\left\{{0}_{\mathrm{vec}}\left({U}\right)\right\}$
9 df0op2 ${⊢}{0}_{\mathrm{hop}}=ℋ×{0}_{ℋ}$
10 1 hhnv ${⊢}{U}\in \mathrm{NrmCVec}$
11 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
12 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
13 11 12 2 0ofval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {U}\in \mathrm{NrmCVec}\right)\to {Z}=\mathrm{BaseSet}\left({U}\right)×\left\{{0}_{\mathrm{vec}}\left({U}\right)\right\}$
14 10 10 13 mp2an ${⊢}{Z}=\mathrm{BaseSet}\left({U}\right)×\left\{{0}_{\mathrm{vec}}\left({U}\right)\right\}$
15 8 9 14 3eqtr4i ${⊢}{0}_{\mathrm{hop}}={Z}$