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 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ∈ 𝐵 )
23 5 21 7 22 syl3anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ∈ 𝐵 )
24 oveq2 ⊢ ( 𝑟 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) → ( 𝑥 + 𝑟 ) = ( 𝑥 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) )
25 24 eqeq1d ⊢ ( 𝑟 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) → ( ( 𝑥 + 𝑟 ) = 𝑦 ↔ ( 𝑥 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) = 𝑦 ) )
26 25 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑟 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) → ( ( 𝑥 + 𝑟 ) = 𝑦 ↔ ( 𝑥 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) = 𝑦 ) )
27 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
28 1 2 27 19 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝐺 ) )
29 28 adantrr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝐺 ) )
30 29 oveq1d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) + 𝑦 ) = ( ( 0g ‘ 𝐺 ) + 𝑦 ) )
31 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) + 𝑦 ) = ( 𝑥 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) )
32 5 9 21 7 31 syl13anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) + 𝑦 ) = ( 𝑥 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) )
33 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
34 1 2 27 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 )
35 33 6 34 syl2an ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 )
36 30 32 35 3eqtr3d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑦 ) ) = 𝑦 )
37 23 26 36 rspcedvd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 )
38 18 37 jca ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
39 38 ralrimivva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
40 3 4 39 3jca ⊢ ( 𝐺 ∈ Grp → ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )
41 simp1 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐺 ∈ Smgrp )
42 1 2 dfgrp3lem ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) )
43 1 2 dfgrp2 ⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑢 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑢 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑢 ) ) )
44 41 42 43 sylanbrc ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐺 ∈ Grp )
45 40 44 impbii ⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∃ 𝑙 ∈ 𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟 ∈ 𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )