Theorem funcoeqres

Description: Express a constraint on a composition as a constraint on the composand. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	funcoeqres	$$⊢\left(\mathrm{Fun}G\wedge F\circ G=H\right)\to {F\upharpoonright }_{\mathrm{ran}G}=H\circ G^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		funcocnv2	$$⊢\mathrm{Fun}G\to G\circ G^{-1}={\mathrm{I}\upharpoonright }_{\mathrm{ran}G}$$
2	1	coeq2d	$$⊢\mathrm{Fun}G\to F\circ \left(G\circ G^{-1}\right)=F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}G}\right)$$
3		coass	$$⊢\left(F\circ G\right)\circ G^{-1}=F\circ \left(G\circ G^{-1}\right)$$
4	3	eqcomi	$$⊢F\circ \left(G\circ G^{-1}\right)=\left(F\circ G\right)\circ G^{-1}$$
5		coires1	$$⊢F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}G}\right)={F\upharpoonright }_{\mathrm{ran}G}$$
6	2 4 5	3eqtr3g	$$⊢\mathrm{Fun}G\to \left(F\circ G\right)\circ G^{-1}={F\upharpoonright }_{\mathrm{ran}G}$$
7		coeq1	$$⊢F\circ G=H\to \left(F\circ G\right)\circ G^{-1}=H\circ G^{-1}$$
8	6 7	sylan9req	$$⊢\left(\mathrm{Fun}G\wedge F\circ G=H\right)\to {F\upharpoonright }_{\mathrm{ran}G}=H\circ G^{-1}$$