Theorem gsumpropd2

Description: A stronger version of gsumpropd , working for magma, where only the closure of the addition operation on a common base is required, see gsummgmpropd . (Contributed by Thierry Arnoux, 28-Jun-2017)

	Ref	Expression
Hypotheses	gsumpropd2.f	|- ( ph -> F e. V )
	gsumpropd2.g	|- ( ph -> G e. W )
	gsumpropd2.h	|- ( ph -> H e. X )
	gsumpropd2.b	|- ( ph -> ( Base ` G ) = ( Base ` H ) )
	gsumpropd2.c	|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )
	gsumpropd2.e	|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )
	gsumpropd2.n	|- ( ph -> Fun F )
	gsumpropd2.r	|- ( ph -> ran F C_ ( Base ` G ) )
Assertion	gsumpropd2	|- ( ph -> ( G gsum F ) = ( H gsum F ) )

Proof

Step	Hyp	Ref	Expression
1		gsumpropd2.f	|- ( ph -> F e. V )
2		gsumpropd2.g	|- ( ph -> G e. W )
3		gsumpropd2.h	|- ( ph -> H e. X )
4		gsumpropd2.b	|- ( ph -> ( Base ` G ) = ( Base ` H ) )
5		gsumpropd2.c	|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )
6		gsumpropd2.e	|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )
7		gsumpropd2.n	|- ( ph -> Fun F )
8		gsumpropd2.r	|- ( ph -> ran F C_ ( Base ` G ) )
9		eqid	|- ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) ) = ( `' F " ( _V \ { s e. ( Base ` G ) | A. t e. ( Base ` G ) ( ( s ( +g ` G ) t ) = t /\ ( t ( +g ` G ) s ) = t ) } ) )
10		eqid	|- ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) ) = ( `' F " ( _V \ { s e. ( Base ` H ) | A. t e. ( Base ` H ) ( ( s ( +g ` H ) t ) = t /\ ( t ( +g ` H ) s ) = t ) } ) )
11	1 2 3 4 5 6 7 8 9 10	gsumpropd2lem	|- ( ph -> ( G gsum F ) = ( H gsum F ) )