Theorem cocnv

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

	Ref	Expression
Assertion	cocnv	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = ( 𝐹 ↾ ran 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		coass	⊢ ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) )
2		funcocnv2	⊢ ( Fun 𝐺 → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ ran 𝐺 ) )
3	2	adantl	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ ran 𝐺 ) )
4	3	coeq2d	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) ) = ( 𝐹 ∘ ( I ↾ ran 𝐺 ) ) )
5		resco	⊢ ( ( 𝐹 ∘ I ) ↾ ran 𝐺 ) = ( 𝐹 ∘ ( I ↾ ran 𝐺 ) )
6		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
7		coi1	⊢ ( Rel 𝐹 → ( 𝐹 ∘ I ) = 𝐹 )
8	6 7	syl	⊢ ( Fun 𝐹 → ( 𝐹 ∘ I ) = 𝐹 )
9	8	reseq1d	⊢ ( Fun 𝐹 → ( ( 𝐹 ∘ I ) ↾ ran 𝐺 ) = ( 𝐹 ↾ ran 𝐺 ) )
10	9	adantr	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ I ) ↾ ran 𝐺 ) = ( 𝐹 ↾ ran 𝐺 ) )
11	5 10	eqtr3id	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( 𝐹 ∘ ( I ↾ ran 𝐺 ) ) = ( 𝐹 ↾ ran 𝐺 ) )
12	4 11	eqtrd	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) ) = ( 𝐹 ↾ ran 𝐺 ) )
13	1 12	syl5eq	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = ( 𝐹 ↾ ran 𝐺 ) )