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 𝐺 ) = ( 𝐻 ∘ ◡ 𝐺 ) )