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 ⊢W∈oGrp∧opp𝑔⁡W∈oGrp∧W∈Archi→W∈Abel

Proof

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