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	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
4		df-ch0	$$⊢0_{\mathscr{H}}=\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_{\mathscr{H}}=\left\{0_{\mathrm{vec}}\left(U\right)\right\}$$
8	3 7	xpeq12i	$$⊢\mathscr{H}\times 0_{\mathscr{H}}=\mathrm{BaseSet}\left(U\right)\times \left\{0_{\mathrm{vec}}\left(U\right)\right\}$$
9		df0op2	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times 0_{\mathscr{H}}$$
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)\times \left\{0_{\mathrm{vec}}\left(U\right)\right\}$$
14	10 10 13	mp2an	$$⊢Z=\mathrm{BaseSet}\left(U\right)\times \left\{0_{\mathrm{vec}}\left(U\right)\right\}$$
15	8 9 14	3eqtr4i	$$⊢0_{\mathrm{hop}}=Z$$