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
Assertion dfgrp3 Could not format assertion : No typesetting found for |- ( 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 ) ) ) with typecode |-

Proof

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