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 funres ⊢ ( Fun 𝐻 → Fun ( 𝐻 ↾ 𝑥 ) )
48 46 47 syl ⊢ ( 𝜑 → Fun ( 𝐻 ↾ 𝑥 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → Fun ( 𝐻 ↾ 𝑥 ) )
50 8 fsuppimpd ⊢ ( 𝜑 → ( 𝐻 supp 0 ) ∈ Fin )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐻 supp 0 ) ∈ Fin )
52 fex ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝑆 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 ∈ V )
53 12 6 52 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ V )
54 2 fvexi ⊢ 0 ∈ V
55 ressuppss ⊢ ( ( 𝐻 ∈ V ∧ 0 ∈ V ) → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) )
56 53 54 55 sylancl ⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ⊆ ( 𝐻 supp 0 ) )
58 51 57 ssfid ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin )
59 resfunexg ⊢ ( ( Fun 𝐻 ∧ 𝑥 ∈ V ) → ( 𝐻 ↾ 𝑥 ) ∈ V )
60 46 35 59 sylancl ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑥 ) ∈ V )
61 isfsupp ⊢ ( ( ( 𝐻 ↾ 𝑥 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐻 ↾ 𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻 ↾ 𝑥 ) ∧ ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin ) ) )
62 60 54 61 sylancl ⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻 ↾ 𝑥 ) ∧ ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( ( 𝐻 ↾ 𝑥 ) finSupp 0 ↔ ( Fun ( 𝐻 ↾ 𝑥 ) ∧ ( ( 𝐻 ↾ 𝑥 ) supp 0 ) ∈ Fin ) ) )
64 49 58 63 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐻 ↾ 𝑥 ) finSupp 0 )
65 2 4 34 36 37 40 45 64 gsumzsubmcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) ∈ 𝑆 )
66 65 snssd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ 𝑆 )
67 1 4 cntz2ss ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ⊆ 𝑆 ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
68 33 66 67 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝑍 ‘ 𝑆 ) ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
69 32 68 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → 𝑆 ⊆ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
70 eldifi ⊢ ( 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) → 𝑘 ∈ 𝐴 )
71 70 adantl ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) → 𝑘 ∈ 𝐴 )
72 ffvelrn ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑆 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
73 11 71 72 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
74 69 73 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
75 1 2 3 4 5 6 7 8 13 16 17 20 23 31 74 gsumzaddlem ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )