This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) ) )