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		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)$$
10	1	pjbdlni	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\in \mathrm{BndLinOp}$$
11	2	pjbdlni	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{BndLinOp}$$
12	10 11	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)$$
13		pjadj3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$
14	2 13	ax-mp	$$⊢{adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$
15		pjadj3	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
16	1 15	ax-mp	$$⊢{adj}_h\left({\mathrm{proj}}_{ℎ}\left(G\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
17	14 16	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)$$
18	12 17	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)$$
19	9 18	eqtr3di	$$⊢{\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}}_{ℎ}$$