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 ‘ 𝐺 )
	eldprdi.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
	eldprdi.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	eldprdi.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	eldprdi.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
	dprdfinv.b	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	dprdfinv	⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝐹 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝑁 ∘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝐺 Σg 𝐹 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldprdi.0	⊢ 0 = ( 0g ‘ 𝐺 )
2		eldprdi.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
3		eldprdi.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
4		eldprdi.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
5		eldprdi.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
6		dprdfinv.b	⊢ 𝑁 = ( invg ‘ 𝐺 )
7		dprdgrp	⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
8	3 7	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
9		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10	9 6	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝑁 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
11	8 10	syl	⊢ ( 𝜑 → 𝑁 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
12	2 3 4 5 9	dprdff	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
13		fcompt	⊢ ( ( 𝑁 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) ∧ 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) ) → ( 𝑁 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
14	11 12 13	syl2anc	⊢ ( 𝜑 → ( 𝑁 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
15	3 4	dprdf2	⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
16	15	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
17	2 3 4 5	dprdfcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) )
18	6	subginvcl	⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝑆 ‘ 𝑥 ) )
19	16 17 18	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝑆 ‘ 𝑥 ) )
20	3 4	dprddomcld	⊢ ( 𝜑 → 𝐼 ∈ V )
21	20	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ V )
22		funmpt	⊢ Fun ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) )
23	22	a1i	⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
24	2 3 4 5	dprdffsupp	⊢ ( 𝜑 → 𝐹 finSupp 0 )
25		ssidd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
26	1	fvexi	⊢ 0 ∈ V
27	26	a1i	⊢ ( 𝜑 → 0 ∈ V )
28	12 25 20 27	suppssr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
29	28	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑁 ‘ 0 ) )
30	1 6	grpinvid	⊢ ( 𝐺 ∈ Grp → ( 𝑁 ‘ 0 ) = 0 )
31	8 30	syl	⊢ ( 𝜑 → ( 𝑁 ‘ 0 ) = 0 )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑁 ‘ 0 ) = 0 )
33	29 32	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 )
34	33 20	suppss2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
35		fsuppsssupp	⊢ ( ( ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∧ ( 𝐹 finSupp 0 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) finSupp 0 )
36	21 23 24 34 35	syl22anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) finSupp 0 )
37	2 3 4 19 36	dprdwd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝑊 )
38	14 37	eqeltrd	⊢ ( 𝜑 → ( 𝑁 ∘ 𝐹 ) ∈ 𝑊 )
39		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
40	2 3 4 5 39	dprdfcntz	⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
41	9 1 39 6 8 20 12 40 24	gsumzinv	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑁 ∘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝐺 Σg 𝐹 ) ) )
42	38 41	jca	⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝐹 ) ∈ 𝑊 ∧ ( 𝐺 Σg ( 𝑁 ∘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝐺 Σg 𝐹 ) ) ) )