Metamath Proof Explorer

Theorem f1ocan1fv

Description: Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 27-Dec-2014)

		Ref	Expression
	Assertion	f1ocan1fv	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to (F \circ G) (G^{-1} (X)) = F (X)$

Proof

Step	Hyp	Ref	Expression
1		f1of	$⊢ G : A \underset{1-1 onto}{⟶} B \to G : A ⟶ B$
2	1	3ad2ant2	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to G : A ⟶ B$
3		f1ocnv	$⊢ G : A \underset{1-1 onto}{⟶} B \to G^{-1} : B \underset{1-1 onto}{⟶} A$
4		f1of	$⊢ G^{-1} : B \underset{1-1 onto}{⟶} A \to G^{-1} : B ⟶ A$
5	3 4	syl	$⊢ G : A \underset{1-1 onto}{⟶} B \to G^{-1} : B ⟶ A$
6	5	3ad2ant2	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to G^{-1} : B ⟶ A$
7		simp3	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to X \in B$
8	6 7	ffvelcdmd	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to G^{-1} (X) \in A$
9		fvco3	$⊢ (G : A ⟶ B \land G^{-1} (X) \in A) \to (F \circ G) (G^{-1} (X)) = F (G (G^{-1} (X)))$
10	2 8 9	syl2anc	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to (F \circ G) (G^{-1} (X)) = F (G (G^{-1} (X)))$
11		f1ocnvfv2	$⊢ (G : A \underset{1-1 onto}{⟶} B \land X \in B) \to G (G^{-1} (X)) = X$
12	11	3adant1	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to G (G^{-1} (X)) = X$
13	12	fveq2d	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to F (G (G^{-1} (X))) = F (X)$
14	10 13	eqtrd	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in B) \to (F \circ G) (G^{-1} (X)) = F (X)$