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

Metamath Proof Explorer

Theorem grplinv

Description: The left inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grpinv.b 
|- B = ( Base ` G )
grpinv.p 
|- .+ = ( +g ` G )
grpinv.u 
|- .0. = ( 0g ` G )
grpinv.n 
|- N = ( invg ` G )
Assertion grplinv 
|- ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )

Proof

Step Hyp Ref Expression
1 grpinv.b 
 |-  B = ( Base ` G )
2 grpinv.p 
 |-  .+ = ( +g ` G )
3 grpinv.u 
 |-  .0. = ( 0g ` G )
4 grpinv.n 
 |-  N = ( invg ` G )
5 1 2 3 4 grpinvval 
 |-  ( X e. B -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )
6 5 adantl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )
7 1 2 3 grpinveu 
 |-  ( ( G e. Grp /\ X e. B ) -> E! y e. B ( y .+ X ) = .0. )
8 riotacl2 
 |-  ( E! y e. B ( y .+ X ) = .0. -> ( iota_ y e. B ( y .+ X ) = .0. ) e. { y e. B | ( y .+ X ) = .0. } )
9 7 8 syl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( iota_ y e. B ( y .+ X ) = .0. ) e. { y e. B | ( y .+ X ) = .0. } )
10 6 9 eqeltrd 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. { y e. B | ( y .+ X ) = .0. } )
11 oveq1 
 |-  ( y = ( N ` X ) -> ( y .+ X ) = ( ( N ` X ) .+ X ) )
12 11 eqeq1d 
 |-  ( y = ( N ` X ) -> ( ( y .+ X ) = .0. <-> ( ( N ` X ) .+ X ) = .0. ) )
13 12 elrab 
 |-  ( ( N ` X ) e. { y e. B | ( y .+ X ) = .0. } <-> ( ( N ` X ) e. B /\ ( ( N ` X ) .+ X ) = .0. ) )
14 13 simprbi 
 |-  ( ( N ` X ) e. { y e. B | ( y .+ X ) = .0. } -> ( ( N ` X ) .+ X ) = .0. )
15 10 14 syl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )