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

Metamath Proof Explorer

Theorem 2fvcoidd

Description: Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019)

Ref Expression
Hypotheses 2fvcoidd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2fvcoidd.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
2fvcoidd.i ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ( 𝐺 ‘ ( 𝐹 ‘ 𝑎 ) ) = 𝑎 )
Assertion 2fvcoidd ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 2fvcoidd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 2fvcoidd.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
3 2fvcoidd.i ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ( 𝐺 ‘ ( 𝐹 ‘ 𝑎 ) ) = 𝑎 )
4 fcompt ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
5 2 1 4 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
6 2fveq3 ⊢ ( 𝑎 = 𝑥 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑎 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
7 id ⊢ ( 𝑎 = 𝑥 → 𝑎 = 𝑥 )
8 6 7 eqeq12d ⊢ ( 𝑎 = 𝑥 → ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑎 ) ) = 𝑎 ↔ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) )
9 8 rspccv ⊢ ( ∀ 𝑎 ∈ 𝐴 ( 𝐺 ‘ ( 𝐹 ‘ 𝑎 ) ) = 𝑎 → ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) )
10 3 9 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 ) )
11 10 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝑥 )
12 11 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) )
13 mptresid ⊢ ( I ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑥 )
14 12 13 eqtr4di ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( I ↾ 𝐴 ) )
15 5 14 eqtrd ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )