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

Metamath Proof Explorer

Theorem grpinvex

Description: Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grpcl.b 
|- B = ( Base ` G )
grpcl.p 
|- .+ = ( +g ` G )
grpinvex.p 
|- .0. = ( 0g ` G )
Assertion grpinvex 
|- ( ( G e. Grp /\ X e. B ) -> E. y e. B ( y .+ X ) = .0. )

Proof

Step Hyp Ref Expression
1 grpcl.b 
 |-  B = ( Base ` G )
2 grpcl.p 
 |-  .+ = ( +g ` G )
3 grpinvex.p 
 |-  .0. = ( 0g ` G )
4 1 2 3 isgrp 
 |-  ( G e. Grp <-> ( G e. Mnd /\ A. x e. B E. y e. B ( y .+ x ) = .0. ) )
5 4 simprbi 
 |-  ( G e. Grp -> A. x e. B E. y e. B ( y .+ x ) = .0. )
6 oveq2 
 |-  ( x = X -> ( y .+ x ) = ( y .+ X ) )
7 6 eqeq1d 
 |-  ( x = X -> ( ( y .+ x ) = .0. <-> ( y .+ X ) = .0. ) )
8 7 rexbidv 
 |-  ( x = X -> ( E. y e. B ( y .+ x ) = .0. <-> E. y e. B ( y .+ X ) = .0. ) )
9 8 rspccva 
 |-  ( ( A. x e. B E. y e. B ( y .+ x ) = .0. /\ X e. B ) -> E. y e. B ( y .+ X ) = .0. )
10 5 9 sylan 
 |-  ( ( G e. Grp /\ X e. B ) -> E. y e. B ( y .+ X ) = .0. )