Metamath Proof Explorer


Theorem dprdfinv

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

Ref Expression
Hypotheses eldprdi.0 0 ˙ = 0 G
eldprdi.w W = h i I S i | finSupp 0 ˙ h
eldprdi.1 φ G dom DProd S
eldprdi.2 φ dom S = I
eldprdi.3 φ F W
dprdfinv.b N = inv g G
Assertion dprdfinv φ N F W G N F = N G F

Proof

Step Hyp Ref Expression
1 eldprdi.0 0 ˙ = 0 G
2 eldprdi.w W = h i I S i | finSupp 0 ˙ h
3 eldprdi.1 φ G dom DProd S
4 eldprdi.2 φ dom S = I
5 eldprdi.3 φ F W
6 dprdfinv.b N = inv g G
7 dprdgrp G dom DProd S G Grp
8 3 7 syl φ G Grp
9 eqid Base G = Base G
10 9 6 grpinvf G Grp N : Base G Base G
11 8 10 syl φ N : Base G Base G
12 2 3 4 5 9 dprdff φ F : I Base G
13 fcompt N : Base G Base G F : I Base G N F = x I N F x
14 11 12 13 syl2anc φ N F = x I N F x
15 3 4 dprdf2 φ S : I SubGrp G
16 15 ffvelrnda φ x I S x SubGrp G
17 2 3 4 5 dprdfcl φ x I F x S x
18 6 subginvcl S x SubGrp G F x S x N F x S x
19 16 17 18 syl2anc φ x I N F x S x
20 3 4 dprddomcld φ I V
21 20 mptexd φ x I N F x V
22 funmpt Fun x I N F x
23 22 a1i φ Fun x I N F x
24 2 3 4 5 dprdffsupp φ finSupp 0 ˙ F
25 ssidd φ F supp 0 ˙ F supp 0 ˙
26 1 fvexi 0 ˙ V
27 26 a1i φ 0 ˙ V
28 12 25 20 27 suppssr φ x I supp 0 ˙ F F x = 0 ˙
29 28 fveq2d φ x I supp 0 ˙ F N F x = N 0 ˙
30 1 6 grpinvid G Grp N 0 ˙ = 0 ˙
31 8 30 syl φ N 0 ˙ = 0 ˙
32 31 adantr φ x I supp 0 ˙ F N 0 ˙ = 0 ˙
33 29 32 eqtrd φ x I supp 0 ˙ F N F x = 0 ˙
34 33 20 suppss2 φ x I N F x supp 0 ˙ F supp 0 ˙
35 fsuppsssupp x I N F x V Fun x I N F x finSupp 0 ˙ F x I N F x supp 0 ˙ F supp 0 ˙ finSupp 0 ˙ x I N F x
36 21 23 24 34 35 syl22anc φ finSupp 0 ˙ x I N F x
37 2 3 4 19 36 dprdwd φ x I N F x W
38 14 37 eqeltrd φ N F W
39 eqid Cntz G = Cntz G
40 2 3 4 5 39 dprdfcntz φ ran F Cntz G ran F
41 9 1 39 6 8 20 12 40 24 gsumzinv φ G N F = N G F
42 38 41 jca φ N F W G N F = N G F