This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 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 ↾ 𝐴 ) ) = 𝐹 )