Theorem pjssdif2i

Description: The projection subspace of the difference between two projectors. Part 2 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	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)$$

Proof

Step	Hyp	Ref	Expression
1		pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
4	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
5		hodval	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
6	3 4 5	mp3an12	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
7	6	adantl	$$⊢\left(G\subseteq H\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
8	2 1	pjssmi	$$⊢x\in \mathscr{H}\to \left(G\subseteq H\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)\right)$$
9	8	impcom	$$⊢\left(G\subseteq H\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)$$
10	7 9	eqtrd	$$⊢\left(G\subseteq H\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)$$
11	10	ralrimiva	$$⊢G\subseteq H\to \forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)$$
12	3 4	hosubfni	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)Fn\mathscr{H}$$
13	1	choccli	$$⊢\perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
14	2 13	chincli	$$⊢H\cap \perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	14	pjfni	$$⊢{\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)Fn\mathscr{H}$$
16		eqfnfv	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)Fn\mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)Fn\mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\leftrightarrow \forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)\right)$$
17	12 15 16	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\leftrightarrow \forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)$$
18	11 17	sylibr	$$⊢G\subseteq H\to {\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)$$
19	14	pjige0i	$$⊢x\in \mathscr{H}\to 0\le {\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
20	19	adantl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\wedge x\in \mathscr{H}\right)\to 0\le {\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
21		fveq1	$$⊢{\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)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)$$
22	21	oveq1d	$$⊢{\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)\right)\left(x\right){\cdot }_{\mathrm{ih}}x={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
23	22	adantr	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
24	20 23	breqtrrd	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\wedge x\in \mathscr{H}\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
25	24	ralrimiva	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\to \forall x\in \mathscr{H}0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
26	1 2	pjssposi	$$⊢\forall x\in \mathscr{H}0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x\leftrightarrow G\subseteq H$$
27	25 26	sylib	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\to G\subseteq H$$
28	18 27	impbii	$$⊢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)$$