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 e. oGrp /\ ( oppG ` W ) e. oGrp /\ W e. Archi ) -> W e. Abel )

Proof

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