Metamath Proof Explorer


Theorem gsumcllem

Description: Lemma for gsumcl and related theorems. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-2019)

Ref Expression
Hypotheses gsumcllem.f
|- ( ph -> F : A --> B )
gsumcllem.a
|- ( ph -> A e. V )
gsumcllem.z
|- ( ph -> Z e. U )
gsumcllem.s
|- ( ph -> ( F supp Z ) C_ W )
Assertion gsumcllem
|- ( ( ph /\ W = (/) ) -> F = ( k e. A |-> Z ) )

Proof

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 ) )