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