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