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. = ( 0g ` G )
eldprdi.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
eldprdi.1 
|- ( ph -> G dom DProd S )
eldprdi.2 
|- ( ph -> dom S = I )
eldprdi.3 
|- ( ph -> F e. W )
dprdfinv.b 
|- N = ( invg ` G )
Assertion dprdfinv 
|- ( ph -> ( ( N o. F ) e. W /\ ( G gsum ( N o. F ) ) = ( N ` ( G gsum F ) ) ) )

Proof

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