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 ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )