# 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}={\mathrm{Base}}_{{G}}$
dfgrp2.p
Assertion dfgrp2 Could not format assertion : No typesetting found for |- ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) ) with typecode |-

### Proof

Step Hyp Ref Expression
1 dfgrp2.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 dfgrp2.p
3 grpsgrp Could not format ( G e. Grp -> G e. Smgrp ) : No typesetting found for |- ( G e. Grp -> G e. Smgrp ) with typecode |-
4 grpmnd ${⊢}{G}\in \mathrm{Grp}\to {G}\in \mathrm{Mnd}$
5 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
6 1 5 mndidcl ${⊢}{G}\in \mathrm{Mnd}\to {0}_{{G}}\in {B}$
7 4 6 syl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {B}$
8 oveq1
9 8 eqeq1d
10 eqeq2
11 10 rexbidv
12 9 11 anbi12d
13 12 ralbidv
15 1 2 5 mndlid
16 4 15 sylan
17 1 2 5 grpinvex
18 16 17 jca
19 18 ralrimiva
20 7 14 19 rspcedvd
21 3 20 jca Could not format ( G e. Grp -> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) ) : No typesetting found for |- ( G e. Grp -> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) ) with typecode |-
22 1 a1i Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> B = ( Base  G ) ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> B = ( Base  G ) ) with typecode |-
23 2 a1i Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> .+ = ( +g  G ) ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> .+ = ( +g  G ) ) with typecode |-
24 sgrpmgm Could not format ( G e. Smgrp -> G e. Mgm ) : No typesetting found for |- ( G e. Smgrp -> G e. Mgm ) with typecode |-
25 24 adantl Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Mgm ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> G e. Mgm ) with typecode |-
26 1 2 mgmcl
27 25 26 syl3an1 Could not format ( ( ( ( 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 ) : No typesetting found for |- ( ( ( ( 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 ) with typecode |-
28 1 2 sgrpass Could not format ( ( G e. Smgrp /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) with typecode |-
29 28 adantll Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-
30 simpll Could not format ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> n e. B ) : No typesetting found for |- ( ( ( n e. B /\ A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) /\ G e. Smgrp ) -> n e. B ) with typecode |-
31 oveq2
32 id ${⊢}{x}={a}\to {x}={a}$
33 31 32 eqeq12d
34 oveq2
35 34 eqeq1d
36 35 rexbidv
37 33 36 anbi12d
38 37 rspcv
39 simpl
40 38 39 syl6com
41 40 ad2antlr Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
42 41 imp Could not format ( ( ( ( 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 ) : No typesetting found for |- ( ( ( ( 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 ) with typecode |-
43 oveq1
44 43 eqeq1d
45 44 cbvrexvw
46 45 biimpi