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 ) ) )