This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tsmspropd

Description: The group sum depends only on the base set, additive operation, and topology components. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd etc. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses tsmspropd.f 
|- ( ph -> F e. V )
tsmspropd.g 
|- ( ph -> G e. W )
tsmspropd.h 
|- ( ph -> H e. X )
tsmspropd.b 
|- ( ph -> ( Base ` G ) = ( Base ` H ) )
tsmspropd.p 
|- ( ph -> ( +g ` G ) = ( +g ` H ) )
tsmspropd.j 
|- ( ph -> ( TopOpen ` G ) = ( TopOpen ` H ) )
Assertion tsmspropd 
|- ( ph -> ( G tsums F ) = ( H tsums F ) )

Proof

Step Hyp Ref Expression
1 tsmspropd.f 
 |-  ( ph -> F e. V )
2 tsmspropd.g 
 |-  ( ph -> G e. W )
3 tsmspropd.h 
 |-  ( ph -> H e. X )
4 tsmspropd.b 
 |-  ( ph -> ( Base ` G ) = ( Base ` H ) )
5 tsmspropd.p 
 |-  ( ph -> ( +g ` G ) = ( +g ` H ) )
6 tsmspropd.j 
 |-  ( ph -> ( TopOpen ` G ) = ( TopOpen ` H ) )
7 6 oveq1d 
 |-  ( ph -> ( ( TopOpen ` G ) fLimf ( ( ~P dom F i^i Fin ) filGen ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } ) ) ) = ( ( TopOpen ` H ) fLimf ( ( ~P dom F i^i Fin ) filGen ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } ) ) ) )
8 1 resexd 
 |-  ( ph -> ( F |` y ) e. _V )
9 8 2 3 4 5 gsumpropd 
 |-  ( ph -> ( G gsum ( F |` y ) ) = ( H gsum ( F |` y ) ) )
10 9 mpteq2dv 
 |-  ( ph -> ( y e. ( ~P dom F i^i Fin ) |-> ( G gsum ( F |` y ) ) ) = ( y e. ( ~P dom F i^i Fin ) |-> ( H gsum ( F |` y ) ) ) )
11 7 10 fveq12d 
 |-  ( ph -> ( ( ( TopOpen ` G ) fLimf ( ( ~P dom F i^i Fin ) filGen ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } ) ) ) ` ( y e. ( ~P dom F i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) = ( ( ( TopOpen ` H ) fLimf ( ( ~P dom F i^i Fin ) filGen ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } ) ) ) ` ( y e. ( ~P dom F i^i Fin ) |-> ( H gsum ( F |` y ) ) ) ) )
12 eqid 
 |-  ( Base ` G ) = ( Base ` G )
13 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
14 eqid 
 |-  ( ~P dom F i^i Fin ) = ( ~P dom F i^i Fin )
15 eqid 
 |-  ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } ) = ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } )
16 eqidd 
 |-  ( ph -> dom F = dom F )
17 12 13 14 15 2 1 16 tsmsval2 
 |-  ( ph -> ( G tsums F ) = ( ( ( TopOpen ` G ) fLimf ( ( ~P dom F i^i Fin ) filGen ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } ) ) ) ` ( y e. ( ~P dom F i^i Fin ) |-> ( G gsum ( F |` y ) ) ) ) )
18 eqid 
 |-  ( Base ` H ) = ( Base ` H )
19 eqid 
 |-  ( TopOpen ` H ) = ( TopOpen ` H )
20 18 19 14 15 3 1 16 tsmsval2 
 |-  ( ph -> ( H tsums F ) = ( ( ( TopOpen ` H ) fLimf ( ( ~P dom F i^i Fin ) filGen ran ( z e. ( ~P dom F i^i Fin ) |-> { y e. ( ~P dom F i^i Fin ) | z C_ y } ) ) ) ` ( y e. ( ~P dom F i^i Fin ) |-> ( H gsum ( F |` y ) ) ) ) )
21 11 17 20 3eqtr4d 
 |-  ( ph -> ( G tsums F ) = ( H tsums F ) )