Metamath Proof Explorer

Theorem dprdfsub

Description: Take the difference 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 )
dprdfsub.b 
|- .- = ( -g ` G )
Assertion dprdfsub 
|- ( 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 dprdfsub.b 
 |-  .- = ( -g ` G )
8 eqid 
 |-  ( Base ` G ) = ( Base ` G )
9 2 3 4 5 8 dprdff 
 |-  ( ph -> F : I --> ( Base ` G ) )
10 9 ffvelrnda 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. ( Base ` G ) )
11 2 3 4 6 8 dprdff 
 |-  ( ph -> H : I --> ( Base ` G ) )
12 11 ffvelrnda 
 |-  ( ( ph /\ k e. I ) -> ( H ` k ) e. ( Base ` G ) )
13 eqid 
 |-  ( +g ` G ) = ( +g ` G )
14 eqid 
 |-  ( invg ` G ) = ( invg ` G )
15 8 13 14 7 grpsubval 
 |-  ( ( ( F ` k ) e. ( Base ` G ) /\ ( H ` k ) e. ( Base ` G ) ) -> ( ( F ` k ) .- ( H ` k ) ) = ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) )
16 10 12 15 syl2anc 
 |-  ( ( ph /\ k e. I ) -> ( ( F ` k ) .- ( H ` k ) ) = ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) )
17 16 mpteq2dva 
 |-  ( ph -> ( k e. I |-> ( ( F ` k ) .- ( H ` k ) ) ) = ( k e. I |-> ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) ) )
18 3 4 dprddomcld 
 |-  ( ph -> I e. _V )
19 9 feqmptd 
 |-  ( ph -> F = ( k e. I |-> ( F ` k ) ) )
20 11 feqmptd 
 |-  ( ph -> H = ( k e. I |-> ( H ` k ) ) )
21 18 10 12 19 20 offval2 
 |-  ( ph -> ( F oF .- H ) = ( k e. I |-> ( ( F ` k ) .- ( H ` k ) ) ) )
22 fvexd 
 |-  ( ( ph /\ k e. I ) -> ( ( invg ` G ) ` ( H ` k ) ) e. _V )
23 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
24 3 23 syl 
 |-  ( ph -> G e. Grp )
25 8 14 24 grpinvf1o 
 |-  ( ph -> ( invg ` G ) : ( Base ` G ) -1-1-onto-> ( Base ` G ) )
26 f1of 
 |-  ( ( invg ` G ) : ( Base ` G ) -1-1-onto-> ( Base ` G ) -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
27 25 26 syl 
 |-  ( ph -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
28 27 feqmptd 
 |-  ( ph -> ( invg ` G ) = ( x e. ( Base ` G ) |-> ( ( invg ` G ) ` x ) ) )
29 fveq2 
 |-  ( x = ( H ` k ) -> ( ( invg ` G ) ` x ) = ( ( invg ` G ) ` ( H ` k ) ) )
30 12 20 28 29 fmptco 
 |-  ( ph -> ( ( invg ` G ) o. H ) = ( k e. I |-> ( ( invg ` G ) ` ( H ` k ) ) ) )
31 18 10 22 19 30 offval2 
 |-  ( ph -> ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) = ( k e. I |-> ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) ) )
32 17 21 31 3eqtr4d 
 |-  ( ph -> ( F oF .- H ) = ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) )
33 1 2 3 4 6 14 dprdfinv 
 |-  ( ph -> ( ( ( invg ` G ) o. H ) e. W /\ ( G gsum ( ( invg ` G ) o. H ) ) = ( ( invg ` G ) ` ( G gsum H ) ) ) )
34 33 simpld 
 |-  ( ph -> ( ( invg ` G ) o. H ) e. W )
35 1 2 3 4 5 34 13 dprdfadd 
 |-  ( ph -> ( ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) e. W /\ ( G gsum ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) ) = ( ( G gsum F ) ( +g ` G ) ( G gsum ( ( invg ` G ) o. H ) ) ) ) )
36 35 simpld 
 |-  ( ph -> ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) e. W )
37 32 36 eqeltrd 
 |-  ( ph -> ( F oF .- H ) e. W )
38 32 oveq2d 
 |-  ( ph -> ( G gsum ( F oF .- H ) ) = ( G gsum ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) ) )
39 33 simprd 
 |-  ( ph -> ( G gsum ( ( invg ` G ) o. H ) ) = ( ( invg ` G ) ` ( G gsum H ) ) )
40 39 oveq2d 
 |-  ( ph -> ( ( G gsum F ) ( +g ` G ) ( G gsum ( ( invg ` G ) o. H ) ) ) = ( ( G gsum F ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum H ) ) ) )
41 35 simprd 
 |-  ( ph -> ( G gsum ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) ) = ( ( G gsum F ) ( +g ` G ) ( G gsum ( ( invg ` G ) o. H ) ) ) )
42 8 dprdssv 
 |-  ( G DProd S ) C_ ( Base ` G )
43 1 2 3 4 5 eldprdi 
 |-  ( ph -> ( G gsum F ) e. ( G DProd S ) )
44 42 43 sselid 
 |-  ( ph -> ( G gsum F ) e. ( Base ` G ) )
45 1 2 3 4 6 eldprdi 
 |-  ( ph -> ( G gsum H ) e. ( G DProd S ) )
46 42 45 sselid 
 |-  ( ph -> ( G gsum H ) e. ( Base ` G ) )
47 8 13 14 7 grpsubval 
 |-  ( ( ( G gsum F ) e. ( Base ` G ) /\ ( G gsum H ) e. ( Base ` G ) ) -> ( ( G gsum F ) .- ( G gsum H ) ) = ( ( G gsum F ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum H ) ) ) )
48 44 46 47 syl2anc 
 |-  ( ph -> ( ( G gsum F ) .- ( G gsum H ) ) = ( ( G gsum F ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum H ) ) ) )
49 40 41 48 3eqtr4d 
 |-  ( ph -> ( G gsum ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )
50 38 49 eqtrd 
 |-  ( ph -> ( G gsum ( F oF .- H ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )
51 37 50 jca 
 |-  ( ph -> ( ( F oF .- H ) e. W /\ ( G gsum ( F oF .- H ) ) = ( ( G gsum F ) .- ( G gsum H ) ) ) )