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 \land F \circ G = H) \to {F ↾}_{ran G} = H \circ G^{-1}$

Step	Hyp	Ref	Expression
1		funcocnv2	$⊢ Fun G \to G \circ G^{-1} = {I ↾}_{ran G}$
2	1	coeq2d	$⊢ Fun G \to F \circ (G \circ G^{-1}) = F \circ ({I ↾}_{ran G})$
3		coass	$⊢ (F \circ G) \circ G^{-1} = F \circ (G \circ G^{-1})$
4	3	eqcomi	$⊢ F \circ (G \circ G^{-1}) = (F \circ G) \circ G^{-1}$
5		coires1	$⊢ F \circ ({I ↾}_{ran G}) = {F ↾}_{ran G}$
6	2 4 5	3eqtr3g	$⊢ Fun G \to (F \circ G) \circ G^{-1} = {F ↾}_{ran G}$
7		coeq1	$⊢ F \circ G = H \to (F \circ G) \circ G^{-1} = H \circ G^{-1}$
8	6 7	sylan9req	$⊢ (Fun G \land F \circ G = H) \to {F ↾}_{ran G} = H \circ G^{-1}$

Metamath Proof Explorer