Theorem df0op2

Description: Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df0op2	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times 0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
2		ffn	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\to 0_{\mathrm{hop}}Fn\mathscr{H}$$
3	1 2	ax-mp	$$⊢0_{\mathrm{hop}}Fn\mathscr{H}$$
4		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
5	4	rgen	$$⊢\forall x\in \mathscr{H}{0}_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
6		fconstfv	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\left\{0_{ℎ}\right\}\leftrightarrow \left(0_{\mathrm{hop}}Fn\mathscr{H}\wedge \forall x\in \mathscr{H}{0}_{\mathrm{hop}}\left(x\right)=0_{ℎ}\right)$$
7	3 5 6	mpbir2an	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\left\{0_{ℎ}\right\}$$
8		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
9	8	elexi	$$⊢0_{ℎ}\in \mathrm{V}$$
10	9	fconst2	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\left\{0_{ℎ}\right\}\leftrightarrow 0_{\mathrm{hop}}=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
11	7 10	mpbi	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
12		df-ch0	$$⊢0_{\mathscr{H}}=\left\{0_{ℎ}\right\}$$
13	12	xpeq2i	$$⊢\mathscr{H}\times 0_{\mathscr{H}}=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
14	11 13	eqtr4i	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times 0_{\mathscr{H}}$$