Metamath Proof Explorer

Theorem cocnv

Description: Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion cocnv 
|- ( ( Fun F /\ Fun G ) -> ( ( F o. G ) o. `' G ) = ( F |` ran G ) )

Proof

Step Hyp Ref Expression
1 coass 
 |-  ( ( F o. G ) o. `' G ) = ( F o. ( G o. `' G ) )
2 funcocnv2 
 |-  ( Fun G -> ( G o. `' G ) = ( _I |` ran G ) )
3 2 adantl 
 |-  ( ( Fun F /\ Fun G ) -> ( G o. `' G ) = ( _I |` ran G ) )
4 3 coeq2d 
 |-  ( ( Fun F /\ Fun G ) -> ( F o. ( G o. `' G ) ) = ( F o. ( _I |` ran G ) ) )
5 resco 
 |-  ( ( F o. _I ) |` ran G ) = ( F o. ( _I |` ran G ) )
6 funrel 
 |-  ( Fun F -> Rel F )
7 coi1 
 |-  ( Rel F -> ( F o. _I ) = F )
8 6 7 syl 
 |-  ( Fun F -> ( F o. _I ) = F )
9 8 reseq1d 
 |-  ( Fun F -> ( ( F o. _I ) |` ran G ) = ( F |` ran G ) )
10 9 adantr 
 |-  ( ( Fun F /\ Fun G ) -> ( ( F o. _I ) |` ran G ) = ( F |` ran G ) )
11 5 10 eqtr3id 
 |-  ( ( Fun F /\ Fun G ) -> ( F o. ( _I |` ran G ) ) = ( F |` ran G ) )
12 4 11 eqtrd 
 |-  ( ( Fun F /\ Fun G ) -> ( F o. ( G o. `' G ) ) = ( F |` ran G ) )
13 1 12 eqtrid 
 |-  ( ( Fun F /\ Fun G ) -> ( ( F o. G ) o. `' G ) = ( F |` ran G ) )