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		resexg	|- ( F e. V -> ( F |` y ) e. _V )
9	1 8	syl	|- ( ph -> ( F |` y ) e. _V )
10	9 2 3 4 5	gsumpropd	|- ( ph -> ( G gsum ( F |` y ) ) = ( H gsum ( F |` y ) ) )
11	10	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 ) ) ) )
12	7 11	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 ) ) ) ) )
13		eqid	|- ( Base ` G ) = ( Base ` G )
14		eqid	|- ( TopOpen ` G ) = ( TopOpen ` G )
15		eqid	|- ( ~P dom F i^i Fin ) = ( ~P dom F i^i Fin )
16		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 } )
17		eqidd	|- ( ph -> dom F = dom F )
18	13 14 15 16 2 1 17	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 ) ) ) ) )
19		eqid	|- ( Base ` H ) = ( Base ` H )
20		eqid	|- ( TopOpen ` H ) = ( TopOpen ` H )
21	19 20 15 16 3 1 17	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 ) ) ) ) )
22	12 18 21	3eqtr4d	|- ( ph -> ( G tsums F ) = ( H tsums F ) )