Metamath Proof Explorer

Theorem gsum2d

Description: Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

Ref Expression
Hypotheses gsum2d.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsum2d.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsum2d.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsum2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsum2d.r ⊢ ( 𝜑 → Rel 𝐴 )
gsum2d.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
gsum2d.s ⊢ ( 𝜑 → dom 𝐴 ⊆ 𝐷 )
gsum2d.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsum2d.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsum2d ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsum2d.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsum2d.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsum2d.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsum2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 gsum2d.r ⊢ ( 𝜑 → Rel 𝐴 )
6 gsum2d.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
7 gsum2d.s ⊢ ( 𝜑 → dom 𝐴 ⊆ 𝐷 )
8 gsum2d.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9 gsum2d.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
10 1 2 3 4 5 6 7 8 9 gsum2dlem2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
11 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
12 11 8 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
13 relss ⊢ ( ( 𝐹 supp 0 ) ⊆ 𝐴 → ( Rel 𝐴 → Rel ( 𝐹 supp 0 ) ) )
14 12 5 13 sylc ⊢ ( 𝜑 → Rel ( 𝐹 supp 0 ) )
15 relssdmrn ⊢ ( Rel ( 𝐹 supp 0 ) → ( 𝐹 supp 0 ) ⊆ ( dom ( 𝐹 supp 0 ) × ran ( 𝐹 supp 0 ) ) )
16 ssv ⊢ ran ( 𝐹 supp 0 ) ⊆ V
17 xpss2 ⊢ ( ran ( 𝐹 supp 0 ) ⊆ V → ( dom ( 𝐹 supp 0 ) × ran ( 𝐹 supp 0 ) ) ⊆ ( dom ( 𝐹 supp 0 ) × V ) )
18 16 17 ax-mp ⊢ ( dom ( 𝐹 supp 0 ) × ran ( 𝐹 supp 0 ) ) ⊆ ( dom ( 𝐹 supp 0 ) × V )
19 15 18 sstrdi ⊢ ( Rel ( 𝐹 supp 0 ) → ( 𝐹 supp 0 ) ⊆ ( dom ( 𝐹 supp 0 ) × V ) )
20 14 19 syl ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( dom ( 𝐹 supp 0 ) × V ) )
21 12 20 ssind ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐴 ∩ ( dom ( 𝐹 supp 0 ) × V ) ) )
22 df-res ⊢ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) = ( 𝐴 ∩ ( dom ( 𝐹 supp 0 ) × V ) )
23 21 22 sseqtrrdi ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) )
24 1 2 3 4 8 23 9 gsumres ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg 𝐹 ) )
25 dmss ⊢ ( ( 𝐹 supp 0 ) ⊆ 𝐴 → dom ( 𝐹 supp 0 ) ⊆ dom 𝐴 )
26 12 25 syl ⊢ ( 𝜑 → dom ( 𝐹 supp 0 ) ⊆ dom 𝐴 )
27 26 7 sstrd ⊢ ( 𝜑 → dom ( 𝐹 supp 0 ) ⊆ 𝐷 )
28 27 resmptd ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ↾ dom ( 𝐹 supp 0 ) ) = ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) )
29 28 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ↾ dom ( 𝐹 supp 0 ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
30 1 2 3 4 5 6 7 8 9 gsum2dlem1 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )
32 31 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) : 𝐷 ⟶ 𝐵 )
33 vex ⊢ 𝑗 ∈ V
34 vex ⊢ 𝑘 ∈ V
35 33 34 elimasn ⊢ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
36 35 biimpi ⊢ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
37 36 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
38 eldifn ⊢ ( 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) → ¬ 𝑗 ∈ dom ( 𝐹 supp 0 ) )
39 38 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) ) → ¬ 𝑗 ∈ dom ( 𝐹 supp 0 ) )
40 33 34 opeldm ⊢ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) → 𝑗 ∈ dom ( 𝐹 supp 0 ) )
41 39 40 nsyl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) ) → ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) )
42 37 41 eldifd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) )
43 df-ov ⊢ ( 𝑗 𝐹 𝑘 ) = ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ )
44 ssidd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
45 2 fvexi ⊢ 0 ∈ V
46 45 a1i ⊢ ( 𝜑 → 0 ∈ V )
47 8 44 4 46 suppssr ⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 )
48 43 47 syl5eq ⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
49 42 48 syldan ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
50 49 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
51 50 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) = ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ 0 ) )
52 51 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ 0 ) ) )
53 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
54 3 53 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
55 imaexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 “ { 𝑗 } ) ∈ V )
56 4 55 syl ⊢ ( 𝜑 → ( 𝐴 “ { 𝑗 } ) ∈ V )
57 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐴 “ { 𝑗 } ) ∈ V ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ 0 ) ) = 0 )
58 54 56 57 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ 0 ) ) = 0 )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ 0 ) ) = 0 )
60 52 59 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐷 ∖ dom ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = 0 )
61 60 6 suppss2 ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) supp 0 ) ⊆ dom ( 𝐹 supp 0 ) )
62 funmpt ⊢ Fun ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
63 62 a1i ⊢ ( 𝜑 → Fun ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) )
64 9 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
65 dmfi ⊢ ( ( 𝐹 supp 0 ) ∈ Fin → dom ( 𝐹 supp 0 ) ∈ Fin )
66 64 65 syl ⊢ ( 𝜑 → dom ( 𝐹 supp 0 ) ∈ Fin )
67 66 61 ssfid ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) supp 0 ) ∈ Fin )
68 6 mptexd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ∈ V )
69 isfsupp ⊢ ( ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) finSupp 0 ↔ ( Fun ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ∧ ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) supp 0 ) ∈ Fin ) ) )
70 68 46 69 syl2anc ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) finSupp 0 ↔ ( Fun ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ∧ ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) supp 0 ) ∈ Fin ) ) )
71 63 67 70 mpbir2and ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) finSupp 0 )
72 1 2 3 6 32 61 71 gsumres ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ↾ dom ( 𝐹 supp 0 ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
73 29 72 eqtr3d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
74 10 24 73 3eqtr3d ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑗 ∈ 𝐷 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )