Metamath Proof Explorer

Theorem 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 ⊢ φ → F : V ⟶ 1-1 onto X
Assertion f1ovscpbl ⊢ φ ∧ A ∈ K ∧ B ∈ V ∧ C ∈ V → F ⁡ B = F ⁡ C → F ⁡ A + ˙ B = F ⁡ A + ˙ C

Proof

Step Hyp Ref Expression
1 f1ocpbl.f ⊢ φ → F : V ⟶ 1-1 onto X
2 f1of1 ⊢ F : V ⟶ 1-1 onto X → F : V ⟶ 1-1 X
3 1 2 syl ⊢ φ → F : V ⟶ 1-1 X
4 3 adantr ⊢ φ ∧ A ∈ K ∧ B ∈ V ∧ C ∈ V → F : V ⟶ 1-1 X
5 simpr2 ⊢ φ ∧ A ∈ K ∧ B ∈ V ∧ C ∈ V → B ∈ V
6 simpr3 ⊢ φ ∧ A ∈ K ∧ B ∈ V ∧ C ∈ V → C ∈ V
7 f1fveq ⊢ F : V ⟶ 1-1 X ∧ B ∈ V ∧ C ∈ V → F ⁡ B = F ⁡ C ↔ B = C
8 4 5 6 7 syl12anc ⊢ φ ∧ A ∈ K ∧ B ∈ V ∧ C ∈ V → F ⁡ B = F ⁡ C ↔ B = C
9 oveq2 ⊢ B = C → A + ˙ B = A + ˙ C
10 9 fveq2d ⊢ B = C → F ⁡ A + ˙ B = F ⁡ A + ˙ C
11 8 10 biimtrdi ⊢ φ ∧ A ∈ K ∧ B ∈ V ∧ C ∈ V → F ⁡ B = F ⁡ C → F ⁡ A + ˙ B = F ⁡ A + ˙ C