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 
|- B = ( Base ` G )
gsumzadd.0 
|- .0. = ( 0g ` G )
gsumzadd.p 
|- .+ = ( +g ` G )
gsumzadd.z 
|- Z = ( Cntz ` G )
gsumzadd.g 
|- ( ph -> G e. Mnd )
gsumzadd.a 
|- ( ph -> A e. V )
gsumzadd.fn 
|- ( ph -> F finSupp .0. )
gsumzadd.hn 
|- ( ph -> H finSupp .0. )
gsumzadd.s 
|- ( ph -> S e. ( SubMnd ` G ) )
gsumzadd.c 
|- ( ph -> S C_ ( Z ` S ) )
gsumzadd.f 
|- ( ph -> F : A --> S )
gsumzadd.h 
|- ( ph -> H : A --> S )
Assertion gsumzadd 
|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )

Proof

Step Hyp Ref Expression
1 gsumzadd.b 
 |-  B = ( Base ` G )
2 gsumzadd.0 
 |-  .0. = ( 0g ` G )
3 gsumzadd.p 
 |-  .+ = ( +g ` G )
4 gsumzadd.z 
 |-  Z = ( Cntz ` G )
5 gsumzadd.g 
 |-  ( ph -> G e. Mnd )
6 gsumzadd.a 
 |-  ( ph -> A e. V )
7 gsumzadd.fn 
 |-  ( ph -> F finSupp .0. )
8 gsumzadd.hn 
 |-  ( ph -> H finSupp .0. )
9 gsumzadd.s 
 |-  ( ph -> S e. ( SubMnd ` G ) )
10 gsumzadd.c 
 |-  ( ph -> S C_ ( Z ` S ) )
11 gsumzadd.f 
 |-  ( ph -> F : A --> S )
12 gsumzadd.h 
 |-  ( ph -> H : A --> S )
13 eqid 
 |-  ( ( F u. H ) supp .0. ) = ( ( F u. H ) supp .0. )
14 1 submss 
 |-  ( S e. ( SubMnd ` G ) -> S C_ B )
15 9 14 syl 
 |-  ( ph -> S C_ B )
16 11 15 fssd 
 |-  ( ph -> F : A --> B )
17 12 15 fssd 
 |-  ( ph -> H : A --> B )
18 11 frnd 
 |-  ( ph -> ran F C_ S )
19 4 cntzidss 
 |-  ( ( S C_ ( Z ` S ) /\ ran F C_ S ) -> ran F C_ ( Z ` ran F ) )
20 10 18 19 syl2anc 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
21 12 frnd 
 |-  ( ph -> ran H C_ S )
22 4 cntzidss 
 |-  ( ( S C_ ( Z ` S ) /\ ran H C_ S ) -> ran H C_ ( Z ` ran H ) )
23 10 21 22 syl2anc 
 |-  ( ph -> ran H C_ ( Z ` ran H ) )
24 3 submcl 
 |-  ( ( S e. ( SubMnd ` G ) /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )
25 24 3expb 
 |-  ( ( S e. ( SubMnd ` G ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
26 9 25 sylan 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
27 inidm 
 |-  ( A i^i A ) = A
28 26 11 12 6 6 27 off 
 |-  ( ph -> ( F oF .+ H ) : A --> S )
29 28 frnd 
 |-  ( ph -> ran ( F oF .+ H ) C_ S )
30 4 cntzidss 
 |-  ( ( S C_ ( Z ` S ) /\ ran ( F oF .+ H ) C_ S ) -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
31 10 29 30 syl2anc 
 |-  ( ph -> ran ( F oF .+ H ) C_ ( Z ` ran ( F oF .+ H ) ) )
32 10 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> S C_ ( Z ` S ) )
33 15 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> S C_ B )
34 5 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> G e. Mnd )
35 vex 
 |-  x e. _V
36 35 a1i 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> x e. _V )
37 9 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> S e. ( SubMnd ` G ) )
38 simpl 
 |-  ( ( x C_ A /\ k e. ( A \ x ) ) -> x C_ A )
39 fssres 
 |-  ( ( H : A --> S /\ x C_ A ) -> ( H |` x ) : x --> S )
40 12 38 39 syl2an 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( H |` x ) : x --> S )
41 23 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ran H C_ ( Z ` ran H ) )
42 resss 
 |-  ( H |` x ) C_ H
43 42 rnssi 
 |-  ran ( H |` x ) C_ ran H
44 4 cntzidss 
 |-  ( ( ran H C_ ( Z ` ran H ) /\ ran ( H |` x ) C_ ran H ) -> ran ( H |` x ) C_ ( Z ` ran ( H |` x ) ) )
45 41 43 44 sylancl 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ran ( H |` x ) C_ ( Z ` ran ( H |` x ) ) )
46 12 ffund 
 |-  ( ph -> Fun H )
47 46 funresd 
 |-  ( ph -> Fun ( H |` x ) )
48 47 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> Fun ( H |` x ) )
49 8 fsuppimpd 
 |-  ( ph -> ( H supp .0. ) e. Fin )
50 49 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( H supp .0. ) e. Fin )
51 12 6 fexd 
 |-  ( ph -> H e. _V )
52 2 fvexi 
 |-  .0. e. _V
53 ressuppss 
 |-  ( ( H e. _V /\ .0. e. _V ) -> ( ( H |` x ) supp .0. ) C_ ( H supp .0. ) )
54 51 52 53 sylancl 
 |-  ( ph -> ( ( H |` x ) supp .0. ) C_ ( H supp .0. ) )
55 54 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( ( H |` x ) supp .0. ) C_ ( H supp .0. ) )
56 50 55 ssfid 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( ( H |` x ) supp .0. ) e. Fin )
57 resfunexg 
 |-  ( ( Fun H /\ x e. _V ) -> ( H |` x ) e. _V )
58 46 35 57 sylancl 
 |-  ( ph -> ( H |` x ) e. _V )
59 isfsupp 
 |-  ( ( ( H |` x ) e. _V /\ .0. e. _V ) -> ( ( H |` x ) finSupp .0. <-> ( Fun ( H |` x ) /\ ( ( H |` x ) supp .0. ) e. Fin ) ) )
60 58 52 59 sylancl 
 |-  ( ph -> ( ( H |` x ) finSupp .0. <-> ( Fun ( H |` x ) /\ ( ( H |` x ) supp .0. ) e. Fin ) ) )
61 60 adantr 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( ( H |` x ) finSupp .0. <-> ( Fun ( H |` x ) /\ ( ( H |` x ) supp .0. ) e. Fin ) ) )
62 48 56 61 mpbir2and 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( H |` x ) finSupp .0. )
63 2 4 34 36 37 40 45 62 gsumzsubmcl 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( G gsum ( H |` x ) ) e. S )
64 63 snssd 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> { ( G gsum ( H |` x ) ) } C_ S )
65 1 4 cntz2ss 
 |-  ( ( S C_ B /\ { ( G gsum ( H |` x ) ) } C_ S ) -> ( Z ` S ) C_ ( Z ` { ( G gsum ( H |` x ) ) } ) )
66 33 64 65 syl2anc 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( Z ` S ) C_ ( Z ` { ( G gsum ( H |` x ) ) } ) )
67 32 66 sstrd 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> S C_ ( Z ` { ( G gsum ( H |` x ) ) } ) )
68 eldifi 
 |-  ( k e. ( A \ x ) -> k e. A )
69 68 adantl 
 |-  ( ( x C_ A /\ k e. ( A \ x ) ) -> k e. A )
70 ffvelcdm 
 |-  ( ( F : A --> S /\ k e. A ) -> ( F ` k ) e. S )
71 11 69 70 syl2an 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. S )
72 67 71 sseldd 
 |-  ( ( ph /\ ( x C_ A /\ k e. ( A \ x ) ) ) -> ( F ` k ) e. ( Z ` { ( G gsum ( H |` x ) ) } ) )
73 1 2 3 4 5 6 7 8 13 16 17 20 23 31 72 gsumzaddlem 
 |-  ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )