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 φ F : A B
gsumcllem.a φ A V
gsumcllem.z φ Z U
gsumcllem.s φ F supp Z W
Assertion gsumcllem φ W = F = k A Z

Proof

Step Hyp Ref Expression
1 gsumcllem.f φ F : A B
2 gsumcllem.a φ A V
3 gsumcllem.z φ Z U
4 gsumcllem.s φ F supp Z W
5 1 feqmptd φ F = k A F k
6 5 adantr φ W = F = k 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 A W k A
11 10 biimpar W = k A k A W
12 1 4 2 3 suppssr φ k A W F k = Z
13 11 12 sylan2 φ W = k A F k = Z
14 13 anassrs φ W = k A F k = Z
15 14 mpteq2dva φ W = k A F k = k A Z
16 6 15 eqtrd φ W = F = k A Z