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

Metamath Proof Explorer

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