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

Metamath Proof Explorer

Theorem grplrinv

Description: In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021)

Ref Expression
Hypotheses grplrinv.b 
|- B = ( Base ` G )
grplrinv.p 
|- .+ = ( +g ` G )
grplrinv.i 
|- .0. = ( 0g ` G )
Assertion grplrinv 
|- ( G e. Grp -> A. x e. B E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )

Proof

Step Hyp Ref Expression
1 grplrinv.b 
 |-  B = ( Base ` G )
2 grplrinv.p 
 |-  .+ = ( +g ` G )
3 grplrinv.i 
 |-  .0. = ( 0g ` G )
4 eqid 
 |-  ( invg ` G ) = ( invg ` G )
5 1 4 grpinvcl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
6 oveq1 
 |-  ( y = ( ( invg ` G ) ` x ) -> ( y .+ x ) = ( ( ( invg ` G ) ` x ) .+ x ) )
7 6 eqeq1d 
 |-  ( y = ( ( invg ` G ) ` x ) -> ( ( y .+ x ) = .0. <-> ( ( ( invg ` G ) ` x ) .+ x ) = .0. ) )
8 oveq2 
 |-  ( y = ( ( invg ` G ) ` x ) -> ( x .+ y ) = ( x .+ ( ( invg ` G ) ` x ) ) )
9 8 eqeq1d 
 |-  ( y = ( ( invg ` G ) ` x ) -> ( ( x .+ y ) = .0. <-> ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) )
10 7 9 anbi12d 
 |-  ( y = ( ( invg ` G ) ` x ) -> ( ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) <-> ( ( ( ( invg ` G ) ` x ) .+ x ) = .0. /\ ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) ) )
11 10 adantl 
 |-  ( ( ( G e. Grp /\ x e. B ) /\ y = ( ( invg ` G ) ` x ) ) -> ( ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) <-> ( ( ( ( invg ` G ) ` x ) .+ x ) = .0. /\ ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) ) )
12 1 2 3 4 grplinv 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( ( invg ` G ) ` x ) .+ x ) = .0. )
13 1 2 3 4 grprinv 
 |-  ( ( G e. Grp /\ x e. B ) -> ( x .+ ( ( invg ` G ) ` x ) ) = .0. )
14 12 13 jca 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( ( ( invg ` G ) ` x ) .+ x ) = .0. /\ ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) )
15 5 11 14 rspcedvd 
 |-  ( ( G e. Grp /\ x e. B ) -> E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )
16 15 ralrimiva 
 |-  ( G e. Grp -> A. x e. B E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )