Theorem pj3i

Description: 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	pj3i	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)$$

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(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
5		eqeq1	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)$$
6	4 5	mpbiri	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
7	6	rneqd	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\to \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)=\mathrm{ran}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)$$
8		rncoss	$$⊢\mathrm{ran}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\subseteq \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)$$
9	2	pjrni	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)=G$$
10	8 9	sseqtri	$$⊢\mathrm{ran}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\subseteq G$$
11	7 10	eqsstrdi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\to \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G$$
12	1 2 3	pj3si	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)$$
13	11 12	sylan2	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)$$