Metamath Proof Explorer

Theorem cocnvf1o

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

Ref Expression
Hypotheses cocnvf1o.1 
|- ( ph -> F : A --> B )
cocnvf1o.2 
|- ( ph -> G : A --> B )
cocnvf1o.3 
|- ( ph -> H : A -1-1-onto-> A )
Assertion cocnvf1o 
|- ( ph -> ( F = ( G o. H ) <-> G = ( F o. `' H ) ) )

Proof

Step Hyp Ref Expression
1 cocnvf1o.1 
 |-  ( ph -> F : A --> B )
2 cocnvf1o.2 
 |-  ( ph -> G : A --> B )
3 cocnvf1o.3 
 |-  ( ph -> H : A -1-1-onto-> A )
4 simpr 
 |-  ( ( ph /\ F = ( G o. H ) ) -> F = ( G o. H ) )
5 4 coeq1d 
 |-  ( ( ph /\ F = ( G o. H ) ) -> ( F o. `' H ) = ( ( G o. H ) o. `' H ) )
6 coass 
 |-  ( ( G o. H ) o. `' H ) = ( G o. ( H o. `' H ) )
7 5 6 eqtrdi 
 |-  ( ( ph /\ F = ( G o. H ) ) -> ( F o. `' H ) = ( G o. ( H o. `' H ) ) )
8 f1ococnv2 
 |-  ( H : A -1-1-onto-> A -> ( H o. `' H ) = ( _I |` A ) )
9 3 8 syl 
 |-  ( ph -> ( H o. `' H ) = ( _I |` A ) )
10 9 coeq2d 
 |-  ( ph -> ( G o. ( H o. `' H ) ) = ( G o. ( _I |` A ) ) )
11 fcoi1 
 |-  ( G : A --> B -> ( G o. ( _I |` A ) ) = G )
12 2 11 syl 
 |-  ( ph -> ( G o. ( _I |` A ) ) = G )
13 10 12 eqtrd 
 |-  ( ph -> ( G o. ( H o. `' H ) ) = G )
14 13 adantr 
 |-  ( ( ph /\ F = ( G o. H ) ) -> ( G o. ( H o. `' H ) ) = G )
15 7 14 eqtr2d 
 |-  ( ( ph /\ F = ( G o. H ) ) -> G = ( F o. `' H ) )
16 simpr 
 |-  ( ( ph /\ G = ( F o. `' H ) ) -> G = ( F o. `' H ) )
17 16 coeq1d 
 |-  ( ( ph /\ G = ( F o. `' H ) ) -> ( G o. H ) = ( ( F o. `' H ) o. H ) )
18 coass 
 |-  ( ( F o. `' H ) o. H ) = ( F o. ( `' H o. H ) )
19 17 18 eqtrdi 
 |-  ( ( ph /\ G = ( F o. `' H ) ) -> ( G o. H ) = ( F o. ( `' H o. H ) ) )
20 f1ococnv1 
 |-  ( H : A -1-1-onto-> A -> ( `' H o. H ) = ( _I |` A ) )
21 3 20 syl 
 |-  ( ph -> ( `' H o. H ) = ( _I |` A ) )
22 21 coeq2d 
 |-  ( ph -> ( F o. ( `' H o. H ) ) = ( F o. ( _I |` A ) ) )
23 fcoi1 
 |-  ( F : A --> B -> ( F o. ( _I |` A ) ) = F )
24 1 23 syl 
 |-  ( ph -> ( F o. ( _I |` A ) ) = F )
25 22 24 eqtrd 
 |-  ( ph -> ( F o. ( `' H o. H ) ) = F )
26 25 adantr 
 |-  ( ( ph /\ G = ( F o. `' H ) ) -> ( F o. ( `' H o. H ) ) = F )
27 19 26 eqtr2d 
 |-  ( ( ph /\ G = ( F o. `' H ) ) -> F = ( G o. H ) )
28 15 27 impbida 
 |-  ( ph -> ( F = ( G o. H ) <-> G = ( F o. `' H ) ) )