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	ffvelcdmda	\|- ( ( 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 ) ) ) )

Metamath Proof Explorer

Theorem dprdfinv

Proof