Metamath Proof Explorer


Theorem gsumfs2d

Description: Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses gsumfs2d.p 𝑥 𝜑
gsumfs2d.b 𝐵 = ( Base ‘ 𝑊 )
gsumfs2d.1 0 = ( 0g𝑊 )
gsumfs2d.r ( 𝜑 → Rel 𝐴 )
gsumfs2d.2 ( 𝜑𝐹 finSupp 0 )
gsumfs2d.w ( 𝜑𝑊 ∈ CMnd )
gsumfs2d.3 ( 𝜑𝐹 : 𝐴𝐵 )
gsumfs2d.a ( 𝜑𝐴𝑋 )
Assertion gsumfs2d ( 𝜑 → ( 𝑊 Σg 𝐹 ) = ( 𝑊 Σg ( 𝑥 ∈ dom 𝐴 ↦ ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumfs2d.p 𝑥 𝜑
2 gsumfs2d.b 𝐵 = ( Base ‘ 𝑊 )
3 gsumfs2d.1 0 = ( 0g𝑊 )
4 gsumfs2d.r ( 𝜑 → Rel 𝐴 )
5 gsumfs2d.2 ( 𝜑𝐹 finSupp 0 )
6 gsumfs2d.w ( 𝜑𝑊 ∈ CMnd )
7 gsumfs2d.3 ( 𝜑𝐹 : 𝐴𝐵 )
8 gsumfs2d.a ( 𝜑𝐴𝑋 )
9 6 adantr ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → 𝑊 ∈ CMnd )
10 8 adantr ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → 𝐴𝑋 )
11 10 imaexd ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → ( 𝐴 “ { 𝑥 } ) ∈ V )
12 7 ffnd ( 𝜑𝐹 Fn 𝐴 )
13 12 ad2antrr ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → 𝐹 Fn 𝐴 )
14 8 ad2antrr ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → 𝐴𝑋 )
15 3 fvexi 0 ∈ V
16 15 a1i ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → 0 ∈ V )
17 simpr ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) )
18 17 eldifad ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) )
19 vex 𝑥 ∈ V
20 vex 𝑦 ∈ V
21 19 20 elimasn ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
22 21 biimpi ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
23 18 22 syl ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
24 17 eldifbd ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) )
25 19 20 elimasn ( 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 supp 0 ) )
26 25 biimpri ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 supp 0 ) → 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) )
27 24 26 nsyl ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 supp 0 ) )
28 23 27 eldifd ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) )
29 13 14 16 28 fvdifsupp ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( ( 𝐴 “ { 𝑥 } ) ∖ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 0 )
30 5 fsuppimpd ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
31 30 adantr ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → ( 𝐹 supp 0 ) ∈ Fin )
32 imafi2 ( ( 𝐹 supp 0 ) ∈ Fin → ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ∈ Fin )
33 31 32 syl ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ∈ Fin )
34 7 ad2antrr ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → 𝐹 : 𝐴𝐵 )
35 22 adantl ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
36 34 35 ffvelcdmd ( ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐵 )
37 suppssdm ( 𝐹 supp 0 ) ⊆ dom 𝐹
38 37 7 fssdm ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
39 38 adantr ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
40 imass1 ( ( 𝐹 supp 0 ) ⊆ 𝐴 → ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ⊆ ( 𝐴 “ { 𝑥 } ) )
41 39 40 syl ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ⊆ ( 𝐴 “ { 𝑥 } ) )
42 2 3 9 11 29 33 36 41 gsummptres2 ( ( 𝜑𝑥 ∈ dom ( 𝐹 supp 0 ) ) → ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) = ( 𝑊 Σg ( 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
43 42 mpteq2dva ( 𝜑 → ( 𝑥 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) = ( 𝑥 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝑊 Σg ( 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) )
44 43 oveq2d ( 𝜑 → ( 𝑊 Σg ( 𝑥 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝑊 Σg ( 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )
45 8 dmexd ( 𝜑 → dom 𝐴 ∈ V )
46 12 ad2antrr ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → 𝐹 Fn 𝐴 )
47 8 ad2antrr ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → 𝐴𝑋 )
48 15 a1i ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → 0 ∈ V )
49 22 adantl ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
50 simplr ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → 𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) )
51 50 eldifbd ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ¬ 𝑥 ∈ dom ( 𝐹 supp 0 ) )
52 19 20 opeldm ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 supp 0 ) → 𝑥 ∈ dom ( 𝐹 supp 0 ) )
53 51 52 nsyl ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 supp 0 ) )
54 49 53 eldifd ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) )
55 46 47 48 54 fvdifsupp ( ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 0 )
56 55 mpteq2dva ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ 0 ) )
57 56 oveq2d ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) = ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ 0 ) ) )
58 6 cmnmndd ( 𝜑𝑊 ∈ Mnd )
59 8 adantr ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) → 𝐴𝑋 )
60 59 imaexd ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝐴 “ { 𝑥 } ) ∈ V )
61 3 gsumz ( ( 𝑊 ∈ Mnd ∧ ( 𝐴 “ { 𝑥 } ) ∈ V ) → ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ 0 ) ) = 0 )
62 58 60 61 syl2an2r ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ 0 ) ) = 0 )
63 57 62 eqtrd ( ( 𝜑𝑥 ∈ ( dom 𝐴 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) = 0 )
64 dmfi ( ( 𝐹 supp 0 ) ∈ Fin → dom ( 𝐹 supp 0 ) ∈ Fin )
65 30 64 syl ( 𝜑 → dom ( 𝐹 supp 0 ) ∈ Fin )
66 6 adantr ( ( 𝜑𝑥 ∈ dom 𝐴 ) → 𝑊 ∈ CMnd )
67 8 adantr ( ( 𝜑𝑥 ∈ dom 𝐴 ) → 𝐴𝑋 )
68 67 imaexd ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( 𝐴 “ { 𝑥 } ) ∈ V )
69 7 ad2antrr ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → 𝐹 : 𝐴𝐵 )
70 22 adantl ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
71 69 70 ffvelcdmd ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝐵 )
72 71 fmpttd ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) : ( 𝐴 “ { 𝑥 } ) ⟶ 𝐵 )
73 68 mptexd ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ∈ V )
74 72 ffnd ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) Fn ( 𝐴 “ { 𝑥 } ) )
75 15 a1i ( ( 𝜑𝑥 ∈ dom 𝐴 ) → 0 ∈ V )
76 30 adantr ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( 𝐹 supp 0 ) ∈ Fin )
77 76 32 syl ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ∈ Fin )
78 eqid ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
79 simp-4l ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → 𝜑 )
80 simp-4r ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → 𝑥 ∈ dom 𝐴 )
81 simpr ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → 𝑦 = 𝑡 )
82 simpllr ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) )
83 81 82 eqeltrd ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) )
84 simplr ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) )
85 81 84 eqneltrd ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) )
86 12 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → 𝐹 Fn 𝐴 )
87 8 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → 𝐴𝑋 )
88 15 a1i ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → 0 ∈ V )
89 70 adantr ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
90 26 con3i ( ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) → ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 supp 0 ) )
91 90 adantl ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 supp 0 ) )
92 89 91 eldifd ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) )
93 86 87 88 92 fvdifsupp ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 0 )
94 79 80 83 85 93 syl1111anc ( ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) ∧ 𝑦 = 𝑡 ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 0 )
95 simplr ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) )
96 15 a1i ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → 0 ∈ V )
97 78 94 95 96 fvmptd2 ( ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) ∧ ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ) → ( ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ‘ 𝑡 ) = 0 )
98 97 ex ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) → ( ¬ 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) → ( ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ‘ 𝑡 ) = 0 ) )
99 98 orrd ( ( ( 𝜑𝑥 ∈ dom 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 “ { 𝑥 } ) ) → ( 𝑡 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ∨ ( ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ‘ 𝑡 ) = 0 ) )
100 73 74 75 77 99 finnzfsuppd ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) finSupp 0 )
101 2 3 66 68 72 100 gsumcl ( ( 𝜑𝑥 ∈ dom 𝐴 ) → ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ∈ 𝐵 )
102 dmss ( ( 𝐹 supp 0 ) ⊆ 𝐴 → dom ( 𝐹 supp 0 ) ⊆ dom 𝐴 )
103 38 102 syl ( 𝜑 → dom ( 𝐹 supp 0 ) ⊆ dom 𝐴 )
104 2 3 6 45 63 65 101 103 gsummptres2 ( 𝜑 → ( 𝑊 Σg ( 𝑥 ∈ dom 𝐴 ↦ ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )
105 7 38 feqresmpt ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝑧 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹𝑧 ) ) )
106 105 oveq2d ( 𝜑 → ( 𝑊 Σg ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( 𝑊 Σg ( 𝑧 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹𝑧 ) ) ) )
107 ssidd ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
108 2 3 6 8 7 107 5 gsumres ( 𝜑 → ( 𝑊 Σg ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( 𝑊 Σg 𝐹 ) )
109 nfcv 𝑦 ( 𝐹𝑧 )
110 fveq2 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
111 relss ( ( 𝐹 supp 0 ) ⊆ 𝐴 → ( Rel 𝐴 → Rel ( 𝐹 supp 0 ) ) )
112 38 4 111 sylc ( 𝜑 → Rel ( 𝐹 supp 0 ) )
113 7 adantr ( ( 𝜑𝑧 ∈ ( 𝐹 supp 0 ) ) → 𝐹 : 𝐴𝐵 )
114 38 sselda ( ( 𝜑𝑧 ∈ ( 𝐹 supp 0 ) ) → 𝑧𝐴 )
115 113 114 ffvelcdmd ( ( 𝜑𝑧 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹𝑧 ) ∈ 𝐵 )
116 109 1 2 110 112 30 6 115 gsummpt2d ( 𝜑 → ( 𝑊 Σg ( 𝑧 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹𝑧 ) ) ) = ( 𝑊 Σg ( 𝑥 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝑊 Σg ( 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )
117 106 108 116 3eqtr3d ( 𝜑 → ( 𝑊 Σg 𝐹 ) = ( 𝑊 Σg ( 𝑥 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝑊 Σg ( 𝑦 ∈ ( ( 𝐹 supp 0 ) “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )
118 44 104 117 3eqtr4rd ( 𝜑 → ( 𝑊 Σg 𝐹 ) = ( 𝑊 Σg ( 𝑥 ∈ dom 𝐴 ↦ ( 𝑊 Σg ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )