Metamath Proof Explorer

Theorem archiabl

Description: Archimedean left- and right- ordered groups are Abelian. (Contributed by Thierry Arnoux, 1-May-2018)

Ref Expression
Assertion archiabl ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) → 𝑊 ∈ Abel )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
3 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
4 eqid ⊢ ( lt ‘ 𝑊 ) = ( lt ‘ 𝑊 )
5 eqid ⊢ ( .g ‘ 𝑊 ) = ( .g ‘ 𝑊 )
6 simpll1 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ oGrp )
7 simpll3 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Archi )
8 simplr ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
9 simprl ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 )
10 simp2 ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
11 simp1rr ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) )
12 simp3 ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 )
13 breq2 ⊢ ( 𝑥 = 𝑦 → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ↔ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) )
14 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑣 ( le ‘ 𝑊 ) 𝑥 ↔ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
15 13 14 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 → 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
16 15 rspcv ⊢ ( 𝑦 ∈ ( Base ‘ 𝑊 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 → 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
17 10 11 12 16 syl3c ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → 𝑣 ( le ‘ 𝑊 ) 𝑦 )
18 1 2 3 4 5 6 7 8 9 17 archiabllem1 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
19 18 adantllr ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
20 breq2 ⊢ ( 𝑢 = 𝑣 → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ↔ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) )
21 breq1 ⊢ ( 𝑢 = 𝑣 → ( 𝑢 ( le ‘ 𝑊 ) 𝑥 ↔ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) )
22 21 imbi2d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
23 22 ralbidv ⊢ ( 𝑢 = 𝑣 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
24 20 23 anbi12d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) )
25 24 cbvrexvw ⊢ ( ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
26 25 bilani ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
27 19 26 r19.29a ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
28 simpl1 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ oGrp )
29 simpl3 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Archi )
30 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
31 simpl2 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ( oppg ‘ 𝑊 ) ∈ oGrp )
32 ralnex ⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
33 32 bilanri ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
34 rexanali ⊢ ( ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) )
35 34 imbi2i ⊢ ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
36 imnan ⊢ ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
37 35 36 bitri ⊢ ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
38 37 ralbii ⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
39 33 38 sylibr ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
40 21 notbid ⊢ ( 𝑢 = 𝑣 → ( ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ↔ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) )
41 40 anbi2d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
42 41 rexbidv ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
43 20 42 imbi12d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) )
44 43 cbvralvw ⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
45 39 44 sylib ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
46 45 r19.21bi ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
47 14 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ↔ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
48 13 47 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
49 48 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
50 46 49 imbitrdi ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
51 50 3impia ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
52 simp1l1 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → 𝑊 ∈ oGrp )
53 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
54 53 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
55 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
56 52 54 55 3syl ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → 𝑊 ∈ Toset )
57 simp2 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
58 1 3 4 tltnle ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( lt ‘ 𝑊 ) 𝑣 ↔ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
59 58 bicomd ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
60 59 3com23 ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
61 60 3expa ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
62 61 anbi2d ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) ) )
63 62 rexbidva ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) ) )
64 56 57 63 syl2anc ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) ) )
65 51 64 mpbid ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
66 1 2 3 4 5 28 29 30 31 65 archiabllem2 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
67 27 66 pm2.61dan ⊢ ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) → 𝑊 ∈ Abel )