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 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
52 34 51 syl 
 |-  ( ph -> G e. Mnd )
53 eqid 
 |-  ( ( F u. H ) supp .0. ) = ( ( F u. H ) supp .0. )
54 2 3 4 5 50 dprdfcntz 
 |-  ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
55 2 3 4 6 50 dprdfcntz 
 |-  ( ph -> ran H C_ ( ( Cntz ` G ) ` ran H ) )
56 2 3 4 49 50 dprdfcntz 
 |-  ( ph -> ran ( F oF .+ H ) C_ ( ( Cntz ` G ) ` ran ( F oF .+ H ) ) )
57 52 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> G e. Mnd )
58 vex 
 |-  x e. _V
59 58 a1i 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> x e. _V )
60 eldifi 
 |-  ( k e. ( I \ x ) -> k e. I )
61 60 adantl 
 |-  ( ( x C_ I /\ k e. ( I \ x ) ) -> k e. I )
62 ffvelrn 
 |-  ( ( F : I --> ( Base ` G ) /\ k e. I ) -> ( F ` k ) e. ( Base ` G ) )
63 12 61 62 syl2an 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( F ` k ) e. ( Base ` G ) )
64 63 snssd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( F ` k ) } C_ ( Base ` G ) )
65 11 50 cntzsubm 
 |-  ( ( G e. Mnd /\ { ( F ` k ) } C_ ( Base ` G ) ) -> ( ( Cntz ` G ) ` { ( F ` k ) } ) e. ( SubMnd ` G ) )
66 57 64 65 syl2anc 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( ( Cntz ` G ) ` { ( F ` k ) } ) e. ( SubMnd ` G ) )
67 14 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> H : I --> ( Base ` G ) )
68 67 ffnd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> H Fn I )
69 simprl 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> x C_ I )
70 fnssres 
 |-  ( ( H Fn I /\ x C_ I ) -> ( H |` x ) Fn x )
71 68 69 70 syl2anc 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) Fn x )
72 fvres 
 |-  ( y e. x -> ( ( H |` x ) ` y ) = ( H ` y ) )
73 72 adantl 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( ( H |` x ) ` y ) = ( H ` y ) )
74 3 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> G dom DProd S )
75 4 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> dom S = I )
76 74 75 dprdf2 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> S : I --> ( SubGrp ` G ) )
77 61 ad2antlr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> k e. I )
78 76 77 ffvelrnd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( S ` k ) e. ( SubGrp ` G ) )
79 11 subgss 
 |-  ( ( S ` k ) e. ( SubGrp ` G ) -> ( S ` k ) C_ ( Base ` G ) )
80 78 79 syl 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( S ` k ) C_ ( Base ` G ) )
81 5 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> F e. W )
82 2 74 75 81 dprdfcl 
 |-  ( ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) /\ k e. I ) -> ( F ` k ) e. ( S ` k ) )
83 77 82 mpdan 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( F ` k ) e. ( S ` k ) )
84 83 snssd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> { ( F ` k ) } C_ ( S ` k ) )
85 11 50 cntz2ss 
 |-  ( ( ( S ` k ) C_ ( Base ` G ) /\ { ( F ` k ) } C_ ( S ` k ) ) -> ( ( Cntz ` G ) ` ( S ` k ) ) C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) )
86 80 84 85 syl2anc 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( ( Cntz ` G ) ` ( S ` k ) ) C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) )
87 69 sselda 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> y e. I )
88 simpr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> y e. x )
89 simplrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> k e. ( I \ x ) )
90 89 eldifbd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> -. k e. x )
91 nelne2 
 |-  ( ( y e. x /\ -. k e. x ) -> y =/= k )
92 88 90 91 syl2anc 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> y =/= k )
93 74 75 87 77 92 50 dprdcntz 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( S ` y ) C_ ( ( Cntz ` G ) ` ( S ` k ) ) )
94 6 ad2antrr 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> H e. W )
95 2 74 75 94 dprdfcl 
 |-  ( ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) /\ y e. I ) -> ( H ` y ) e. ( S ` y ) )
96 87 95 mpdan 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( H ` y ) e. ( S ` y ) )
97 93 96 sseldd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( H ` y ) e. ( ( Cntz ` G ) ` ( S ` k ) ) )
98 86 97 sseldd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( H ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
99 73 98 eqeltrd 
 |-  ( ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) /\ y e. x ) -> ( ( H |` x ) ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
100 99 ralrimiva 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> A. y e. x ( ( H |` x ) ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
101 ffnfv 
 |-  ( ( H |` x ) : x --> ( ( Cntz ` G ) ` { ( F ` k ) } ) <-> ( ( H |` x ) Fn x /\ A. y e. x ( ( H |` x ) ` y ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) ) )
102 71 100 101 sylanbrc 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) : x --> ( ( Cntz ` G ) ` { ( F ` k ) } ) )
103 resss 
 |-  ( H |` x ) C_ H
104 103 rnssi 
 |-  ran ( H |` x ) C_ ran H
105 50 cntzidss 
 |-  ( ( ran H C_ ( ( Cntz ` G ) ` ran H ) /\ ran ( H |` x ) C_ ran H ) -> ran ( H |` x ) C_ ( ( Cntz ` G ) ` ran ( H |` x ) ) )
106 55 104 105 sylancl 
 |-  ( ph -> ran ( H |` x ) C_ ( ( Cntz ` G ) ` ran ( H |` x ) ) )
107 106 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ran ( H |` x ) C_ ( ( Cntz ` G ) ` ran ( H |` x ) ) )
108 22 27 fsuppres 
 |-  ( ph -> ( H |` x ) finSupp .0. )
109 108 adantr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) finSupp .0. )
110 1 50 57 59 66 102 107 109 gsumzsubmcl 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( G gsum ( H |` x ) ) e. ( ( Cntz ` G ) ` { ( F ` k ) } ) )
111 110 snssd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( G gsum ( H |` x ) ) } C_ ( ( Cntz ` G ) ` { ( F ` k ) } ) )
112 67 69 fssresd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( H |` x ) : x --> ( Base ` G ) )
113 11 1 50 57 59 112 107 109 gsumzcl 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( G gsum ( H |` x ) ) e. ( Base ` G ) )
114 113 snssd 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( G gsum ( H |` x ) ) } C_ ( Base ` G ) )
115 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 ) ) } ) ) )
116 114 64 115 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 ) ) } ) ) )
117 111 116 mpbid 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> { ( F ` k ) } C_ ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) )
118 fvex 
 |-  ( F ` k ) e. _V
119 118 snss 
 |-  ( ( F ` k ) e. ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) <-> { ( F ` k ) } C_ ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) )
120 117 119 sylibr 
 |-  ( ( ph /\ ( x C_ I /\ k e. ( I \ x ) ) ) -> ( F ` k ) e. ( ( Cntz ` G ) ` { ( G gsum ( H |` x ) ) } ) )
121 11 1 7 50 52 8 21 22 53 12 14 54 55 56 120 gsumzaddlem 
 |-  ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )
122 49 121 jca 
 |-  ( ph -> ( ( F oF .+ H ) e. W /\ ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) )