Theorem cocnvf1o

Description: Composing with the inverse of a bijection. (Contributed by Thierry Arnoux, 15-Jan-2026)

	Ref	Expression
Hypotheses	cocnvf1o.1	$$⊢\phi \to F:A⟶B$$
	cocnvf1o.2	$$⊢\phi \to G:A⟶B$$
	cocnvf1o.3	$$⊢\phi \to H:A\underset{1-1\; onto}{⟶}A$$
Assertion	cocnvf1o	$$⊢\phi \to \left(F=G\circ H\leftrightarrow G=F\circ H^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cocnvf1o.1	$$⊢\phi \to F:A⟶B$$
2		cocnvf1o.2	$$⊢\phi \to G:A⟶B$$
3		cocnvf1o.3	$$⊢\phi \to H:A\underset{1-1\; onto}{⟶}A$$
4		simpr	$$⊢\left(\phi \wedge F=G\circ H\right)\to F=G\circ H$$
5	4	coeq1d	$$⊢\left(\phi \wedge F=G\circ H\right)\to F\circ H^{-1}=\left(G\circ H\right)\circ H^{-1}$$
6		coass	$$⊢\left(G\circ H\right)\circ H^{-1}=G\circ \left(H\circ H^{-1}\right)$$
7	5 6	eqtrdi	$$⊢\left(\phi \wedge F=G\circ H\right)\to F\circ H^{-1}=G\circ \left(H\circ H^{-1}\right)$$
8		f1ococnv2	$$⊢H:A\underset{1-1\; onto}{⟶}A\to H\circ H^{-1}={\mathrm{I}\upharpoonright }_A$$
9	3 8	syl	$$⊢\phi \to H\circ H^{-1}={\mathrm{I}\upharpoonright }_A$$
10	9	coeq2d	$$⊢\phi \to G\circ \left(H\circ H^{-1}\right)=G\circ \left({\mathrm{I}\upharpoonright }_A\right)$$
11		fcoi1	$$⊢G:A⟶B\to G\circ \left({\mathrm{I}\upharpoonright }_A\right)=G$$
12	2 11	syl	$$⊢\phi \to G\circ \left({\mathrm{I}\upharpoonright }_A\right)=G$$
13	10 12	eqtrd	$$⊢\phi \to G\circ \left(H\circ H^{-1}\right)=G$$
14	13	adantr	$$⊢\left(\phi \wedge F=G\circ H\right)\to G\circ \left(H\circ H^{-1}\right)=G$$
15	7 14	eqtr2d	$$⊢\left(\phi \wedge F=G\circ H\right)\to G=F\circ H^{-1}$$
16		simpr	$$⊢\left(\phi \wedge G=F\circ H^{-1}\right)\to G=F\circ H^{-1}$$
17	16	coeq1d	$$⊢\left(\phi \wedge G=F\circ H^{-1}\right)\to G\circ H=\left(F\circ H^{-1}\right)\circ H$$
18		coass	$$⊢\left(F\circ H^{-1}\right)\circ H=F\circ \left(H^{-1}\circ H\right)$$
19	17 18	eqtrdi	$$⊢\left(\phi \wedge G=F\circ H^{-1}\right)\to G\circ H=F\circ \left(H^{-1}\circ H\right)$$
20		f1ococnv1	$$⊢H:A\underset{1-1\; onto}{⟶}A\to H^{-1}\circ H={\mathrm{I}\upharpoonright }_A$$
21	3 20	syl	$$⊢\phi \to H^{-1}\circ H={\mathrm{I}\upharpoonright }_A$$
22	21	coeq2d	$$⊢\phi \to F\circ \left(H^{-1}\circ H\right)=F\circ \left({\mathrm{I}\upharpoonright }_A\right)$$
23		fcoi1	$$⊢F:A⟶B\to F\circ \left({\mathrm{I}\upharpoonright }_A\right)=F$$
24	1 23	syl	$$⊢\phi \to F\circ \left({\mathrm{I}\upharpoonright }_A\right)=F$$
25	22 24	eqtrd	$$⊢\phi \to F\circ \left(H^{-1}\circ H\right)=F$$
26	25	adantr	$$⊢\left(\phi \wedge G=F\circ H^{-1}\right)\to F\circ \left(H^{-1}\circ H\right)=F$$
27	19 26	eqtr2d	$$⊢\left(\phi \wedge G=F\circ H^{-1}\right)\to F=G\circ H$$
28	15 27	impbida	$$⊢\phi \to \left(F=G\circ H\leftrightarrow G=F\circ H^{-1}\right)$$