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 syl6bi φ A K B V C V F B = F C F A + ˙ B = F A + ˙ C