Step |
Hyp |
Ref |
Expression |
1 |
|
f1ocpbl.f |
|- ( ph -> F : V -1-1-onto-> X ) |
2 |
1
|
f1ocpbllem |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) <-> ( A = C /\ B = D ) ) ) |
3 |
|
oveq12 |
|- ( ( A = C /\ B = D ) -> ( A .+ B ) = ( C .+ D ) ) |
4 |
3
|
fveq2d |
|- ( ( A = C /\ B = D ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) |
5 |
2 4
|
syl6bi |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) ) |