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

Metamath Proof Explorer

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