Theorem pj3lem1

Description: Lemma for projection triplet theorem. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjadj2co.1	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
	pjadj2co.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjadj2co.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pj3lem1	$$⊢A\in \left(\left(F\cap G\right)\cap H\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		pjadj2co.1	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjadj2co.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjadj2co.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
4		coass	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
5	4	fveq1i	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\left(A\right)$$
6		elin	$$⊢A\in \left(F\cap \left(G\cap H\right)\right)\leftrightarrow \left(A\in F\wedge A\in \left(G\cap H\right)\right)$$
7	1	cheli	$$⊢A\in F\to A\in \mathscr{H}$$
8	7	adantr	$$⊢\left(A\in F\wedge A\in \left(G\cap H\right)\right)\to A\in \mathscr{H}$$
9	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right):\mathscr{H}⟶\mathscr{H}$$
10	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
11	3	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
12	10 11	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
13	9 12	hocoi	$$⊢A\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)$$
14	8 13	syl	$$⊢\left(A\in F\wedge A\in \left(G\cap H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)$$
15	2 3	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$$
16		eleq1	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\in F\leftrightarrow A\in F\right)$$
17		pjid	$$⊢\left(F\in {\mathbf{C}}_{\mathscr{H}}\wedge \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\in F\right)\to {\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)$$
18	1 17	mpan	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\in F\to {\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)$$
19	16 18	syl6bir	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A\to \left(A\in F\to {\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)$$
20		eqeq2	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=A\right)$$
21	19 20	sylibd	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A\to \left(A\in F\to {\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=A\right)$$
22	15 21	syl	$$⊢A\in \left(G\cap H\right)\to \left(A\in F\to {\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=A\right)$$
23	22	impcom	$$⊢\left(A\in F\wedge A\in \left(G\cap H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(F\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)\right)=A$$
24	14 23	eqtrd	$$⊢\left(A\in F\wedge A\in \left(G\cap H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\left(A\right)=A$$
25	6 24	sylbi	$$⊢A\in \left(F\cap \left(G\cap H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\left(A\right)=A$$
26		inass	$$⊢\left(F\cap G\right)\cap H=F\cap \left(G\cap H\right)$$
27	25 26	eleq2s	$$⊢A\in \left(\left(F\cap G\right)\cap H\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\left(A\right)=A$$
28	5 27	syl5eq	$$⊢A\in \left(\left(F\cap G\right)\cap H\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right)=A$$