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 | |
|
eldprdi.w | |
||
eldprdi.1 | |
||
eldprdi.2 | |
||
eldprdi.3 | |
||
dprdfadd.4 | |
||
dprdfadd.b | |
||
Assertion | dprdfadd | |