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

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 ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↦ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )