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 ` G )
tsmssub.1
|- ( ph -> G e. CMnd )
tsmssub.2
|- ( ph -> G e. TopGrp )
tsmssub.a
|- ( ph -> A e. V )
tsmssub.f
|- ( ph -> F : A --> B )
tsmssub.h
|- ( ph -> H : A --> B )
tsmssub.x
|- ( ph -> X e. ( G tsums F ) )
tsmssub.y
|- ( ph -> Y e. ( G tsums H ) )
Assertion tsmssub
|- ( ph -> ( X .- Y ) e. ( G tsums ( F oF .- H ) ) )

Proof

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