Metamath Proof Explorer


Theorem gsumzadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumzadd.b 𝐵 = ( Base ‘ 𝐺 )
gsumzadd.0 0 = ( 0g𝐺 )
gsumzadd.p + = ( +g𝐺 )
gsumzadd.z 𝑍 = ( Cntz ‘ 𝐺 )
gsumzadd.g ( 𝜑𝐺 ∈ Mnd )
gsumzadd.a ( 𝜑𝐴𝑉 )
gsumzadd.fn ( 𝜑𝐹 finSupp 0 )
gsumzadd.hn ( 𝜑𝐻 finSupp 0 )
gsumzadd.s ( 𝜑𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
gsumzadd.c ( 𝜑𝑆 ⊆ ( 𝑍𝑆 ) )
gsumzadd.f ( 𝜑𝐹 : 𝐴𝑆 )
gsumzadd.h ( 𝜑𝐻 : 𝐴𝑆 )
Assertion gsumzadd ( 𝜑 → ( 𝐺 Σg ( 𝐹f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsumzadd.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumzadd.0 0 = ( 0g𝐺 )
3 gsumzadd.p + = ( +g𝐺 )
4 gsumzadd.z 𝑍 = ( Cntz ‘ 𝐺 )
5 gsumzadd.g ( 𝜑𝐺 ∈ Mnd )
6 gsumzadd.a ( 𝜑𝐴𝑉 )
7 gsumzadd.fn ( 𝜑𝐹 finSupp 0 )
8 gsumzadd.hn ( 𝜑𝐻 finSupp 0 )
9 gsumzadd.s ( 𝜑𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
10 gsumzadd.c ( 𝜑𝑆 ⊆ ( 𝑍𝑆 ) )
11 gsumzadd.f ( 𝜑𝐹 : 𝐴𝑆 )
12 gsumzadd.h ( 𝜑𝐻 : 𝐴𝑆 )
13 eqid ( ( 𝐹𝐻 ) supp 0 ) = ( ( 𝐹𝐻 ) supp 0 )
14 1 submss ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆𝐵 )
15 9 14 syl ( 𝜑𝑆𝐵 )
16 11 15 fssd ( 𝜑𝐹 : 𝐴𝐵 )
17 12 15 fssd ( 𝜑𝐻 : 𝐴𝐵 )
18 11 frnd ( 𝜑 → ran 𝐹𝑆 )
19 4 cntzidss ( ( 𝑆 ⊆ ( 𝑍𝑆 ) ∧ ran 𝐹𝑆 ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
20 10 18 19 syl2anc ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
21 12 frnd ( 𝜑 → ran 𝐻𝑆 )
22 4 cntzidss ( ( 𝑆 ⊆ ( 𝑍𝑆 ) ∧ ran 𝐻𝑆 ) → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) )
23 10 21 22 syl2anc ( 𝜑 → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) )
24 3 submcl ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑥𝑆𝑦𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
25 24 3expb ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
26 9 25 sylan ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
27 inidm ( 𝐴𝐴 ) = 𝐴
28 26 11 12 6 6 27 off ( 𝜑 → ( 𝐹f + 𝐻 ) : 𝐴𝑆 )
29 28 frnd ( 𝜑 → ran ( 𝐹f + 𝐻 ) ⊆ 𝑆 )
30 4 cntzidss ( ( 𝑆 ⊆ ( 𝑍𝑆 ) ∧ ran ( 𝐹f + 𝐻 ) ⊆ 𝑆 ) → ran ( 𝐹f + 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹f + 𝐻 ) ) )
31 10 29 30 syl2anc ( 𝜑 → ran ( 𝐹f + 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹f + 𝐻 ) ) )
32 10 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → 𝑆 ⊆ ( 𝑍𝑆 ) )
33 15 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → 𝑆𝐵 )
34 5 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → 𝐺 ∈ Mnd )
35 vex 𝑥 ∈ V
36 35 a1i ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → 𝑥 ∈ V )
37 9 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
38 simpl ( ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) → 𝑥𝐴 )
39 fssres ( ( 𝐻 : 𝐴𝑆𝑥𝐴 ) → ( 𝐻𝑥 ) : 𝑥𝑆 )
40 12 38 39 syl2an ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( 𝐻𝑥 ) : 𝑥𝑆 )
41 23 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) )
42 resss ( 𝐻𝑥 ) ⊆ 𝐻
43 42 rnssi ran ( 𝐻𝑥 ) ⊆ ran 𝐻
44 4 cntzidss ( ( ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) ∧ ran ( 𝐻𝑥 ) ⊆ ran 𝐻 ) → ran ( 𝐻𝑥 ) ⊆ ( 𝑍 ‘ ran ( 𝐻𝑥 ) ) )
45 41 43 44 sylancl ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ran ( 𝐻𝑥 ) ⊆ ( 𝑍 ‘ ran ( 𝐻𝑥 ) ) )
46 12 ffund ( 𝜑 → Fun 𝐻 )
47 46 funresd ( 𝜑 → Fun ( 𝐻𝑥 ) )
48 47 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → Fun ( 𝐻𝑥 ) )
49 8 fsuppimpd ( 𝜑 → ( 𝐻 supp 0 ) ∈ Fin )
50 49 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( 𝐻 supp 0 ) ∈ Fin )
51 12 6 fexd ( 𝜑𝐻 ∈ V )
52 2 fvexi 0 ∈ V
53 ressuppss ( ( 𝐻 ∈ V ∧ 0 ∈ V ) → ( ( 𝐻𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) )
54 51 52 53 sylancl ( 𝜑 → ( ( 𝐻𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) )
55 54 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( ( 𝐻𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) )
56 50 55 ssfid ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( ( 𝐻𝑥 ) supp 0 ) ∈ Fin )
57 resfunexg ( ( Fun 𝐻𝑥 ∈ V ) → ( 𝐻𝑥 ) ∈ V )
58 46 35 57 sylancl ( 𝜑 → ( 𝐻𝑥 ) ∈ V )
59 isfsupp ( ( ( 𝐻𝑥 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐻𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻𝑥 ) ∧ ( ( 𝐻𝑥 ) supp 0 ) ∈ Fin ) ) )
60 58 52 59 sylancl ( 𝜑 → ( ( 𝐻𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻𝑥 ) ∧ ( ( 𝐻𝑥 ) supp 0 ) ∈ Fin ) ) )
61 60 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( ( 𝐻𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻𝑥 ) ∧ ( ( 𝐻𝑥 ) supp 0 ) ∈ Fin ) ) )
62 48 56 61 mpbir2and ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( 𝐻𝑥 ) finSupp 0 )
63 2 4 34 36 37 40 45 62 gsumzsubmcl ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( 𝐺 Σg ( 𝐻𝑥 ) ) ∈ 𝑆 )
64 63 snssd ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → { ( 𝐺 Σg ( 𝐻𝑥 ) ) } ⊆ 𝑆 )
65 1 4 cntz2ss ( ( 𝑆𝐵 ∧ { ( 𝐺 Σg ( 𝐻𝑥 ) ) } ⊆ 𝑆 ) → ( 𝑍𝑆 ) ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻𝑥 ) ) } ) )
66 33 64 65 syl2anc ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( 𝑍𝑆 ) ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻𝑥 ) ) } ) )
67 32 66 sstrd ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → 𝑆 ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻𝑥 ) ) } ) )
68 eldifi ( 𝑘 ∈ ( 𝐴𝑥 ) → 𝑘𝐴 )
69 68 adantl ( ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) → 𝑘𝐴 )
70 ffvelrn ( ( 𝐹 : 𝐴𝑆𝑘𝐴 ) → ( 𝐹𝑘 ) ∈ 𝑆 )
71 11 69 70 syl2an ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( 𝐹𝑘 ) ∈ 𝑆 )
72 67 71 sseldd ( ( 𝜑 ∧ ( 𝑥𝐴𝑘 ∈ ( 𝐴𝑥 ) ) ) → ( 𝐹𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻𝑥 ) ) } ) )
73 1 2 3 4 5 6 7 8 13 16 17 20 23 31 72 gsumzaddlem ( 𝜑 → ( 𝐺 Σg ( 𝐹f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )