Theorem fcoi1

Description: Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	fcoi1	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2		df-fn	⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
3		eqimss	⊢ ( dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴 )
4		cnvi	⊢ ◡ I = I
5	4	reseq1i	⊢ ( ◡ I ↾ 𝐴 ) = ( I ↾ 𝐴 )
6	5	cnveqi	⊢ ◡ ( ◡ I ↾ 𝐴 ) = ◡ ( I ↾ 𝐴 )
7		cnvresid	⊢ ◡ ( I ↾ 𝐴 ) = ( I ↾ 𝐴 )
8	6 7	eqtr2i	⊢ ( I ↾ 𝐴 ) = ◡ ( ◡ I ↾ 𝐴 )
9	8	coeq2i	⊢ ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = ( 𝐹 ∘ ◡ ( ◡ I ↾ 𝐴 ) )
10		cores2	⊢ ( dom 𝐹 ⊆ 𝐴 → ( 𝐹 ∘ ◡ ( ◡ I ↾ 𝐴 ) ) = ( 𝐹 ∘ I ) )
11	9 10	syl5eq	⊢ ( dom 𝐹 ⊆ 𝐴 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = ( 𝐹 ∘ I ) )
12	3 11	syl	⊢ ( dom 𝐹 = 𝐴 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = ( 𝐹 ∘ I ) )
13		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
14		coi1	⊢ ( Rel 𝐹 → ( 𝐹 ∘ I ) = 𝐹 )
15	13 14	syl	⊢ ( Fun 𝐹 → ( 𝐹 ∘ I ) = 𝐹 )
16	12 15	sylan9eqr	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )
17	2 16	sylbi	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )
18	1 17	syl	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )