Metamath Proof Explorer


Theorem tsmssub

Description: The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses tsmssub.b B = Base G
tsmssub.p - ˙ = - G
tsmssub.1 φ G CMnd
tsmssub.2 φ G TopGrp
tsmssub.a φ A V
tsmssub.f φ F : A B
tsmssub.h φ H : A B
tsmssub.x φ X G tsums F
tsmssub.y φ Y G tsums H
Assertion tsmssub φ X - ˙ Y G tsums F - ˙ f H

Proof

Step Hyp Ref Expression
1 tsmssub.b B = Base G
2 tsmssub.p - ˙ = - G
3 tsmssub.1 φ G CMnd
4 tsmssub.2 φ G TopGrp
5 tsmssub.a φ A V
6 tsmssub.f φ F : A B
7 tsmssub.h φ H : A B
8 tsmssub.x φ X G tsums F
9 tsmssub.y φ Y G tsums H
10 eqid + G = + G
11 tgptmd G TopGrp G TopMnd
12 4 11 syl φ G TopMnd
13 tgpgrp G TopGrp G Grp
14 eqid inv g G = inv g G
15 1 14 grpinvf G Grp inv g G : B B
16 4 13 15 3syl φ inv g G : B B
17 fco inv g G : B B H : A B inv g G H : A B
18 16 7 17 syl2anc φ inv g G H : A B
19 1 14 3 4 5 7 9 tsmsinv φ inv g G Y G tsums inv g G H
20 1 10 3 12 5 6 18 8 19 tsmsadd φ X + G inv g G Y G tsums F + G f inv g G H
21 tgptps G TopGrp G TopSp
22 4 21 syl φ G TopSp
23 1 3 22 5 6 tsmscl φ G tsums F B
24 23 8 sseldd φ X B
25 1 3 22 5 7 tsmscl φ G tsums H B
26 25 9 sseldd φ Y B
27 1 10 14 2 grpsubval X B Y B X - ˙ Y = X + G inv g G Y
28 24 26 27 syl2anc φ X - ˙ Y = X + G inv g G Y
29 6 ffvelrnda φ k A F k B
30 7 ffvelrnda φ k A H k B
31 1 10 14 2 grpsubval F k B H k B F k - ˙ H k = F k + G inv g G H k
32 29 30 31 syl2anc φ k A F k - ˙ H k = F k + G inv g G H k
33 32 mpteq2dva φ k A F k - ˙ H k = k A F k + G inv g G H k
34 6 feqmptd φ F = k A F k
35 7 feqmptd φ H = k A H k
36 5 29 30 34 35 offval2 φ F - ˙ f H = k A F k - ˙ H k
37 fvexd φ k A inv g G H k V
38 16 feqmptd φ inv g G = x B inv g G x
39 fveq2 x = H k inv g G x = inv g G H k
40 30 35 38 39 fmptco φ inv g G H = k A inv g G H k
41 5 29 37 34 40 offval2 φ F + G f inv g G H = k A F k + G inv g G H k
42 33 36 41 3eqtr4d φ F - ˙ f H = F + G f inv g G H
43 42 oveq2d φ G tsums F - ˙ f H = G tsums F + G f inv g G H
44 20 28 43 3eltr4d φ X - ˙ Y G tsums F - ˙ f H