Theorem pjci

Description: Two subspaces commute iff their projections commute. Lemma 4 of Kalmbach p. 67. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

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

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	pjclem2	$$⊢G{𝐶}_{\mathscr{H}}H\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
4	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)$$
5	1 2	pjclem3	$$⊢{\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(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
6	2	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	1 6	pjclem4	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)$$
8	5 7	syl	$$⊢{\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(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)$$
9	4 8	oveq12d	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)$$
10		df-iop	$$⊢I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
11	10	coeq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
12	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
13	12	hoid1i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(G\right)$$
14	11 13	eqtr3i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
15	2	pjtoi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
16	15	coeq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
17	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
18	6	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
19	1 17 18	pjsdii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)$$
20	16 19	eqtr3i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)$$
21	14 20	eqtr3i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right){+}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\right)$$
22		inss2	$$⊢G\cap H\subseteq H$$
23	1	choccli	$$⊢\perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
24	2 23	chub2i	$$⊢H\subseteq \perp \left(G\right){\vee }_{\mathscr{H}}H$$
25	22 24	sstri	$$⊢G\cap H\subseteq \perp \left(G\right){\vee }_{\mathscr{H}}H$$
26	1 2	chdmm3i	$$⊢\perp \left(G\cap \perp \left(H\right)\right)=\perp \left(G\right){\vee }_{\mathscr{H}}H$$
27	25 26	sseqtrri	$$⊢G\cap H\subseteq \perp \left(G\cap \perp \left(H\right)\right)$$
28	1 2	chincli	$$⊢G\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
29	1 6	chincli	$$⊢G\cap \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
30	28 29	pjscji	$$⊢G\cap H\subseteq \perp \left(G\cap \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)$$
31	27 30	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)$$
32	9 21 31	3eqtr4g	$$⊢{\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)={\mathrm{proj}}_{ℎ}\left(\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\right)$$
33	28 29	chjcli	$$⊢\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
34	1 33	pj11i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\right)\leftrightarrow G=\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)$$
35	32 34	sylib	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to G=\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)$$
36	1 2	cmbri	$$⊢G{𝐶}_{\mathscr{H}}H\leftrightarrow G=\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)$$
37	35 36	sylibr	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to G{𝐶}_{\mathscr{H}}H$$
38	3 37	impbii	$$⊢G{𝐶}_{\mathscr{H}}H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$