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 ˙ = 0 G
eldprdi.w W = h i I S i | finSupp 0 ˙ h
eldprdi.1 φ G dom DProd S
eldprdi.2 φ dom S = I
eldprdi.3 φ F W
dprdfadd.4 φ H W
dprdfsub.b - ˙ = - G
Assertion dprdfsub φ F - ˙ f H W G F - ˙ f H = G F - ˙ G H

Proof

Step Hyp Ref Expression
1 eldprdi.0 0 ˙ = 0 G
2 eldprdi.w W = h i I S i | finSupp 0 ˙ h
3 eldprdi.1 φ G dom DProd S
4 eldprdi.2 φ dom S = I
5 eldprdi.3 φ F W
6 dprdfadd.4 φ H W
7 dprdfsub.b - ˙ = - G
8 eqid Base G = Base G
9 2 3 4 5 8 dprdff φ F : I Base G
10 9 ffvelrnda φ k I F k Base G
11 2 3 4 6 8 dprdff φ H : I Base G
12 11 ffvelrnda φ k I H k Base G
13 eqid + G = + G
14 eqid inv g G = inv g G
15 8 13 14 7 grpsubval F k Base G H k Base G F k - ˙ H k = F k + G inv g G H k
16 10 12 15 syl2anc φ k I F k - ˙ H k = F k + G inv g G H k
17 16 mpteq2dva φ k I F k - ˙ H k = k I F k + G inv g G H k
18 3 4 dprddomcld φ I V
19 9 feqmptd φ F = k I F k
20 11 feqmptd φ H = k I H k
21 18 10 12 19 20 offval2 φ F - ˙ f H = k I F k - ˙ H k
22 fvexd φ k I inv g G H k V
23 dprdgrp G dom DProd S G Grp
24 3 23 syl φ G Grp
25 8 14 24 grpinvf1o φ inv g G : Base G 1-1 onto Base G
26 f1of inv g G : Base G 1-1 onto Base G inv g G : Base G Base G
27 25 26 syl φ inv g G : Base G Base G
28 27 feqmptd φ inv g G = x Base G inv g G x
29 fveq2 x = H k inv g G x = inv g G H k
30 12 20 28 29 fmptco φ inv g G H = k I inv g G H k
31 18 10 22 19 30 offval2 φ F + G f inv g G H = k I F k + G inv g G H k
32 17 21 31 3eqtr4d φ F - ˙ f H = F + G f inv g G H
33 1 2 3 4 6 14 dprdfinv φ inv g G H W G inv g G H = inv g G G H
34 33 simpld φ inv g G H W
35 1 2 3 4 5 34 13 dprdfadd φ F + G f inv g G H W G F + G f inv g G H = G F + G G inv g G H
36 35 simpld φ F + G f inv g G H W
37 32 36 eqeltrd φ F - ˙ f H W
38 32 oveq2d φ G F - ˙ f H = G F + G f inv g G H
39 33 simprd φ G inv g G H = inv g G G H
40 39 oveq2d φ G F + G G inv g G H = G F + G inv g G G H
41 35 simprd φ G F + G f inv g G H = G F + G G inv g G H
42 8 dprdssv G DProd S Base G
43 1 2 3 4 5 eldprdi φ G F G DProd S
44 42 43 sselid φ G F Base G
45 1 2 3 4 6 eldprdi φ G H G DProd S
46 42 45 sselid φ G H Base G
47 8 13 14 7 grpsubval G F Base G G H Base G G F - ˙ G H = G F + G inv g G G H
48 44 46 47 syl2anc φ G F - ˙ G H = G F + G inv g G G H
49 40 41 48 3eqtr4d φ G F + G f inv g G H = G F - ˙ G H
50 38 49 eqtrd φ G F - ˙ f H = G F - ˙ G H
51 37 50 jca φ F - ˙ f H W G F - ˙ f H = G F - ˙ G H