Theorem pjclem4a

Description: Lemma for projection commutation theorem. (Contributed by NM, 2-Dec-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	pjclem4a	$$⊢A\in \left(G\cap H\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		elin	$$⊢A\in \left(G\cap H\right)\leftrightarrow \left(A\in G\wedge A\in H\right)$$
4	2	cheli	$$⊢A\in H\to A\in \mathscr{H}$$
5	4	adantl	$$⊢\left(A\in G\wedge A\in H\right)\to A\in \mathscr{H}$$
6	1 2	pjcoi	$$⊢A\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
7	5 6	syl	$$⊢\left(A\in G\wedge A\in H\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
8		pjid	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in H\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A$$
9	2 8	mpan	$$⊢A\in H\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A$$
10		eleq1	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in G\leftrightarrow A\in G\right)$$
11		pjid	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
12	1 11	mpan	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in G\to {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
13	10 12	syl6bir	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\to \left(A\in G\to {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
14		eqeq2	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=A\right)$$
15	13 14	sylibd	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=A\to \left(A\in G\to {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=A\right)$$
16	9 15	syl	$$⊢A\in H\to \left(A\in G\to {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=A\right)$$
17	16	impcom	$$⊢\left(A\in G\wedge A\in H\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=A$$
18	7 17	eqtrd	$$⊢\left(A\in G\wedge A\in H\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A$$
19	3 18	sylbi	$$⊢A\in \left(G\cap H\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A$$