Metamath Proof Explorer

Theorem tsmsadd

Description: The sum of two infinite group sums. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmsadd.b 
|- B = ( Base ` G )
tsmsadd.p 
|- .+ = ( +g ` G )
tsmsadd.1 
|- ( ph -> G e. CMnd )
tsmsadd.2 
|- ( ph -> G e. TopMnd )
tsmsadd.a 
|- ( ph -> A e. V )
tsmsadd.f 
|- ( ph -> F : A --> B )
tsmsadd.h 
|- ( ph -> H : A --> B )
tsmsadd.x 
|- ( ph -> X e. ( G tsums F ) )
tsmsadd.y 
|- ( ph -> Y e. ( G tsums H ) )
Assertion tsmsadd 
|- ( ph -> ( X .+ Y ) e. ( G tsums ( F oF .+ H ) ) )

Proof

Step Hyp Ref Expression
1 tsmsadd.b 
 |-  B = ( Base ` G )
2 tsmsadd.p 
 |-  .+ = ( +g ` G )
3 tsmsadd.1 
 |-  ( ph -> G e. CMnd )
4 tsmsadd.2 
 |-  ( ph -> G e. TopMnd )
5 tsmsadd.a 
 |-  ( ph -> A e. V )
6 tsmsadd.f 
 |-  ( ph -> F : A --> B )
7 tsmsadd.h 
 |-  ( ph -> H : A --> B )
8 tsmsadd.x 
 |-  ( ph -> X e. ( G tsums F ) )
9 tsmsadd.y 
 |-  ( ph -> Y e. ( G tsums H ) )
10 tmdtps 
 |-  ( G e. TopMnd -> G e. TopSp )
11 4 10 syl 
 |-  ( ph -> G e. TopSp )
12 1 3 11 5 6 tsmscl 
 |-  ( ph -> ( G tsums F ) C_ B )
13 12 8 sseldd 
 |-  ( ph -> X e. B )
14 1 3 11 5 7 tsmscl 
 |-  ( ph -> ( G tsums H ) C_ B )
15 14 9 sseldd 
 |-  ( ph -> Y e. B )
16 eqid 
 |-  ( +f ` G ) = ( +f ` G )
17 1 2 16 plusfval 
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( +f ` G ) Y ) = ( X .+ Y ) )
18 13 15 17 syl2anc 
 |-  ( ph -> ( X ( +f ` G ) Y ) = ( X .+ Y ) )
19 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
20 1 19 istps 
 |-  ( G e. TopSp <-> ( TopOpen ` G ) e. ( TopOn ` B ) )
21 11 20 sylib 
 |-  ( ph -> ( TopOpen ` G ) e. ( TopOn ` B ) )
22 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
23 eqid 
 |-  ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } )
24 eqid 
 |-  ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } )
25 22 23 24 5 tsmsfbas 
 |-  ( ph -> ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) )
26 fgcl 
 |-  ( ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
27 25 26 syl 
 |-  ( ph -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
28 1 22 3 5 6 tsmslem1 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` z ) ) e. B )
29 1 22 3 5 7 tsmslem1 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( H |` z ) ) e. B )
30 1 19 22 24 3 5 6 tsmsval 
 |-  ( ph -> ( G tsums F ) = ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) )
31 8 30 eleqtrd 
 |-  ( ph -> X e. ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) )
32 1 19 22 24 3 5 7 tsmsval 
 |-  ( ph -> ( G tsums H ) = ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( H |` z ) ) ) ) )
33 9 32 eleqtrd 
 |-  ( ph -> Y e. ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( H |` z ) ) ) ) )
34 19 16 tmdcn 
 |-  ( G e. TopMnd -> ( +f ` G ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
35 4 34 syl 
 |-  ( ph -> ( +f ` G ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
36 13 15 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
37 txtopon 
 |-  ( ( ( TopOpen ` G ) e. ( TopOn ` B ) /\ ( TopOpen ` G ) e. ( TopOn ` B ) ) -> ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) e. ( TopOn ` ( B X. B ) ) )
38 21 21 37 syl2anc 
 |-  ( ph -> ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) e. ( TopOn ` ( B X. B ) ) )
39 toponuni 
 |-  ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) e. ( TopOn ` ( B X. B ) ) -> ( B X. B ) = U. ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) )
40 38 39 syl 
 |-  ( ph -> ( B X. B ) = U. ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) )
41 36 40 eleqtrd 
 |-  ( ph -> <. X , Y >. e. U. ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) )
42 eqid 
 |-  U. ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) = U. ( ( TopOpen ` G ) tX ( TopOpen ` G ) )
43 42 cncnpi 
 |-  ( ( ( +f ` G ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) /\ <. X , Y >. e. U. ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) ) -> ( +f ` G ) e. ( ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) CnP ( TopOpen ` G ) ) ` <. X , Y >. ) )
44 35 41 43 syl2anc 
 |-  ( ph -> ( +f ` G ) e. ( ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) CnP ( TopOpen ` G ) ) ` <. X , Y >. ) )
