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

Metamath Proof Explorer

Theorem grpidd

Description: Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grpidd.b 
|- ( ph -> B = ( Base ` G ) )
grpidd.p 
|- ( ph -> .+ = ( +g ` G ) )
grpidd.z 
|- ( ph -> .0. e. B )
grpidd.i 
|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
grpidd.j 
|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
Assertion grpidd 
|- ( ph -> .0. = ( 0g ` G ) )

Proof

Step Hyp Ref Expression
1 grpidd.b 
 |-  ( ph -> B = ( Base ` G ) )
2 grpidd.p 
 |-  ( ph -> .+ = ( +g ` G ) )
3 grpidd.z 
 |-  ( ph -> .0. e. B )
4 grpidd.i 
 |-  ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
5 grpidd.j 
 |-  ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 eqid 
 |-  ( +g ` G ) = ( +g ` G )
9 3 1 eleqtrd 
 |-  ( ph -> .0. e. ( Base ` G ) )
10 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` G ) ) )
11 10 biimpar 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> x e. B )
12 2 adantr 
 |-  ( ( ph /\ x e. B ) -> .+ = ( +g ` G ) )
13 12 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( .0. .+ x ) = ( .0. ( +g ` G ) x ) )
14 13 4 eqtr3d 
 |-  ( ( ph /\ x e. B ) -> ( .0. ( +g ` G ) x ) = x )
15 11 14 syldan 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> ( .0. ( +g ` G ) x ) = x )
16 12 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( x .+ .0. ) = ( x ( +g ` G ) .0. ) )
17 16 5 eqtr3d 
 |-  ( ( ph /\ x e. B ) -> ( x ( +g ` G ) .0. ) = x )
18 11 17 syldan 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> ( x ( +g ` G ) .0. ) = x )
19 6 7 8 9 15 18 ismgmid2 
 |-  ( ph -> .0. = ( 0g ` G ) )