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