Theorem pjcmul1i

Description: A necessary and sufficient condition for the product of two projectors to be a projector is that the projectors commute. Part 1 of Theorem 1 of AkhiezerGlazman p. 65. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjclem1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjcmul1i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	pjclem4	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$
4		pjmfn	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}$$
5	1 2	chincli	$$⊢G\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
6		fnfvelrn	$$⊢\left({\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}\wedge G\cap H\in {\mathbf{C}}_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(G\cap H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
7	4 5 6	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
8	3 7	eqeltrdi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
9	1	pjbdlni	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{BndLinOp}$$
10	2	pjbdlni	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{BndLinOp}$$
11	9 10	adjcoi	$$⊢{adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)={adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\circ {adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\right)$$
12		pjadj3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$
13	2 12	ax-mp	$$⊢{adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$
14		pjadj3	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
15	1 14	ax-mp	$$⊢{adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
16	13 15	coeq12i	$$⊢{adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\circ {adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
17	11 16	eqtri	$$⊢{adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
18		pjadj2	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)$$
19	17 18	syl5reqr	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
20	8 19	impbii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$