Theorem pjige0

Description: The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjige0	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to 0\le {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
2	1	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right)$$
3	2	oveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}A$$
4	3	breq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left(0\le {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A\leftrightarrow 0\le {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)$$
5	4	imbi2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left(\left(A\in \mathscr{H}\to 0\le {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)\leftrightarrow \left(A\in \mathscr{H}\to 0\le {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)\right)$$
6		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
7	6	elimel	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
8	7	pjige0i	$$⊢A\in \mathscr{H}\to 0\le {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}A$$
9	5 8	dedth	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\in \mathscr{H}\to 0\le {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)$$
10	9	imp	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to 0\le {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A$$