Theorem pjclem2

Description: Lemma for projection commutation theorem. (Contributed by NM, 17-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	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)$$

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		incom	$$⊢G\cap H=H\cap G$$
4	3	fveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap H\right)={\mathrm{proj}}_{ℎ}\left(H\cap G\right)$$
5	1 2	pjclem1	$$⊢G{𝐶}_{\mathscr{H}}H\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$
6	1 2	cmcmi	$$⊢G{𝐶}_{\mathscr{H}}H\leftrightarrow H{𝐶}_{\mathscr{H}}G$$
7	2 1	pjclem1	$$⊢H{𝐶}_{\mathscr{H}}G\to {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap G\right)$$
8	6 7	sylbi	$$⊢G{𝐶}_{\mathscr{H}}H\to {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(H\cap G\right)$$
9	4 5 8	3eqtr4a	$$⊢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)$$