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 ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ) |