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 5 21 7 grpcld 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( ( invg ` G ) ` x ) .+ y ) e. B )
23 oveq2 
 |-  ( r = ( ( ( invg ` G ) ` x ) .+ y ) -> ( x .+ r ) = ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) )
24 23 eqeq1d 
 |-  ( r = ( ( ( invg ` G ) ` x ) .+ y ) -> ( ( x .+ r ) = y <-> ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) = y ) )
25 24 adantl 
 |-  ( ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) /\ r = ( ( ( invg ` G ) ` x ) .+ y ) ) -> ( ( x .+ r ) = y <-> ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) = y ) )
26 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
27 1 2 26 19 grprinv 
 |-  ( ( G e. Grp /\ x e. B ) -> ( x .+ ( ( invg ` G ) ` x ) ) = ( 0g ` G ) )
28 27 adantrr 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x .+ ( ( invg ` G ) ` x ) ) = ( 0g ` G ) )
29 28 oveq1d 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ ( ( invg ` G ) ` x ) ) .+ y ) = ( ( 0g ` G ) .+ y ) )
30 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 ) ) )
31 5 9 21 7 30 syl13anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ ( ( invg ` G ) ` x ) ) .+ y ) = ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) )
32 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
33 1 2 26 mndlid 
 |-  ( ( G e. Mnd /\ y e. B ) -> ( ( 0g ` G ) .+ y ) = y )
34 32 6 33 syl2an 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( 0g ` G ) .+ y ) = y )
35 29 31 34 3eqtr3d 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x .+ ( ( ( invg ` G ) ` x ) .+ y ) ) = y )
36 22 25 35 rspcedvd 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> E. r e. B ( x .+ r ) = y )
37 18 36 jca 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) )
38 37 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 ) )
39 3 4 38 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 ) ) )
40 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 )
41 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 ) )
42 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 ) ) )
43 40 41 42 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 )
44 39 43 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 ) ) )