Step |
Hyp |
Ref |
Expression |
1 |
|
gsumcllem.f |
|- ( ph -> F : A --> B ) |
2 |
|
gsumcllem.a |
|- ( ph -> A e. V ) |
3 |
|
gsumcllem.z |
|- ( ph -> Z e. U ) |
4 |
|
gsumcllem.s |
|- ( ph -> ( F supp Z ) C_ W ) |
5 |
1
|
feqmptd |
|- ( ph -> F = ( k e. A |-> ( F ` k ) ) ) |
6 |
5
|
adantr |
|- ( ( ph /\ W = (/) ) -> F = ( k e. A |-> ( F ` k ) ) ) |
7 |
|
difeq2 |
|- ( W = (/) -> ( A \ W ) = ( A \ (/) ) ) |
8 |
|
dif0 |
|- ( A \ (/) ) = A |
9 |
7 8
|
eqtrdi |
|- ( W = (/) -> ( A \ W ) = A ) |
10 |
9
|
eleq2d |
|- ( W = (/) -> ( k e. ( A \ W ) <-> k e. A ) ) |
11 |
10
|
biimpar |
|- ( ( W = (/) /\ k e. A ) -> k e. ( A \ W ) ) |
12 |
1 4 2 3
|
suppssr |
|- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z ) |
13 |
11 12
|
sylan2 |
|- ( ( ph /\ ( W = (/) /\ k e. A ) ) -> ( F ` k ) = Z ) |
14 |
13
|
anassrs |
|- ( ( ( ph /\ W = (/) ) /\ k e. A ) -> ( F ` k ) = Z ) |
15 |
14
|
mpteq2dva |
|- ( ( ph /\ W = (/) ) -> ( k e. A |-> ( F ` k ) ) = ( k e. A |-> Z ) ) |
16 |
6 15
|
eqtrd |
|- ( ( ph /\ W = (/) ) -> F = ( k e. A |-> Z ) ) |