Theorem pjssdif1i

Description: A necessary and sufficient condition for the difference between two projectors to be a projector. Part 1 of Theorem 29.3 of Halmos p. 48 (shortened with pjssposi ). (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjssdif1i	$$⊢G\subseteq H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	pjssdif2i	$$⊢G\subseteq H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)$$
4		pjmfn	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}$$
5	1	choccli	$$⊢\perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	2 5	chincli	$$⊢H\cap \perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7		fnfvelrn	$$⊢\left({\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}\wedge H\cap \perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
8	4 6 7	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
9		eleq1	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\right)$$
10	8 9	mpbiri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\to {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
11		fvelrnb	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow \exists x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)$$
12	4 11	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow \exists x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)$$
13		pjige0	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in \mathscr{H}\right)\to 0\le {\mathrm{proj}}_{ℎ}\left(x\right)\left(y\right){\cdot }_{\mathrm{ih}}y$$
14	13	adantlr	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\wedge y\in \mathscr{H}\right)\to 0\le {\mathrm{proj}}_{ℎ}\left(x\right)\left(y\right){\cdot }_{\mathrm{ih}}y$$
15		fveq1	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(x\right)\left(y\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right)$$
16	15	oveq1d	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(x\right)\left(y\right){\cdot }_{\mathrm{ih}}y=\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y$$
17	16	breq2d	$$⊢{\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\to \left(0\le {\mathrm{proj}}_{ℎ}\left(x\right)\left(y\right){\cdot }_{\mathrm{ih}}y\leftrightarrow 0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y\right)$$
18	17	ad2antlr	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\wedge y\in \mathscr{H}\right)\to \left(0\le {\mathrm{proj}}_{ℎ}\left(x\right)\left(y\right){\cdot }_{\mathrm{ih}}y\leftrightarrow 0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y\right)$$
19	14 18	mpbid	$$⊢\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\wedge y\in \mathscr{H}\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y$$
20	19	ralrimiva	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\to \forall y\in \mathscr{H}0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y$$
21	20	rexlimiva	$$⊢\exists x\in {\mathbf{C}}_{\mathscr{H}}{\mathrm{proj}}_{ℎ}\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\to \forall y\in \mathscr{H}0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y$$
22	12 21	sylbi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \forall y\in \mathscr{H}0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y$$
23	1 2	pjssposi	$$⊢\forall y\in \mathscr{H}0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y\leftrightarrow G\subseteq H$$
24	23 3	bitri	$$⊢\forall y\in \mathscr{H}0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(y\right){\cdot }_{\mathrm{ih}}y\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)$$
25	22 24	sylib	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)$$
26	10 25	impbii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
27	3 26	bitri	$$⊢G\subseteq H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$