Metamath Proof Explorer

Theorem grpidinv

Description: A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006) (Revised by AV, 1-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 grpidinv.b 
 |-  B = ( Base ` G )
2 grpidinv.p 
 |-  .+ = ( +g ` G )
3 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
4 1 3 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
5 oveq1 
 |-  ( u = ( 0g ` G ) -> ( u .+ x ) = ( ( 0g ` G ) .+ x ) )
6 5 eqeq1d 
 |-  ( u = ( 0g ` G ) -> ( ( u .+ x ) = x <-> ( ( 0g ` G ) .+ x ) = x ) )
7 oveq2 
 |-  ( u = ( 0g ` G ) -> ( x .+ u ) = ( x .+ ( 0g ` G ) ) )
8 7 eqeq1d 
 |-  ( u = ( 0g ` G ) -> ( ( x .+ u ) = x <-> ( x .+ ( 0g ` G ) ) = x ) )
9 6 8 anbi12d 
 |-  ( u = ( 0g ` G ) -> ( ( ( u .+ x ) = x /\ ( x .+ u ) = x ) <-> ( ( ( 0g ` G ) .+ x ) = x /\ ( x .+ ( 0g ` G ) ) = x ) ) )
10 eqeq2 
 |-  ( u = ( 0g ` G ) -> ( ( y .+ x ) = u <-> ( y .+ x ) = ( 0g ` G ) ) )
11 eqeq2 
 |-  ( u = ( 0g ` G ) -> ( ( x .+ y ) = u <-> ( x .+ y ) = ( 0g ` G ) ) )
12 10 11 anbi12d 
 |-  ( u = ( 0g ` G ) -> ( ( ( y .+ x ) = u /\ ( x .+ y ) = u ) <-> ( ( y .+ x ) = ( 0g ` G ) /\ ( x .+ y ) = ( 0g ` G ) ) ) )
13 12 rexbidv 
 |-  ( u = ( 0g ` G ) -> ( E. y e. B ( ( y .+ x ) = u /\ ( x .+ y ) = u ) <-> E. y e. B ( ( y .+ x ) = ( 0g ` G ) /\ ( x .+ y ) = ( 0g ` G ) ) ) )
14 9 13 anbi12d 
 |-  ( u = ( 0g ` G ) -> ( ( ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E. y e. B ( ( y .+ x ) = u /\ ( x .+ y ) = u ) ) <-> ( ( ( ( 0g ` G ) .+ x ) = x /\ ( x .+ ( 0g ` G ) ) = x ) /\ E. y e. B ( ( y .+ x ) = ( 0g ` G ) /\ ( x .+ y ) = ( 0g ` G ) ) ) ) )
15 14 ralbidv 
 |-  ( u = ( 0g ` G ) -> ( A. x e. B ( ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E. y e. B ( ( y .+ x ) = u /\ ( x .+ y ) = u ) ) <-> A. x e. B ( ( ( ( 0g ` G ) .+ x ) = x /\ ( x .+ ( 0g ` G ) ) = x ) /\ E. y e. B ( ( y .+ x ) = ( 0g ` G ) /\ ( x .+ y ) = ( 0g ` G ) ) ) ) )
16 15 adantl 
 |-  ( ( G e. Grp /\ u = ( 0g ` G ) ) -> ( A. x e. B ( ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E. y e. B ( ( y .+ x ) = u /\ ( x .+ y ) = u ) ) <-> A. x e. B ( ( ( ( 0g ` G ) .+ x ) = x /\ ( x .+ ( 0g ` G ) ) = x ) /\ E. y e. B ( ( y .+ x ) = ( 0g ` G ) /\ ( x .+ y ) = ( 0g ` G ) ) ) ) )
17 1 2 3 grpidinv2 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( ( ( 0g ` G ) .+ x ) = x /\ ( x .+ ( 0g ` G ) ) = x ) /\ E. y e. B ( ( y .+ x ) = ( 0g ` G ) /\ ( x .+ y ) = ( 0g ` G ) ) ) )
18 17 ralrimiva 
 |-  ( G e. Grp -> A. x e. B ( ( ( ( 0g ` G ) .+ x ) = x /\ ( x .+ ( 0g ` G ) ) = x ) /\ E. y e. B ( ( y .+ x ) = ( 0g ` G ) /\ ( x .+ y ) = ( 0g ` G ) ) ) )
19 4 16 18 rspcedvd 
 |-  ( G e. Grp -> E. u e. B A. x e. B ( ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E. y e. B ( ( y .+ x ) = u /\ ( x .+ y ) = u ) ) )