Theorem pjadjcoi

Description: Adjoint of composition of projections. Special case of Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 6-Oct-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjadjcoi	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	2	pjhcli	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
4	1	pjadji	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\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}}{\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)$$
5	3 4	sylan	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\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}}{\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)$$
6	1	pjhcli	$$⊢B\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\in \mathscr{H}$$
7	2	pjadji	$$⊢\left(A\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\right)$$
8	6 7	sylan2	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\right)$$
9	5 8	eqtrd	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\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({\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\right)$$
10	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)$$
11	10	oveq1d	$$⊢A\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}B={\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}B$$
12	11	adantr	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}B={\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}B$$
13	2 1	pjcoi	$$⊢B\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\right)$$
14	13	oveq2d	$$⊢B\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\right)$$
15	14	adantl	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(B\right)=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(B\right)\right)$$
16	9 12 15	3eqtr4d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(B\right)$$