Step |
Hyp |
Ref |
Expression |
1 |
|
f1ocpbl.f |
|- ( ph -> F : V -1-1-onto-> X ) |
2 |
|
f1of1 |
|- ( F : V -1-1-onto-> X -> F : V -1-1-> X ) |
3 |
1 2
|
syl |
|- ( ph -> F : V -1-1-> X ) |
4 |
3
|
adantr |
|- ( ( ph /\ ( A e. K /\ B e. V /\ C e. V ) ) -> F : V -1-1-> X ) |
5 |
|
simpr2 |
|- ( ( ph /\ ( A e. K /\ B e. V /\ C e. V ) ) -> B e. V ) |
6 |
|
simpr3 |
|- ( ( ph /\ ( A e. K /\ B e. V /\ C e. V ) ) -> C e. V ) |
7 |
|
f1fveq |
|- ( ( F : V -1-1-> X /\ ( B e. V /\ C e. V ) ) -> ( ( F ` B ) = ( F ` C ) <-> B = C ) ) |
8 |
4 5 6 7
|
syl12anc |
|- ( ( ph /\ ( A e. K /\ B e. V /\ C e. 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 |
|- ( ( ph /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( F ` B ) = ( F ` C ) -> ( F ` ( A .+ B ) ) = ( F ` ( A .+ C ) ) ) ) |