f1ocan2fv

Description: Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Step	Hyp	Ref	Expression
1		f1orel	$⊢ G : A \underset{1-1 onto}{⟶} B \to Rel G$
2		dfrel2	$⊢ Rel G \leftrightarrow {G^{-1}}^{-1} = G$
3	1 2	sylib	$⊢ G : A \underset{1-1 onto}{⟶} B \to {G^{-1}}^{-1} = G$
4	3	3ad2ant2	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in A) \to {G^{-1}}^{-1} = G$
5	4	fveq1d	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in A) \to {G^{-1}}^{-1} (X) = G (X)$
6	5	fveq2d	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in A) \to (F \circ G^{-1}) ({G^{-1}}^{-1} (X)) = (F \circ G^{-1}) (G (X))$
7		f1ocnv	$⊢ G : A \underset{1-1 onto}{⟶} B \to G^{-1} : B \underset{1-1 onto}{⟶} A$
8		f1ocan1fv	$⊢ (Fun F \land G^{-1} : B \underset{1-1 onto}{⟶} A \land X \in A) \to (F \circ G^{-1}) ({G^{-1}}^{-1} (X)) = F (X)$
9	7 8	syl3an2	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in A) \to (F \circ G^{-1}) ({G^{-1}}^{-1} (X)) = F (X)$
10	6 9	eqtr3d	$⊢ (Fun F \land G : A \underset{1-1 onto}{⟶} B \land X \in A) \to (F \circ G^{-1}) (G (X)) = F (X)$

Metamath Proof Explorer