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