Metamath Proof Explorer


Theorem dfgrp2e

Description: Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in Lang p. 7. (Contributed by NM, 10-Oct-2006) (Revised by AV, 28-Aug-2021)

Ref Expression
Hypotheses dfgrp2.b 𝐵 = ( Base ‘ 𝐺 )
dfgrp2.p + = ( +g𝐺 )
Assertion dfgrp2e ( 𝐺 ∈ Grp ↔ ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛𝐵𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 dfgrp2.b 𝐵 = ( Base ‘ 𝐺 )
2 dfgrp2.p + = ( +g𝐺 )
3 1 2 dfgrp2 ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑛𝐵𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )
4 ax-1 ( 𝐺 ∈ V → ( 𝑛𝐵𝐺 ∈ V ) )
5 fvprc ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
6 1 eleq2i ( 𝑛𝐵𝑛 ∈ ( Base ‘ 𝐺 ) )
7 eleq2 ( ( Base ‘ 𝐺 ) = ∅ → ( 𝑛 ∈ ( Base ‘ 𝐺 ) ↔ 𝑛 ∈ ∅ ) )
8 noel ¬ 𝑛 ∈ ∅
9 8 pm2.21i ( 𝑛 ∈ ∅ → 𝐺 ∈ V )
10 7 9 syl6bi ( ( Base ‘ 𝐺 ) = ∅ → ( 𝑛 ∈ ( Base ‘ 𝐺 ) → 𝐺 ∈ V ) )
11 6 10 syl5bi ( ( Base ‘ 𝐺 ) = ∅ → ( 𝑛𝐵𝐺 ∈ V ) )
12 5 11 syl ( ¬ 𝐺 ∈ V → ( 𝑛𝐵𝐺 ∈ V ) )
13 4 12 pm2.61i ( 𝑛𝐵𝐺 ∈ V )
14 13 a1d ( 𝑛𝐵 → ( ∀ 𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → 𝐺 ∈ V ) )
15 14 rexlimiv ( ∃ 𝑛𝐵𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → 𝐺 ∈ V )
16 1 2 issgrpv ( 𝐺 ∈ V → ( 𝐺 ∈ Smgrp ↔ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ) )
17 15 16 syl ( ∃ 𝑛𝐵𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → ( 𝐺 ∈ Smgrp ↔ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ) )
18 17 pm5.32ri ( ( 𝐺 ∈ Smgrp ∧ ∃ 𝑛𝐵𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ↔ ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛𝐵𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )
19 3 18 bitri ( 𝐺 ∈ Grp ↔ ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛𝐵𝑥𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )