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
Assertion dfgrp2 G Grp G Smgrp n B x B n + ˙ x = x i B i + ˙ x = n

Proof

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