Metamath Proof Explorer

Theorem dfgrp3

Description: Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Theorem 3.2 of Bruck p. 28. (Contributed by AV, 28-Aug-2021)

Ref Expression
Hypotheses dfgrp3.b 
|- B = ( Base ` G )
dfgrp3.p 
|- .+ = ( +g ` G )
Assertion dfgrp3 
|- ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )

Proof

Step Hyp Ref Expression
1 dfgrp3.b 
 |-  B = ( Base ` G )
2 dfgrp3.p 
 |-  .+ = ( +g ` G )
3 grpsgrp 
 |-  ( G e. Grp -> G e. Smgrp )
4 1 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
5 simpl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> G e. Grp )
6 simpr 
 |-  ( ( x e. B /\ y e. B ) -> y e. B )
7 6 adantl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> y e. B )
8 simpl 
 |-  ( ( x e. B /\ y e. B ) -> x e. B )
9 8 adantl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> x e. B )
10 eqid 
 |-  ( -g ` G ) = ( -g ` G )
11 1 10 grpsubcl 
 |-  ( ( G e. Grp /\ y e. B /\ x e. B ) -> ( y ( -g ` G ) x ) e. B )
12 5 7 9 11 syl3anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( y ( -g ` G ) x ) e. B )
13 oveq1 
 |-  ( l = ( y ( -g ` G ) x ) -> ( l .+ x ) = ( ( y ( -g ` G ) x ) .+ x ) )
14 13 eqeq1d 
 |-  ( l = ( y ( -g ` G ) x ) -> ( ( l .+ x ) = y <-> ( ( y ( -g ` G ) x ) .+ x ) = y ) )
15 14 adantl 
 |-  ( ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) /\ l = ( y ( -g ` G ) x ) ) -> ( ( l .+ x ) = y <-> ( ( y ( -g ` G ) x ) .+ x ) = y ) )
16 1 2 10 grpnpcan 
 |-  ( ( G e. Grp /\ y e. B /\ x e. B ) -> ( ( y ( -g ` G ) x ) .+ x ) = y )
17 5 7 9 16 syl3anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( y ( -g ` G ) x ) .+ x ) = y )
18 12 15 17 rspcedvd 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> E. l e. B ( l .+ x ) = y )
19 eqid 
 |-  ( invg ` G ) = ( invg ` G )
20 1 19 grpinvcl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
21 20 adantrr 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( invg ` G ) ` x ) e. B )
22 1 2 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` x ) e. B /\ y e. B ) -> ( ( ( invg ` G ) ` x ) .+ y ) e. B )
23 5 21 7 22 syl3anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( ( invg ` G ) ` x ) .+ y ) e. B )
24 oveq2 
 |-  ( r = ( ( ( invg ` G ) ` x ) .+ y ) -> ( x .+ r ) = ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) )
25 24 eqeq1d 
 |-  ( r = ( ( ( invg ` G ) ` x ) .+ y ) -> ( ( x .+ r ) = y <-> ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) = y ) )
26 25 adantl 
 |-  ( ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) /\ r = ( ( ( invg ` G ) ` x ) .+ y ) ) -> ( ( x .+ r ) = y <-> ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) = y ) )
27 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
28 1 2 27 19 grprinv 
 |-  ( ( G e. Grp /\ x e. B ) -> ( x .+ ( ( invg ` G ) ` x ) ) = ( 0g ` G ) )
29 28 adantrr 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x .+ ( ( invg ` G ) ` x ) ) = ( 0g ` G ) )
30 29 oveq1d 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ ( ( invg ` G ) ` x ) ) .+ y ) = ( ( 0g ` G ) .+ y ) )
31 1 2 grpass 
 |-  ( ( G e. Grp /\ ( x e. B /\ ( ( invg ` G ) ` x ) e. B /\ y e. B ) ) -> ( ( x .+ ( ( invg ` G ) ` x ) ) .+ y ) = ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) )
32 5 9 21 7 31 syl13anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ ( ( invg ` G ) ` x ) ) .+ y ) = ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) )
33 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
34 1 2 27 mndlid 
 |-  ( ( G e. Mnd /\ y e. B ) -> ( ( 0g ` G ) .+ y ) = y )
35 33 6 34 syl2an 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( 0g ` G ) .+ y ) = y )
36 30 32 35 3eqtr3d 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) = y )
37 23 26 36 rspcedvd 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> E. r e. B ( x .+ r ) = y )
38 18 37 jca 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) )
39 38 ralrimivva 
 |-  ( G e. Grp -> A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) )
40 3 4 39 3jca 
 |-  ( G e. Grp -> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )
41 simp1 
 |-  ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp )
42 1 2 dfgrp3lem 
 |-  ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) )
43 1 2 dfgrp2 
 |-  ( G e. Grp <-> ( G e. Smgrp /\ E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) )
44 41 42 43 sylanbrc 
 |-  ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Grp )
45 40 44 impbii 
 |-  ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )