Theorem gsummgmpropd

Description: A stronger version of gsumpropd if at least one of the involved structures is a magma, see gsumpropd2 . (Contributed by AV, 31-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		gsummgmpropd.f	|- ( ph -> F e. V )
2		gsummgmpropd.g	|- ( ph -> G e. W )
3		gsummgmpropd.h	|- ( ph -> H e. X )
4		gsummgmpropd.b	|- ( ph -> ( Base ` G ) = ( Base ` H ) )
5		gsummgmpropd.m	|- ( ph -> G e. Mgm )
6		gsummgmpropd.e	|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )
7		gsummgmpropd.n	|- ( ph -> Fun F )
8		gsummgmpropd.r	|- ( ph -> ran F C_ ( Base ` G ) )
9		eqid	|- ( Base ` G ) = ( Base ` G )
10		eqid	|- ( +g ` G ) = ( +g ` G )
11	9 10	mgmcl	|- ( ( G e. Mgm /\ s e. ( Base ` G ) /\ t e. ( Base ` G ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )
12	11	3expib	|- ( G e. Mgm -> ( ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) ) )
13	5 12	syl	|- ( ph -> ( ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) ) )
14	13	imp	|- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )
15	1 2 3 4 14 6 7 8	gsumpropd2	|- ( ph -> ( G gsum F ) = ( H gsum F ) )