Metamath Proof Explorer

Theorem gsumsub

Description: The difference of two group sums. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumsub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumsub.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsumsub.m ⊢ − = ( -g ‘ 𝐺 )
gsumsub.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
gsumsub.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumsub.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumsub.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
gsumsub.fn ⊢ ( 𝜑 → 𝐹 finSupp 0 )
gsumsub.hn ⊢ ( 𝜑 → 𝐻 finSupp 0 )
Assertion gsumsub ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsumsub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumsub.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumsub.m ⊢ − = ( -g ‘ 𝐺 )
4 gsumsub.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
5 gsumsub.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 gsumsub.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 gsumsub.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
8 gsumsub.fn ⊢ ( 𝜑 → 𝐹 finSupp 0 )
9 gsumsub.hn ⊢ ( 𝜑 → 𝐻 finSupp 0 )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 ablcmn ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
12 4 11 syl ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
13 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
14 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
15 4 14 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
16 1 13 15 grpinvf1o ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 )
17 f1of ⊢ ( ( invg ‘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 → ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 )
18 16 17 syl ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 )
19 fco ⊢ ( ( ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ) → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) : 𝐴 ⟶ 𝐵 )
20 18 7 19 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) : 𝐴 ⟶ 𝐵 )
21 2 fvexi ⊢ 0 ∈ V
22 21 a1i ⊢ ( 𝜑 → 0 ∈ V )
23 1 fvexi ⊢ 𝐵 ∈ V
24 23 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
25 2 13 grpinvid ⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
26 15 25 syl ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 )
27 22 7 18 5 24 9 26 fsuppco2 ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) finSupp 0 )
28 1 2 10 12 5 6 20 8 27 gsumadd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) )
29 1 2 13 4 5 7 9 gsuminv ⊢ ( 𝜑 → ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) )
30 29 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
31 28 30 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
32 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
33 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝐵 )
34 1 10 13 3 grpsubval ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑘 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
35 32 33 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
36 35 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
37 6 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
38 7 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑘 ) ) )
39 5 32 33 37 38 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) ) )
40 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ∈ V )
41 18 feqmptd ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) )
42 fveq2 ⊢ ( 𝑥 = ( 𝐻 ‘ 𝑘 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) )
43 33 38 41 42 fmptco ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) = ( 𝑘 ∈ 𝐴 ↦ ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
44 5 32 40 37 43 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
45 36 39 44 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) = ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) )
46 45 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( 𝐺 Σg ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) )
47 1 2 12 5 6 8 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )
48 1 2 12 5 7 9 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg 𝐻 ) ∈ 𝐵 )
49 1 10 13 3 grpsubval ⊢ ( ( ( 𝐺 Σg 𝐹 ) ∈ 𝐵 ∧ ( 𝐺 Σg 𝐻 ) ∈ 𝐵 ) → ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
50 47 48 49 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐺 Σg 𝐻 ) ) ) )
51 31 46 50 3eqtr4d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f − 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )