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 𝐵 = ( Base ‘ 𝐺 )
dfgrp3.p + = ( +g𝐺 )
Assertion dfgrp3 ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dfgrp3.b 𝐵 = ( Base ‘ 𝐺 )
2 dfgrp3.p + = ( +g𝐺 )
3 grpsgrp ( 𝐺 ∈ Grp → 𝐺 ∈ Smgrp )
4 1 grpbn0 ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ )
5 simpl ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝐺 ∈ Grp )
6 simpr ( ( 𝑥𝐵𝑦𝐵 ) → 𝑦𝐵 )
7 6 adantl ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑦𝐵 )
8 simpl ( ( 𝑥𝐵𝑦𝐵 ) → 𝑥𝐵 )
9 8 adantl ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑥𝐵 )
10 eqid ( -g𝐺 ) = ( -g𝐺 )
11 1 10 grpsubcl ( ( 𝐺 ∈ Grp ∧ 𝑦𝐵𝑥𝐵 ) → ( 𝑦 ( -g𝐺 ) 𝑥 ) ∈ 𝐵 )
12 5 7 9 11 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑦 ( -g𝐺 ) 𝑥 ) ∈ 𝐵 )
13 oveq1 ( 𝑙 = ( 𝑦 ( -g𝐺 ) 𝑥 ) → ( 𝑙 + 𝑥 ) = ( ( 𝑦 ( -g𝐺 ) 𝑥 ) + 𝑥 ) )
14 13 eqeq1d ( 𝑙 = ( 𝑦 ( -g𝐺 ) 𝑥 ) → ( ( 𝑙 + 𝑥 ) = 𝑦 ↔ ( ( 𝑦 ( -g𝐺 ) 𝑥 ) + 𝑥 ) = 𝑦 ) )
15 14 adantl ( ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑙 = ( 𝑦 ( -g𝐺 ) 𝑥 ) ) → ( ( 𝑙 + 𝑥 ) = 𝑦 ↔ ( ( 𝑦 ( -g𝐺 ) 𝑥 ) + 𝑥 ) = 𝑦 ) )
16 1 2 10 grpnpcan ( ( 𝐺 ∈ Grp ∧ 𝑦𝐵𝑥𝐵 ) → ( ( 𝑦 ( -g𝐺 ) 𝑥 ) + 𝑥 ) = 𝑦 )
17 5 7 9 16 syl3anc ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑦 ( -g𝐺 ) 𝑥 ) + 𝑥 ) = 𝑦 )
18 12 15 17 rspcedvd ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 )
19 eqid ( invg𝐺 ) = ( invg𝐺 )
20 1 19 grpinvcl ( ( 𝐺 ∈ Grp ∧ 𝑥𝐵 ) → ( ( invg𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
21 20 adantrr ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( invg𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
22 1 2 5 21 7 grpcld ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ∈ 𝐵 )
23 oveq2 ( 𝑟 = ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) → ( 𝑥 + 𝑟 ) = ( 𝑥 + ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) )
24 23 eqeq1d ( 𝑟 = ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) → ( ( 𝑥 + 𝑟 ) = 𝑦 ↔ ( 𝑥 + ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) = 𝑦 ) )
25 24 adantl ( ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑟 = ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) → ( ( 𝑥 + 𝑟 ) = 𝑦 ↔ ( 𝑥 + ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) = 𝑦 ) )
26 eqid ( 0g𝐺 ) = ( 0g𝐺 )
27 1 2 26 19 grprinv ( ( 𝐺 ∈ Grp ∧ 𝑥𝐵 ) → ( 𝑥 + ( ( invg𝐺 ) ‘ 𝑥 ) ) = ( 0g𝐺 ) )
28 27 adantrr ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 + ( ( invg𝐺 ) ‘ 𝑥 ) ) = ( 0g𝐺 ) )
29 28 oveq1d ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑥 + ( ( invg𝐺 ) ‘ 𝑥 ) ) + 𝑦 ) = ( ( 0g𝐺 ) + 𝑦 ) )
30 1 2 grpass ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵 ∧ ( ( invg𝐺 ) ‘ 𝑥 ) ∈ 𝐵𝑦𝐵 ) ) → ( ( 𝑥 + ( ( invg𝐺 ) ‘ 𝑥 ) ) + 𝑦 ) = ( 𝑥 + ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) )
31 5 9 21 7 30 syl13anc ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑥 + ( ( invg𝐺 ) ‘ 𝑥 ) ) + 𝑦 ) = ( 𝑥 + ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) )
32 grpmnd ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
33 1 2 26 mndlid ( ( 𝐺 ∈ Mnd ∧ 𝑦𝐵 ) → ( ( 0g𝐺 ) + 𝑦 ) = 𝑦 )
34 32 6 33 syl2an ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 0g𝐺 ) + 𝑦 ) = 𝑦 )
35 29 31 34 3eqtr3d ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 + ( ( ( invg𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) = 𝑦 )
36 22 25 35 rspcedvd ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 )
37 18 36 jca ( ( 𝐺 ∈ Grp ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
38 37 ralrimivva ( 𝐺 ∈ Grp → ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
39 3 4 38 3jca ( 𝐺 ∈ Grp → ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )
40 simp1 ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐺 ∈ Smgrp )
41 1 2 dfgrp3lem ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑢𝐵𝑎𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )
42 1 2 dfgrp2 ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑢𝐵𝑎𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
43 40 41 42 sylanbrc ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐺 ∈ Grp )
44 39 43 impbii ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )