Theorem pjssposi

Description: Projector ordering can be expressed by the subset relationship between their projection subspaces. (i)<->(iii) of Theorem 29.2 of Halmos p. 48. (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	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$$

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	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\in \mathscr{H}$$
4		normcl	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\in ℝ$$
5	3 4	syl	$$⊢x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\in ℝ$$
6	5	resqcld	$$⊢x\in \mathscr{H}\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2\in ℝ$$
7	1	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}$$
8		normcl	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\in ℝ$$
9	7 8	syl	$$⊢x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\in ℝ$$
10	9	resqcld	$$⊢x\in \mathscr{H}\to {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2\in ℝ$$
11	6 10	subge0d	$$⊢x\in \mathscr{H}\to \left(0\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2\right)$$
12	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
13	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
14		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)$$
15	12 13 14	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)$$
16	15	oveq1d	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}x$$
17		id	$$⊢x\in \mathscr{H}\to x\in \mathscr{H}$$
18		his2sub	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}x=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)-\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)$$
19	3 7 17 18	syl3anc	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}x=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)-\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)$$
20	2	pjinormi	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}x={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2$$
21	1	pjinormi	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){\cdot }_{\mathrm{ih}}x={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2$$
22	20 21	oveq12d	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)-\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2$$
23	16 19 22	3eqtrd	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2$$
24	23	breq2d	$$⊢x\in \mathscr{H}\to \left(0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x\leftrightarrow 0\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2\right)$$
25		normge0	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
26	7 25	syl	$$⊢x\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
27		normge0	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$
28	3 27	syl	$$⊢x\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$
29	9 5 26 28	le2sqd	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)}^2\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)}^2\right)$$
30	11 24 29	3bitr4d	$$⊢x\in \mathscr{H}\to \left(0\le \left({\mathrm{proj}}_{ℎ}\left(H\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}x\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)$$
31	30	ralbiia	$$⊢\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 \forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$
32	1 2	pjnormssi	$$⊢G\subseteq H\leftrightarrow \forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$
33	31 32	bitr4i	$$⊢\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$$