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

Metamath Proof Explorer

Theorem grpidd2

Description: Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd . (Contributed by Mario Carneiro, 14-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 grpidd2.b 
 |-  ( ph -> B = ( Base ` G ) )
2 grpidd2.p 
 |-  ( ph -> .+ = ( +g ` G ) )
3 grpidd2.z 
 |-  ( ph -> .0. e. B )
4 grpidd2.i 
 |-  ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
5 grpidd2.j 
 |-  ( ph -> G e. Grp )
6 2 oveqd 
 |-  ( ph -> ( .0. .+ .0. ) = ( .0. ( +g ` G ) .0. ) )
7 oveq2 
 |-  ( x = .0. -> ( .0. .+ x ) = ( .0. .+ .0. ) )
8 id 
 |-  ( x = .0. -> x = .0. )
9 7 8 eqeq12d 
 |-  ( x = .0. -> ( ( .0. .+ x ) = x <-> ( .0. .+ .0. ) = .0. ) )
10 4 ralrimiva 
 |-  ( ph -> A. x e. B ( .0. .+ x ) = x )
11 9 10 3 rspcdva 
 |-  ( ph -> ( .0. .+ .0. ) = .0. )
12 6 11 eqtr3d 
 |-  ( ph -> ( .0. ( +g ` G ) .0. ) = .0. )
13 3 1 eleqtrd 
 |-  ( ph -> .0. e. ( Base ` G ) )
14 eqid 
 |-  ( Base ` G ) = ( Base ` G )
15 eqid 
 |-  ( +g ` G ) = ( +g ` G )
16 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
17 14 15 16 grpid 
 |-  ( ( G e. Grp /\ .0. e. ( Base ` G ) ) -> ( ( .0. ( +g ` G ) .0. ) = .0. <-> ( 0g ` G ) = .0. ) )
18 5 13 17 syl2anc 
 |-  ( ph -> ( ( .0. ( +g ` G ) .0. ) = .0. <-> ( 0g ` G ) = .0. ) )
19 12 18 mpbid 
 |-  ( ph -> ( 0g ` G ) = .0. )
20 19 eqcomd 
 |-  ( ph -> .0. = ( 0g ` G ) )