cocnv

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

		Ref	Expression
	Assertion	cocnv	$⊢ (Fun F \land Fun G) \to (F \circ G) \circ G^{-1} = {F ↾}_{ran G}$

Step	Hyp	Ref	Expression
1		coass	$⊢ (F \circ G) \circ G^{-1} = F \circ (G \circ G^{-1})$
2		funcocnv2	$⊢ Fun G \to G \circ G^{-1} = {I ↾}_{ran G}$
3	2	adantl	$⊢ (Fun F \land Fun G) \to G \circ G^{-1} = {I ↾}_{ran G}$
4	3	coeq2d	$⊢ (Fun F \land Fun G) \to F \circ (G \circ G^{-1}) = F \circ ({I ↾}_{ran G})$
5		resco	$⊢ {(F \circ I) ↾}_{ran G} = F \circ ({I ↾}_{ran G})$
6		funrel	$⊢ Fun F \to Rel F$
7		coi1	$⊢ Rel F \to F \circ I = F$
8	6 7	syl	$⊢ Fun F \to F \circ I = F$
9	8	reseq1d	$⊢ Fun F \to {(F \circ I) ↾}_{ran G} = {F ↾}_{ran G}$
10	9	adantr	$⊢ (Fun F \land Fun G) \to {(F \circ I) ↾}_{ran G} = {F ↾}_{ran G}$
11	5 10	eqtr3id	$⊢ (Fun F \land Fun G) \to F \circ ({I ↾}_{ran G}) = {F ↾}_{ran G}$
12	4 11	eqtrd	$⊢ (Fun F \land Fun G) \to F \circ (G \circ G^{-1}) = {F ↾}_{ran G}$
13	1 12	syl5eq	$⊢ (Fun F \land Fun G) \to (F \circ G) \circ G^{-1} = {F ↾}_{ran G}$

Metamath Proof Explorer