Theorem gsumzinv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsumzinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumzinv.0	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumzinv.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	gsumzinv.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
	gsumzinv.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	gsumzinv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumzinv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsumzinv.c	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
	gsumzinv.n	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	gsumzinv	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumzinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumzinv.0	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumzinv.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4		gsumzinv.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
5		gsumzinv.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6		gsumzinv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7		gsumzinv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8		gsumzinv.c	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
9		gsumzinv.n	⊢ ( 𝜑 → 𝐹 finSupp 0 )
10		eqid	⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 )
11	5	grpmndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
12	1 4	grpinvf	⊢ ( 𝐺 ∈ Grp → 𝐼 : 𝐵 ⟶ 𝐵 )
13	5 12	syl	⊢ ( 𝜑 → 𝐼 : 𝐵 ⟶ 𝐵 )
14		fco	⊢ ( ( 𝐼 : 𝐵 ⟶ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐼 ∘ 𝐹 ) : 𝐴 ⟶ 𝐵 )
15	13 7 14	syl2anc	⊢ ( 𝜑 → ( 𝐼 ∘ 𝐹 ) : 𝐴 ⟶ 𝐵 )
16	10 4	invoppggim	⊢ ( 𝐺 ∈ Grp → 𝐼 ∈ ( 𝐺 GrpIso ( oppg ‘ 𝐺 ) ) )
17		gimghm	⊢ ( 𝐼 ∈ ( 𝐺 GrpIso ( oppg ‘ 𝐺 ) ) → 𝐼 ∈ ( 𝐺 GrpHom ( oppg ‘ 𝐺 ) ) )
18		ghmmhm	⊢ ( 𝐼 ∈ ( 𝐺 GrpHom ( oppg ‘ 𝐺 ) ) → 𝐼 ∈ ( 𝐺 MndHom ( oppg ‘ 𝐺 ) ) )
19	5 16 17 18	4syl	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 MndHom ( oppg ‘ 𝐺 ) ) )
20		eqid	⊢ ( Cntz ‘ ( oppg ‘ 𝐺 ) ) = ( Cntz ‘ ( oppg ‘ 𝐺 ) )
21	3 20	cntzmhm2	⊢ ( ( 𝐼 ∈ ( 𝐺 MndHom ( oppg ‘ 𝐺 ) ) ∧ ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) ) → ( 𝐼 “ ran 𝐹 ) ⊆ ( ( Cntz ‘ ( oppg ‘ 𝐺 ) ) ‘ ( 𝐼 “ ran 𝐹 ) ) )
22	19 8 21	syl2anc	⊢ ( 𝜑 → ( 𝐼 “ ran 𝐹 ) ⊆ ( ( Cntz ‘ ( oppg ‘ 𝐺 ) ) ‘ ( 𝐼 “ ran 𝐹 ) ) )
23		rnco2	⊢ ran ( 𝐼 ∘ 𝐹 ) = ( 𝐼 “ ran 𝐹 )
24	23	fveq2i	⊢ ( 𝑍 ‘ ran ( 𝐼 ∘ 𝐹 ) ) = ( 𝑍 ‘ ( 𝐼 “ ran 𝐹 ) )
25	10 3	oppgcntz	⊢ ( 𝑍 ‘ ( 𝐼 “ ran 𝐹 ) ) = ( ( Cntz ‘ ( oppg ‘ 𝐺 ) ) ‘ ( 𝐼 “ ran 𝐹 ) )
26	24 25	eqtri	⊢ ( 𝑍 ‘ ran ( 𝐼 ∘ 𝐹 ) ) = ( ( Cntz ‘ ( oppg ‘ 𝐺 ) ) ‘ ( 𝐼 “ ran 𝐹 ) )
27	22 23 26	3sstr4g	⊢ ( 𝜑 → ran ( 𝐼 ∘ 𝐹 ) ⊆ ( 𝑍 ‘ ran ( 𝐼 ∘ 𝐹 ) ) )
28	2	fvexi	⊢ 0 ∈ V
29	28	a1i	⊢ ( 𝜑 → 0 ∈ V )
30	1	fvexi	⊢ 𝐵 ∈ V
31	30	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
32	2 4	grpinvid	⊢ ( 𝐺 ∈ Grp → ( 𝐼 ‘ 0 ) = 0 )
33	5 32	syl	⊢ ( 𝜑 → ( 𝐼 ‘ 0 ) = 0 )
34	29 7 13 6 31 9 33	fsuppco2	⊢ ( 𝜑 → ( 𝐼 ∘ 𝐹 ) finSupp 0 )
35	1 2 3 10 11 6 15 27 34	gsumzoppg	⊢ ( 𝜑 → ( ( oppg ‘ 𝐺 ) Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) )
36	10	oppgmnd	⊢ ( 𝐺 ∈ Mnd → ( oppg ‘ 𝐺 ) ∈ Mnd )
37	11 36	syl	⊢ ( 𝜑 → ( oppg ‘ 𝐺 ) ∈ Mnd )
38	1 3 11 37 6 19 7 8 2 9	gsumzmhm	⊢ ( 𝜑 → ( ( oppg ‘ 𝐺 ) Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )
39	35 38	eqtr3d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )