Metamath Proof Explorer

Theorem dprdfadd

Description: Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 
|- .0. = ( 0g ` G )
eldprdi.w 
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
eldprdi.1 
|- ( ph -> G dom DProd S )
eldprdi.2 
|- ( ph -> dom S = I )
eldprdi.3 
|- ( ph -> F e. W )
dprdfadd.4 
|- ( ph -> H e. W )
dprdfadd.b 
|- .+ = ( +g ` G )
Assertion dprdfadd 
|- ( ph -> ( ( F oF .+ H ) e. W /\ ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 
 |-  .0. = ( 0g ` G )
2 eldprdi.w 
 |-  W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3 eldprdi.1 
 |-  ( ph -> G dom DProd S )
4 eldprdi.2 
 |-  ( ph -> dom S = I )
5 eldprdi.3 
 |-  ( ph -> F e. W )
6 dprdfadd.4 
 |-  ( ph -> H e. W )
7 dprdfadd.b 
 |-  .+ = ( +g ` G )
8 3 4 dprddomcld 
 |-  ( ph -> I e. _V )
9 2 3 4 5 dprdfcl 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. ( S ` x ) )
10 2 3 4 6 dprdfcl 
 |-  ( ( ph /\ x e. I ) -> ( H ` x ) e. ( S ` x ) )
11 eqid 
 |-  ( Base ` G ) = ( Base ` G )
12 2 3 4 5 11 dprdff 
 |-  ( ph -> F : I --> ( Base ` G ) )
13 12 feqmptd 
 |-  ( ph -> F = ( x e. I |-> ( F ` x ) ) )
14 2 3 4 6 11 dprdff 
 |-  ( ph -> H : I --> ( Base ` G ) )
15 14 feqmptd 
 |-  ( ph -> H = ( x e. I |-> ( H ` x ) ) )
16 8 9 10 13 15 offval2 
 |-  ( ph -> ( F oF .+ H ) = ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) )
17 3 4 dprdf2 
 |-  ( ph -> S : I --> ( SubGrp ` G ) )
18 17 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) )
19 7 subgcl 
 |-  ( ( ( S ` x ) e. ( SubGrp ` G ) /\ ( F ` x ) e. ( S ` x ) /\ ( H ` x ) e. ( S ` x ) ) -> ( ( F ` x ) .+ ( H ` x ) ) e. ( S ` x ) )
20 18 9 10 19 syl3anc 
 |-  ( ( ph /\ x e. I ) -> ( ( F ` x ) .+ ( H ` x ) ) e. ( S ` x ) )
21 2 3 4 5 dprdffsupp 
 |-  ( ph -> F finSupp .0. )
22 2 3 4 6 dprdffsupp 
 |-  ( ph -> H finSupp .0. )
23 21 22 fsuppunfi 
 |-  ( ph -> ( ( F supp .0. ) u. ( H supp .0. ) ) e. Fin )
24 ssun1 
 |-  ( F supp .0. ) C_ ( ( F supp .0. ) u. ( H supp .0. ) )
25 24 a1i 
 |-  ( ph -> ( F supp .0. ) C_ ( ( F supp .0. ) u. ( H supp .0. ) ) )
26 1 fvexi 
 |-  .0. e. _V
27 26 a1i 
 |-  ( ph -> .0. e. _V )
28 12 25 8 27 suppssr 
 |-  ( ( ph /\ x e. ( I \ ( ( F supp .0. ) u. ( H supp .0. ) ) ) ) -> ( F ` x ) = .0. )
29 ssun2 
 |-  ( H supp .0. ) C_ ( ( F supp .0. ) u. ( H supp .0. ) )
30 29 a1i 
 |-  ( ph -> ( H supp .0. ) C_ ( ( F supp .0. ) u. ( H supp .0. ) ) )
31 14 30 8 27 suppssr 
 |-  ( ( ph /\ x e. ( I \ ( ( F supp .0. ) u. ( H supp .0. ) ) ) ) -> ( H ` x ) = .0. )
32 28 31 oveq12d 
 |-  ( ( ph /\ x e. ( I \ ( ( F supp .0. ) u. ( H supp .0. ) ) ) ) -> ( ( F ` x ) .+ ( H ` x ) ) = ( .0. .+ .0. ) )
33 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
34 3 33 syl 
 |-  ( ph -> G e. Grp )
35 11 1 grpidcl 
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
36 11 7 1 grplid 
 |-  ( ( G e. Grp /\ .0. e. ( Base ` G ) ) -> ( .0. .+ .0. ) = .0. )
37 34 35 36 syl2anc2 
 |-  ( ph -> ( .0. .+ .0. ) = .0. )
38 37 adantr 
 |-  ( ( ph /\ x e. ( I \ ( ( F supp .0. ) u. ( H supp .0. ) ) ) ) -> ( .0. .+ .0. ) = .0. )
39 32 38 eqtrd 
 |-  ( ( ph /\ x e. ( I \ ( ( F supp .0. ) u. ( H supp .0. ) ) ) ) -> ( ( F ` x ) .+ ( H ` x ) ) = .0. )
40 39 8 suppss2 
 |-  ( ph -> ( ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) supp .0. ) C_ ( ( F supp .0. ) u. ( H supp .0. ) ) )
41 23 40 ssfid 
 |-  ( ph -> ( ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) supp .0. ) e. Fin )
42 funmpt 
 |-  Fun ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) )
43 42 a1i 
 |-  ( ph -> Fun ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) )
44 8 mptexd 
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) e. _V )
45 funisfsupp 
 |-  ( ( Fun ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) /\ ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) e. _V /\ .0. e. _V ) -> ( ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) finSupp .0. <-> ( ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) supp .0. ) e. Fin ) )
46 43 44 27 45 syl3anc 
 |-  ( ph -> ( ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) finSupp .0. <-> ( ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) supp .0. ) e. Fin ) )
47 41 46 mpbird 
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) finSupp .0. )
48 2 3 4 20 47 dprdwd 
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) .+ ( H ` x ) ) ) e. W )
49 16 48 eqeltrd 
 |-  ( ph -> ( F oF .+ H ) e. W )
50 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
51 34 grpmndd 
 |-  ( ph -> G e. Mnd )
52 eqid 
 |-  ( ( F u. H ) supp .0. ) = ( ( F u. H ) supp .0. )
53 2 3 4 5 50 dprdfcntz 
 |-  ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
54 2 3 4 6 50 dprdfcntz 
 |-  ( ph -> ran H C_ ( ( Cntz ` G ) ` ran H ) )
55 2 3 4 49 50 dprdfcntz 
 |-  ( ph -> ran ( F oF .+ H ) C_ ( ( Cntz ` G ) ` ran ( F oF .+ H ) ) )
56 51 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> G e. Mnd )
57 vex 
 |-  x e. _V
58 57 a1i 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> x e. _V )
59 eldifi 
 |-  ( k e. ( I \ x ) -> k e. I )
60 59 adantl 
 |-  ( ( x C_ I /\ k e. ( I \ x ) ) -> k e. I )
61 ffvelrn 
 |-  ( ( F : I --> ( Base ` G ) /\ k e. I ) -> ( F ` k ) e. ( Base ` G ) )
62 12 60 61 syl2an 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( F ` k ) e. ( Base ` G ) )
63 62 snssd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( F ` k ) } C_ ( Base ` G ) )
64 11 50 cntzsubm 
 |-  ( ( G e. Mnd /\ { ( F ` k ) } C_ ( Base ` G ) ) -> ( ( Cntz ` G ) ` { ( F ` k ) } ) e. ( SubMnd ` G ) )
65 56 63 64 syl2anc 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( ( Cntz ` G ) ` { ( F ` k ) } ) e. ( SubMnd ` G ) )
66 14 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> H : I --> ( Base ` G ) )
67 66 ffnd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> H Fn I )
68 simprl 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> x C_ I )
69 fnssres 
 |-  ( ( H Fn I /\ x C_ I ) -> ( H |` x ) Fn x )
70 67 68 69 syl2anc 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) Fn x )
71 fvres 
 |-  ( y e. x -> ( ( H |` x ) ` y ) = ( H ` y ) )
72 71 adantl 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( ( H |` x ) ` y ) = ( H ` y ) )
73 3 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> G dom DProd S )
74 4 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> dom S = I )
75 73 74 dprdf2 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> S : I --> ( SubGrp ` G ) )
76 60 ad2antlr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> k e. I )
77 75 76 ffvelrnd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( S ` k ) e. ( SubGrp ` G ) )
78 11 subgss 
 |-  ( ( S ` k ) e. ( SubGrp ` G ) -> ( S ` k ) C_ ( Base ` G ) )
79 77 78 syl 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( S ` k ) C_ ( Base ` G ) )
80 5 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> F e. W )
81 2 73 74 80 dprdfcl 
 |-  ( ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) /\ k e. I ) -> ( F ` k ) e. ( S ` k ) )
82 76 81 mpdan 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( F ` k ) e. ( S ` k ) )
83 82 snssd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> { ( F ` k ) } C_ ( S ` k ) )
84 11 50 cntz2ss 
 |-  ( ( ( S ` k ) C_ ( Base ` G ) /\ { ( F ` k ) } C_ ( S ` k ) ) -> ( ( Cntz ` G ) ` ( S ` k ) ) C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) )
85 79 83 84 syl2anc 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( ( Cntz ` G ) ` ( S ` k ) ) C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) )
86 68 sselda 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> y e. I )
87 simpr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> y e. x )
88 simplrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> k e. ( I \ x ) )
89 88 eldifbd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> -. k e. x )
90 nelne2 
 |-  ( ( y e. x /\ -. k e. x ) -> y =/= k )
91 87 89 90 syl2anc 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> y =/= k )
92 73 74 86 76 91 50 dprdcntz 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( S ` y ) C_ ( ( Cntz ` G ) ` ( S ` k ) ) )
93 6 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> H e. W )
94 2 73 74 93 dprdfcl 
 |-  ( ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) /\ y e. I ) -> ( H ` y ) e. ( S ` y ) )
95 86 94 mpdan 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( H ` y ) e. ( S ` y ) )
96 92 95 sseldd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( H ` y ) e. ( ( Cntz ` G ) ` ( S ` k ) ) )
97 85 96 sseldd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( H ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
98 72 97 eqeltrd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( ( H |` x ) ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
99 98 ralrimiva 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> A. y e. x ( ( H |` x ) ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
100 ffnfv 
 |-  ( ( H |` x ) : x --> ( ( Cntz ` G ) ` { ( F ` k ) } ) <-> ( ( H |` x ) Fn x /\ A. y e. x ( ( H |` x ) ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) ) )
101 70 99 100 sylanbrc 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) : x --> ( ( Cntz ` G ) ` { ( F ` k ) } ) )
102 resss 
 |-  ( H |` x ) C_ H
103 102 rnssi 
 |-  ran ( H |` x ) C_ ran H
104 50 cntzidss 
 |-  ( ( ran H C_ ( ( Cntz ` G ) ` ran H ) /\ ran ( H |` x ) C_ ran H ) -> ran ( H |` x ) C_ ( ( Cntz ` G ) ` ran ( H |` x ) ) )
105 54 103 104 sylancl 
 |-  ( ph -> ran ( H |` x ) C_ ( ( Cntz ` G ) ` ran ( H |` x ) ) )
106 105 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ran ( H |` x ) C_ ( ( Cntz ` G ) ` ran ( H |` x ) ) )
107 22 27 fsuppres 
 |-  ( ph -> ( H |` x ) finSupp .0. )
108 107 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) finSupp .0. )
109 1 50 56 58 65 101 106 108 gsumzsubmcl 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( G gsum ( H |` x ) ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
110 109 snssd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( G gsum ( H |` x ) ) } C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) )
111 66 68 fssresd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) : x --> ( Base ` G ) )
112 11 1 50 56 58 111 106 108 gsumzcl 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( G gsum ( H |` x ) ) e. ( Base ` G ) )
113 112 snssd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( G gsum ( H |` x ) ) } C_ ( Base ` G ) )
114 11 50 cntzrec 
 |-  ( ( { ( G gsum ( H |` x ) ) } C_ ( Base ` G ) /\ { ( F ` k ) } C_ ( Base ` G ) ) -> ( { ( G gsum ( H |` x ) ) } C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) <-> { ( F ` k ) } C_ ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) ) )
115 113 63 114 syl2anc 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( { ( G gsum ( H |` x ) ) } C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) <-> { ( F ` k ) } C_ ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) ) )
116 110 115 mpbid 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( F ` k ) } C_ ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) )
117 fvex 
 |-  ( F ` k ) e. _V
118 117 snss 
 |-  ( ( F ` k ) e. ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) <-> { ( F ` k ) } C_ ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) )
119 116 118 sylibr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( F ` k ) e. ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) )
120 11 1 7 50 51 8 21 22 52 12 14 53 54 55 119 gsumzaddlem 
 |-  ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )
121 49 120 jca 
 |-  ( ph -> ( ( F oF .+ H ) e. W /\ ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) )