Theorem pjadj2coi

Description: Adjoint of double composition of projections. Generalization of special case of Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 1-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	pjadj2coi	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{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){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\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	3	pjhcli	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
5	1 2	pjadjcoi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}B={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)$$
6	4 5	sylan	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}B={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)$$
7	2 1	pjcohcli	$$⊢B\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\in \mathscr{H}$$
8	3	pjadji	$$⊢\left(A\in \mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\right)$$
9	7 8	sylan2	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\right)$$
10	6 9	eqtrd	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\right)$$
11	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right):\mathscr{H}⟶\mathscr{H}$$
12	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
13	11 12	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right):\mathscr{H}⟶\mathscr{H}$$
14	3	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
15	13 14	hocoi	$$⊢A\in \mathscr{H}\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)=\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
16	15	oveq1d	$$⊢A\in \mathscr{H}\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){\cdot }_{\mathrm{ih}}B=\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}B$$
17	16	adantr	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{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){\cdot }_{\mathrm{ih}}B=\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}B$$
18		coass	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)$$
19	18	fveq1i	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\right)\left(B\right)$$
20	12 11	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right):\mathscr{H}⟶\mathscr{H}$$
21	14 20	hocoi	$$⊢B\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\right)$$
22	19 21	syl5eq	$$⊢B\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\right)$$
23	22	oveq2d	$$⊢B\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\right)$$
24	23	adantl	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)\right)$$
25	10 17 24	3eqtr4d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{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){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(B\right)$$