Theorem ho0val

Description: Value of the zero Hilbert space operator (null projector). Remark in Beran p. 111. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	ho0val	$$⊢A\in \mathscr{H}\to 0_{\mathrm{hop}}\left(A\right)=0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		choc1	$$⊢\perp \left(\mathscr{H}\right)=0_{\mathscr{H}}$$
2	1	fveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(\mathscr{H}\right)\right)={\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)$$
3		df-h0op	$$⊢0_{\mathrm{hop}}={\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)$$
4	2 3	eqtr4i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(\mathscr{H}\right)\right)=0_{\mathrm{hop}}$$
5	4	fveq1i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(\mathscr{H}\right)\right)\left(A\right)=0_{\mathrm{hop}}\left(A\right)$$
6		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
7		pjo	$$⊢\left(\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)$$
8	6 7	mpan	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\perp \left(\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)$$
9	5 8	syl5eqr	$$⊢A\in \mathscr{H}\to 0_{\mathrm{hop}}\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)$$
10	6	pjhcli	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\in \mathscr{H}$$
11		hvsubid	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)=0_{ℎ}$$
12	10 11	syl	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)=0_{ℎ}$$
13	9 12	eqtrd	$$⊢A\in \mathscr{H}\to 0_{\mathrm{hop}}\left(A\right)=0_{ℎ}$$