Theorem pjordi

Description: The definition of projector ordering in Halmos p. 42 is equivalent to the definition of projector ordering in Beran p. 110. (We will usually express projector ordering with the even simpler equivalent G C_ H ; see 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	pjordi	$$⊢\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 {\mathrm{proj}}_{ℎ}\left(G\right)\left[\mathscr{H}\right]\subseteq {\mathrm{proj}}_{ℎ}\left(H\right)\left[\mathscr{H}\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	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$$
4	1	pjfoi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}\underset{onto}{⟶}G$$
5		foima	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}\underset{onto}{⟶}G\to {\mathrm{proj}}_{ℎ}\left(G\right)\left[\mathscr{H}\right]=G$$
6	4 5	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left[\mathscr{H}\right]=G$$
7	2	pjfoi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H$$
8		foima	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}\underset{onto}{⟶}H\to {\mathrm{proj}}_{ℎ}\left(H\right)\left[\mathscr{H}\right]=H$$
9	7 8	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left[\mathscr{H}\right]=H$$
10	6 9	sseq12i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left[\mathscr{H}\right]\subseteq {\mathrm{proj}}_{ℎ}\left(H\right)\left[\mathscr{H}\right]\leftrightarrow G\subseteq H$$
11	3 10	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 {\mathrm{proj}}_{ℎ}\left(G\right)\left[\mathscr{H}\right]\subseteq {\mathrm{proj}}_{ℎ}\left(H\right)\left[\mathscr{H}\right]$$