Metamath Proof Explorer


Theorem dfgrp3e

Description: Alternate definition of a group as a set with a closed, associative operation, for which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Exercise 1 of Herstein p. 57. (Contributed by NM, 5-Dec-2006) (Revised by AV, 28-Aug-2021)

Ref Expression
Hypotheses dfgrp3.b 𝐵 = ( Base ‘ 𝐺 )
dfgrp3.p + = ( +g𝐺 )
Assertion dfgrp3e ( 𝐺 ∈ Grp ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgrp3.b 𝐵 = ( Base ‘ 𝐺 )
2 dfgrp3.p + = ( +g𝐺 )
3 1 2 dfgrp3 ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )
4 simp2 ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐵 ≠ ∅ )
5 sgrpmgm ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm )
6 5 adantr ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) → 𝐺 ∈ Mgm )
7 6 adantr ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → 𝐺 ∈ Mgm )
8 simpr ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) → 𝑥𝐵 )
9 8 adantr ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → 𝑥𝐵 )
10 simpr ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → 𝑦𝐵 )
11 1 2 mgmcl ( ( 𝐺 ∈ Mgm ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
12 7 9 10 11 syl3anc ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
13 12 adantr ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
14 1 2 sgrpass ( ( 𝐺 ∈ Smgrp ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
15 14 3anassrs ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) ∧ 𝑧𝐵 ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
16 15 ralrimiva ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
17 16 adantr ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
18 simpr ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
19 13 17 18 3jca ( ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )
20 19 ex ( ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) )
21 20 ralimdva ( ( 𝐺 ∈ Smgrp ∧ 𝑥𝐵 ) → ( ∀ 𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∀ 𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) )
22 21 ralimdva ( 𝐺 ∈ Smgrp → ( ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) )
23 22 a1d ( 𝐺 ∈ Smgrp → ( 𝐵 ≠ ∅ → ( ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) → ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) ) )
24 23 3imp ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )
25 4 24 jca ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) )
26 n0 ( 𝐵 ≠ ∅ ↔ ∃ 𝑎 𝑎𝐵 )
27 3simpa ( ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
28 27 2ralimi ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
29 1 2 issgrpn0 ( 𝑎𝐵 → ( 𝐺 ∈ Smgrp ↔ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ) )
30 28 29 syl5ibr ( 𝑎𝐵 → ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐺 ∈ Smgrp ) )
31 30 exlimiv ( ∃ 𝑎 𝑎𝐵 → ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐺 ∈ Smgrp ) )
32 26 31 sylbi ( 𝐵 ≠ ∅ → ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → 𝐺 ∈ Smgrp ) )
33 32 imp ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) → 𝐺 ∈ Smgrp )
34 simpl ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) → 𝐵 ≠ ∅ )
35 simp3 ( ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
36 35 2ralimi ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) → ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
37 36 adantl ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) → ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) )
38 33 34 37 3jca ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) → ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) )
39 25 38 impbii ( ( 𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) )
40 3 39 bitri ( 𝐺 ∈ Grp ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ∧ ( ∃ 𝑙𝐵 ( 𝑙 + 𝑥 ) = 𝑦 ∧ ∃ 𝑟𝐵 ( 𝑥 + 𝑟 ) = 𝑦 ) ) ) )