This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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