Metamath Proof Explorer

Theorem dfgrp2

Description: Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp , based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 dfgrp2.b 
 |-  B = ( Base ` G )
2 dfgrp2.p 
 |-  .+ = ( +g ` G )
3 grpsgrp 
 |-  ( G e. Grp -> G e. Smgrp )
4 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
5 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
6 1 5 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. B )
7 4 6 syl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
8 oveq1 
 |-  ( n = ( 0g ` G ) -> ( n .+ x ) = ( ( 0g ` G ) .+ x ) )
9 8 eqeq1d 
 |-  ( n = ( 0g ` G ) -> ( ( n .+ x ) = x <-> ( ( 0g ` G ) .+ x ) = x ) )
10 eqeq2 
 |-  ( n = ( 0g ` G ) -> ( ( i .+ x ) = n <-> ( i .+ x ) = ( 0g ` G ) ) )
11 10 rexbidv 
 |-  ( n = ( 0g ` G ) -> ( E. i e. B ( i .+ x ) = n <-> E. i e. B ( i .+ x ) = ( 0g ` G ) ) )
12 9 11 anbi12d 
 |-  ( n = ( 0g ` G ) -> ( ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) <-> ( ( ( 0g ` G ) .+ x ) = x /\ E. i e. B ( i .+ x ) = ( 0g ` G ) ) ) )
13 12 ralbidv 
 |-  ( n = ( 0g ` G ) -> ( A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) <-> A. x e. B ( ( ( 0g ` G ) .+ x ) = x /\ E. i e. B ( i .+ x ) = ( 0g ` G ) ) ) )
14 13 adantl 
 |-  ( ( G e. Grp /\ n = ( 0g ` G ) ) -> ( A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) <-> A. x e. B ( ( ( 0g ` G ) .+ x ) = x /\ E. i e. B ( i .+ x ) = ( 0g ` G ) ) ) )
15 1 2 5 mndlid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( ( 0g ` G ) .+ x ) = x )
16 4 15 sylan 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( 0g ` G ) .+ x ) = x )
17 1 2 5 grpinvex 
 |-  ( ( G e. Grp /\ x e. B ) -> E. i e. B ( i .+ x ) = ( 0g ` G ) )
18 16 17 jca 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( ( 0g ` G ) .+ x ) = x /\ E. i e. B ( i .+ x ) = ( 0g ` G ) ) )
19 18 ralrimiva 
 |-  ( G e. Grp -> A. x e. B ( ( ( 0g ` G ) .+ x ) = x /\ E. i e. B ( i .+ x ) = ( 0g ` G ) ) )
20 7 14 19 rspcedvd 
 |-  ( G e. Grp -> E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) )
21 3 20 jca 
 |-  ( G e. Grp -> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
22 1 a1i 
 |-  ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> B = ( Base ` G ) )
23 2 a1i 
 |-  ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> .+ = ( +g ` G ) )
24 sgrpmgm 
 |-  ( G e. Smgrp -> G e. Mgm )
25 24 adantl 
 |-  ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Mgm )
26 1 2 mgmcl 
 |-  ( ( G e. Mgm /\ a e. B /\ b e. B ) -> ( a .+ b ) e. B )
27 25 26 syl3an1 
 |-  ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B /\ b e. B ) -> ( a .+ b ) e. B )
28 1 2 sgrpass 
 |-  ( ( G e. Smgrp /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) )
29 28 adantll 
 |-  ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) )
30 simpll 
 |-  ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> n e. B )
31 oveq2 
 |-  ( x = a -> ( n .+ x ) = ( n .+ a ) )
32 id 
 |-  ( x = a -> x = a )
33 31 32 eqeq12d 
 |-  ( x = a -> ( ( n .+ x ) = x <-> ( n .+ a ) = a ) )
34 oveq2 
 |-  ( x = a -> ( i .+ x ) = ( i .+ a ) )
35 34 eqeq1d 
 |-  ( x = a -> ( ( i .+ x ) = n <-> ( i .+ a ) = n ) )
36 35 rexbidv 
 |-  ( x = a -> ( E. i e. B ( i .+ x ) = n <-> E. i e. B ( i .+ a ) = n ) )
37 33 36 anbi12d 
 |-  ( x = a -> ( ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) <-> ( ( n .+ a ) = a /\ E. i e. B ( i .+ a ) = n ) ) )
38 37 rspcv 
 |-  ( a e. B -> ( A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( ( n .+ a ) = a /\ E. i e. B ( i .+ a ) = n ) ) )
39 simpl 
 |-  ( ( ( n .+ a ) = a /\ E. i e. B ( i .+ a ) = n ) -> ( n .+ a ) = a )
40 38 39 syl6com 
 |-  ( A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( a e. B -> ( n .+ a ) = a ) )
41 40 ad2antlr 
 |-  ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> ( a e. B -> ( n .+ a ) = a ) )
42 41 imp 
 |-  ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B ) -> ( n .+ a ) = a )
43 oveq1 
 |-  ( i = b -> ( i .+ a ) = ( b .+ a ) )
44 43 eqeq1d 
 |-  ( i = b -> ( ( i .+ a ) = n <-> ( b .+ a ) = n ) )
45 44 cbvrexvw 
 |-  ( E. i e. B ( i .+ a ) = n <-> E. b e. B ( b .+ a ) = n )
46 45 biimpi 
 |-  ( E. i e. B ( i .+ a ) = n -> E. b e. B ( b .+ a ) = n )
47 46 adantl 
 |-  ( ( ( n .+ a ) = a /\ E. i e. B ( i .+ a ) = n ) -> E. b e. B ( b .+ a ) = n )
48 38 47 syl6com 
 |-  ( A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( a e. B -> E. b e. B ( b .+ a ) = n ) )
49 48 ad2antlr 
 |-  ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> ( a e. B -> E. b e. B ( b .+ a ) = n ) )
50 49 imp 
 |-  ( ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) /\ a e. B ) -> E. b e. B ( b .+ a ) = n )
51 22 23 27 29 30 42 50 isgrpde 
 |-  ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Grp )
52 51 ex 
 |-  ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) -> ( G e. Smgrp -> G e. Grp ) )
53 52 rexlimiva 
 |-  ( E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( G e. Smgrp -> G e. Grp ) )
54 53 impcom 
 |-  ( ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) -> G e. Grp )
55 21 54 impbii 
 |-  ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )