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 𝐺 ∧ ( 𝐹 ∘ 𝐺 ) = 𝐻 ) → ( 𝐹 ↾ ran 𝐺 ) = ( 𝐻 ∘ ◡ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 funcocnv2 ⊢ ( Fun 𝐺 → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ ran 𝐺 ) )
2 1 coeq2d ⊢ ( Fun 𝐺 → ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) ) = ( 𝐹 ∘ ( I ↾ ran 𝐺 ) ) )
3 coass ⊢ ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) )
4 3 eqcomi ⊢ ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) ) = ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 )
5 coires1 ⊢ ( 𝐹 ∘ ( I ↾ ran 𝐺 ) ) = ( 𝐹 ↾ ran 𝐺 )
6 2 4 5 3eqtr3g ⊢ ( Fun 𝐺 → ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = ( 𝐹 ↾ ran 𝐺 ) )
7 coeq1 ⊢ ( ( 𝐹 ∘ 𝐺 ) = 𝐻 → ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = ( 𝐻 ∘ ◡ 𝐺 ) )
8 6 7 sylan9req ⊢ ( ( Fun 𝐺 ∧ ( 𝐹 ∘ 𝐺 ) = 𝐻 ) → ( 𝐹 ↾ ran 𝐺 ) = ( 𝐻 ∘ ◡ 𝐺 ) )