f1ovscpbl

Description: An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015)

		Ref	Expression
	Hypothesis	f1ocpbl.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} X$
	Assertion	f1ovscpbl	$⊢ (φ \land (A \in K \land B \in V \land C \in V)) \to (F (B) = F (C) \to F (A \underset{˙}{+} B) = F (A \underset{˙}{+} C))$

Step	Hyp	Ref	Expression
1		f1ocpbl.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} X$
2		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} X \to F : V \underset{1-1}{⟶} X$
3	1 2	syl	$⊢ φ \to F : V \underset{1-1}{⟶} X$
4	3	adantr	$⊢ (φ \land (A \in K \land B \in V \land C \in V)) \to F : V \underset{1-1}{⟶} X$
5		simpr2	$⊢ (φ \land (A \in K \land B \in V \land C \in V)) \to B \in V$
6		simpr3	$⊢ (φ \land (A \in K \land B \in V \land C \in V)) \to C \in V$
7		f1fveq	$⊢ (F : V \underset{1-1}{⟶} X \land (B \in V \land C \in V)) \to (F (B) = F (C) \leftrightarrow B = C)$
8	4 5 6 7	syl12anc	$⊢ (φ \land (A \in K \land B \in V \land C \in V)) \to (F (B) = F (C) \leftrightarrow B = C)$
9		oveq2	$⊢ B = C \to A \underset{˙}{+} B = A \underset{˙}{+} C$
10	9	fveq2d	$⊢ B = C \to F (A \underset{˙}{+} B) = F (A \underset{˙}{+} C)$
11	8 10	biimtrdi	$⊢ (φ \land (A \in K \land B \in V \land C \in V)) \to (F (B) = F (C) \to F (A \underset{˙}{+} B) = F (A \underset{˙}{+} C))$

Metamath Proof Explorer