This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 
|- ( ( Fun G /\ ( F o. G ) = H ) -> ( F |` ran G ) = ( H o. `' G ) )

Proof

Step Hyp Ref Expression
1 funcocnv2 
 |-  ( Fun G -> ( G o. `' G ) = ( _I |` ran G ) )
2 1 coeq2d 
 |-  ( Fun G -> ( F o. ( G o. `' G ) ) = ( F o. ( _I |` ran G ) ) )
3 coass 
 |-  ( ( F o. G ) o. `' G ) = ( F o. ( G o. `' G ) )
4 3 eqcomi 
 |-  ( F o. ( G o. `' G ) ) = ( ( F o. G ) o. `' G )
5 coires1 
 |-  ( F o. ( _I |` ran G ) ) = ( F |` ran G )
6 2 4 5 3eqtr3g 
 |-  ( Fun G -> ( ( F o. G ) o. `' G ) = ( F |` ran G ) )
7 coeq1 
 |-  ( ( F o. G ) = H -> ( ( F o. G ) o. `' G ) = ( H o. `' G ) )
8 6 7 sylan9req 
 |-  ( ( Fun G /\ ( F o. G ) = H ) -> ( F |` ran G ) = ( H o. `' G ) )