# 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 ${⊢}{\phi }\to {F}:{A}⟶{B}$
gsumcllem.a ${⊢}{\phi }\to {A}\in {V}$
gsumcllem.z ${⊢}{\phi }\to {Z}\in {U}$
gsumcllem.s ${⊢}{\phi }\to {F}\mathrm{supp}{Z}\subseteq {W}$
Assertion gsumcllem ${⊢}\left({\phi }\wedge {W}=\varnothing \right)\to {F}=\left({k}\in {A}⟼{Z}\right)$

### Proof

Step Hyp Ref Expression
1 gsumcllem.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
2 gsumcllem.a ${⊢}{\phi }\to {A}\in {V}$
3 gsumcllem.z ${⊢}{\phi }\to {Z}\in {U}$
4 gsumcllem.s ${⊢}{\phi }\to {F}\mathrm{supp}{Z}\subseteq {W}$
5 1 feqmptd ${⊢}{\phi }\to {F}=\left({k}\in {A}⟼{F}\left({k}\right)\right)$
6 5 adantr ${⊢}\left({\phi }\wedge {W}=\varnothing \right)\to {F}=\left({k}\in {A}⟼{F}\left({k}\right)\right)$
7 difeq2 ${⊢}{W}=\varnothing \to {A}\setminus {W}={A}\setminus \varnothing$
8 dif0 ${⊢}{A}\setminus \varnothing ={A}$
9 7 8 syl6eq ${⊢}{W}=\varnothing \to {A}\setminus {W}={A}$
10 9 eleq2d ${⊢}{W}=\varnothing \to \left({k}\in \left({A}\setminus {W}\right)↔{k}\in {A}\right)$
11 10 biimpar ${⊢}\left({W}=\varnothing \wedge {k}\in {A}\right)\to {k}\in \left({A}\setminus {W}\right)$
12 1 4 2 3 suppssr ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {F}\left({k}\right)={Z}$
13 11 12 sylan2 ${⊢}\left({\phi }\wedge \left({W}=\varnothing \wedge {k}\in {A}\right)\right)\to {F}\left({k}\right)={Z}$
14 13 anassrs ${⊢}\left(\left({\phi }\wedge {W}=\varnothing \right)\wedge {k}\in {A}\right)\to {F}\left({k}\right)={Z}$
15 14 mpteq2dva ${⊢}\left({\phi }\wedge {W}=\varnothing \right)\to \left({k}\in {A}⟼{F}\left({k}\right)\right)=\left({k}\in {A}⟼{Z}\right)$
16 6 15 eqtrd ${⊢}\left({\phi }\wedge {W}=\varnothing \right)\to {F}=\left({k}\in {A}⟼{Z}\right)$