Metamath Proof Explorer


Theorem dprdfadd

Description: Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 0˙=0G
eldprdi.w W=hiISi|finSupp0˙h
eldprdi.1 φGdomDProdS
eldprdi.2 φdomS=I
eldprdi.3 φFW
dprdfadd.4 φHW
dprdfadd.b +˙=+G
Assertion dprdfadd φF+˙fHWGF+˙fH=GF+˙GH

Proof

Step Hyp Ref Expression
1 eldprdi.0 0˙=0G
2 eldprdi.w W=hiISi|finSupp0˙h
3 eldprdi.1 φGdomDProdS
4 eldprdi.2 φdomS=I
5 eldprdi.3 φFW
6 dprdfadd.4 φHW
7 dprdfadd.b +˙=+G
8 3 4 dprddomcld φIV
9 2 3 4 5 dprdfcl φxIFxSx
10 2 3 4 6 dprdfcl φxIHxSx
11 eqid BaseG=BaseG
12 2 3 4 5 11 dprdff φF:IBaseG
13 12 feqmptd φF=xIFx
14 2 3 4 6 11 dprdff φH:IBaseG
15 14 feqmptd φH=xIHx
16 8 9 10 13 15 offval2 φF+˙fH=xIFx+˙Hx
17 3 4 dprdf2 φS:ISubGrpG
18 17 ffvelrnda φxISxSubGrpG
19 7 subgcl SxSubGrpGFxSxHxSxFx+˙HxSx
20 18 9 10 19 syl3anc φxIFx+˙HxSx
21 2 3 4 5 dprdffsupp φfinSupp0˙F
22 2 3 4 6 dprdffsupp φfinSupp0˙H
23 21 22 fsuppunfi φsupp0˙Fsupp0˙HFin
24 ssun1 Fsupp0˙supp0˙Fsupp0˙H
25 24 a1i φFsupp0˙supp0˙Fsupp0˙H
26 1 fvexi 0˙V
27 26 a1i φ0˙V
28 12 25 8 27 suppssr φxIsupp0˙Fsupp0˙HFx=0˙
29 ssun2 Hsupp0˙supp0˙Fsupp0˙H
30 29 a1i φHsupp0˙supp0˙Fsupp0˙H
31 14 30 8 27 suppssr φxIsupp0˙Fsupp0˙HHx=0˙
32 28 31 oveq12d φxIsupp0˙Fsupp0˙HFx+˙Hx=0˙+˙0˙
33 dprdgrp GdomDProdSGGrp
34 3 33 syl φGGrp
35 11 1 grpidcl GGrp0˙BaseG
36 11 7 1 grplid GGrp0˙BaseG0˙+˙0˙=0˙
37 34 35 36 syl2anc2 φ0˙+˙0˙=0˙
38 37 adantr φxIsupp0˙Fsupp0˙H0˙+˙0˙=0˙
39 32 38 eqtrd φxIsupp0˙Fsupp0˙HFx+˙Hx=0˙
40 39 8 suppss2 φxIFx+˙Hxsupp0˙supp0˙Fsupp0˙H
41 23 40 ssfid φxIFx+˙Hxsupp0˙Fin
42 funmpt FunxIFx+˙Hx
43 42 a1i φFunxIFx+˙Hx
44 8 mptexd φxIFx+˙HxV
45 funisfsupp FunxIFx+˙HxxIFx+˙HxV0˙VfinSupp0˙xIFx+˙HxxIFx+˙Hxsupp0˙Fin
46 43 44 27 45 syl3anc φfinSupp0˙xIFx+˙HxxIFx+˙Hxsupp0˙Fin
47 41 46 mpbird φfinSupp0˙xIFx+˙Hx
48 2 3 4 20 47 dprdwd φxIFx+˙HxW
49 16 48 eqeltrd φF+˙fHW
50 eqid CntzG=CntzG
51 34 grpmndd φGMnd
52 eqid FHsupp0˙=FHsupp0˙
53 2 3 4 5 50 dprdfcntz φranFCntzGranF
54 2 3 4 6 50 dprdfcntz φranHCntzGranH
55 2 3 4 49 50 dprdfcntz φranF+˙fHCntzGranF+˙fH
56 51 adantr φxIkIxGMnd
57 vex xV
58 57 a1i φxIkIxxV
59 eldifi kIxkI
60 59 adantl xIkIxkI
61 ffvelrn F:IBaseGkIFkBaseG
62 12 60 61 syl2an φxIkIxFkBaseG
63 62 snssd φxIkIxFkBaseG
64 11 50 cntzsubm GMndFkBaseGCntzGFkSubMndG
65 56 63 64 syl2anc φxIkIxCntzGFkSubMndG
66 14 adantr φxIkIxH:IBaseG
67 66 ffnd φxIkIxHFnI
68 simprl φxIkIxxI
69 fnssres HFnIxIHxFnx
70 67 68 69 syl2anc φxIkIxHxFnx
71 fvres yxHxy=Hy
72 71 adantl φxIkIxyxHxy=Hy
73 3 ad2antrr φxIkIxyxGdomDProdS
74 4 ad2antrr φxIkIxyxdomS=I
75 73 74 dprdf2 φxIkIxyxS:ISubGrpG
76 60 ad2antlr φxIkIxyxkI
77 75 76 ffvelrnd φxIkIxyxSkSubGrpG
78 11 subgss SkSubGrpGSkBaseG
79 77 78 syl φxIkIxyxSkBaseG
80 5 ad2antrr φxIkIxyxFW
81 2 73 74 80 dprdfcl φxIkIxyxkIFkSk
82 76 81 mpdan φxIkIxyxFkSk
83 82 snssd φxIkIxyxFkSk
84 11 50 cntz2ss SkBaseGFkSkCntzGSkCntzGFk
85 79 83 84 syl2anc φxIkIxyxCntzGSkCntzGFk
86 68 sselda φxIkIxyxyI
87 simpr φxIkIxyxyx
88 simplrr φxIkIxyxkIx
89 88 eldifbd φxIkIxyx¬kx
90 nelne2 yx¬kxyk
91 87 89 90 syl2anc φxIkIxyxyk
92 73 74 86 76 91 50 dprdcntz φxIkIxyxSyCntzGSk
93 6 ad2antrr φxIkIxyxHW
94 2 73 74 93 dprdfcl φxIkIxyxyIHySy
95 86 94 mpdan φxIkIxyxHySy
96 92 95 sseldd φxIkIxyxHyCntzGSk
97 85 96 sseldd φxIkIxyxHyCntzGFk
98 72 97 eqeltrd φxIkIxyxHxyCntzGFk
99 98 ralrimiva φxIkIxyxHxyCntzGFk
100 ffnfv Hx:xCntzGFkHxFnxyxHxyCntzGFk
101 70 99 100 sylanbrc φxIkIxHx:xCntzGFk
102 resss HxH
103 102 rnssi ranHxranH
104 50 cntzidss ranHCntzGranHranHxranHranHxCntzGranHx
105 54 103 104 sylancl φranHxCntzGranHx
106 105 adantr φxIkIxranHxCntzGranHx
107 22 27 fsuppres φfinSupp0˙Hx
108 107 adantr φxIkIxfinSupp0˙Hx
109 1 50 56 58 65 101 106 108 gsumzsubmcl φxIkIxGHxCntzGFk
110 109 snssd φxIkIxGHxCntzGFk
111 66 68 fssresd φxIkIxHx:xBaseG
112 11 1 50 56 58 111 106 108 gsumzcl φxIkIxGHxBaseG
113 112 snssd φxIkIxGHxBaseG
114 11 50 cntzrec GHxBaseGFkBaseGGHxCntzGFkFkCntzGGHx
115 113 63 114 syl2anc φxIkIxGHxCntzGFkFkCntzGGHx
116 110 115 mpbid φxIkIxFkCntzGGHx
117 fvex FkV
118 117 snss FkCntzGGHxFkCntzGGHx
119 116 118 sylibr φxIkIxFkCntzGGHx
120 11 1 7 50 51 8 21 22 52 12 14 53 54 55 119 gsumzaddlem φGF+˙fH=GF+˙GH
121 49 120 jca φF+˙fHWGF+˙fH=GF+˙GH