45 21 21 27 28 29 31 33 44 flfcnp2 
 |-  ( ph -> ( X ( +f ` G ) Y ) e. ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) ) ) )
46 18 45 eqeltrrd 
 |-  ( ph -> ( X .+ Y ) e. ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) ) ) )
47 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
48 3 47 syl 
 |-  ( ph -> G e. Mnd )
49 1 2 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
50 49 3expb 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
51 48 50 sylan 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
52 inidm 
 |-  ( A i^i A ) = A
53 51 6 7 5 5 52 off 
 |-  ( ph -> ( F oF .+ H ) : A --> B )
54 1 19 22 24 3 5 53 tsmsval 
 |-  ( ph -> ( G tsums ( F oF .+ H ) ) = ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( ( F oF .+ H ) |` z ) ) ) ) )
55 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
56 3 adantr 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> G e. CMnd )
57 elinel2 
 |-  ( z e. ( ~P A i^i Fin ) -> z e. Fin )
58 57 adantl 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> z e. Fin )
59 elfpw 
 |-  ( z e. ( ~P A i^i Fin ) <-> ( z C_ A /\ z e. Fin ) )
60 59 simplbi 
 |-  ( z e. ( ~P A i^i Fin ) -> z C_ A )
61 fssres 
 |-  ( ( F : A --> B /\ z C_ A ) -> ( F |` z ) : z --> B )
62 6 60 61 syl2an 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) : z --> B )
63 fssres 
 |-  ( ( H : A --> B /\ z C_ A ) -> ( H |` z ) : z --> B )
64 7 60 63 syl2an 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( H |` z ) : z --> B )
65 fvexd 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( 0g ` G ) e. _V )
66 62 58 65 fdmfifsupp 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) finSupp ( 0g ` G ) )
67 64 58 65 fdmfifsupp 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( H |` z ) finSupp ( 0g ` G ) )
68 1 55 2 56 58 62 64 66 67 gsumadd 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( ( F |` z ) oF .+ ( H |` z ) ) ) = ( ( G gsum ( F |` z ) ) .+ ( G gsum ( H |` z ) ) ) )
69 6 5 fexd 
 |-  ( ph -> F e. _V )
70 7 5 fexd 
 |-  ( ph -> H e. _V )
71 offres 
 |-  ( ( F e. _V /\ H e. _V ) -> ( ( F oF .+ H ) |` z ) = ( ( F |` z ) oF .+ ( H |` z ) ) )
72 69 70 71 syl2anc 
 |-  ( ph -> ( ( F oF .+ H ) |` z ) = ( ( F |` z ) oF .+ ( H |` z ) ) )
73 72 adantr 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( ( F oF .+ H ) |` z ) = ( ( F |` z ) oF .+ ( H |` z ) ) )
74 73 oveq2d 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( ( F oF .+ H ) |` z ) ) = ( G gsum ( ( F |` z ) oF .+ ( H |` z ) ) ) )
75 1 2 16 plusfval 
 |-  ( ( ( G gsum ( F |` z ) ) e. B /\ ( G gsum ( H |` z ) ) e. B ) -> ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) = ( ( G gsum ( F |` z ) ) .+ ( G gsum ( H |` z ) ) ) )
76 28 29 75 syl2anc 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) = ( ( G gsum ( F |` z ) ) .+ ( G gsum ( H |` z ) ) ) )
77 68 74 76 3eqtr4d 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( ( F oF .+ H ) |` z ) ) = ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) )
78 77 mpteq2dva 
 |-  ( ph -> ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( ( F oF .+ H ) |` z ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) ) )
79 78 fveq2d 
 |-  ( ph -> ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( ( F oF .+ H ) |` z ) ) ) ) = ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) ) ) )
80 54 79 eqtrd 
 |-  ( ph -> ( G tsums ( F oF .+ H ) ) = ( ( ( TopOpen ` G ) fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( ( G gsum ( F |` z ) ) ( +f ` G ) ( G gsum ( H |` z ) ) ) ) ) )
81 46 80 eleqtrrd 
 |-  ( ph -> ( X .+ Y ) e. ( G tsums ( F oF .+ H ) ) )