Step |
Hyp |
Ref |
Expression |
1 |
|
archiabllem.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
2 |
|
archiabllem.0 |
⊢ 0 = ( 0g ‘ 𝑊 ) |
3 |
|
archiabllem.e |
⊢ ≤ = ( le ‘ 𝑊 ) |
4 |
|
archiabllem.t |
⊢ < = ( lt ‘ 𝑊 ) |
5 |
|
archiabllem.m |
⊢ · = ( .g ‘ 𝑊 ) |
6 |
|
archiabllem.g |
⊢ ( 𝜑 → 𝑊 ∈ oGrp ) |
7 |
|
archiabllem.a |
⊢ ( 𝜑 → 𝑊 ∈ Archi ) |
8 |
|
archiabllem2.1 |
⊢ + = ( +g ‘ 𝑊 ) |
9 |
|
archiabllem2.2 |
⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp ) |
10 |
|
archiabllem2.3 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ) |
11 |
|
ogrpgrp |
⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp ) |
12 |
6 11
|
syl |
⊢ ( 𝜑 → 𝑊 ∈ Grp ) |
13 |
6
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ oGrp ) |
14 |
7
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ Archi ) |
15 |
9
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( oppg ‘ 𝑊 ) ∈ oGrp ) |
16 |
|
simp1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) |
17 |
16 10
|
syl3an1 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) ) |
18 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) |
19 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 ) |
20 |
1 2 3 4 5 13 14 8 15 17 18 19
|
archiabllem2b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) |
21 |
20
|
3expb |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) |
22 |
21
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) |
23 |
1 8
|
isabl2 |
⊢ ( 𝑊 ∈ Abel ↔ ( 𝑊 ∈ Grp ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) ) |
24 |
12 22 23
|
sylanbrc |
⊢ ( 𝜑 → 𝑊 ∈ Abel ) |