This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 simpr 
 |-  ( ( ( 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. u e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) u /\ A. x e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> u ( le ` W ) x ) ) )
21 breq2 
 |-  ( u = v -> ( ( 0g ` W ) ( lt ` W ) u <-> ( 0g ` W ) ( lt ` W ) v ) )
22 breq1 
 |-  ( u = v -> ( u ( le ` W ) x <-> v ( le ` W ) x ) )
23 22 imbi2d 
 |-  ( u = v -> ( ( ( 0g ` W ) ( lt ` W ) x -> u ( le ` W ) x ) <-> ( ( 0g ` W ) ( lt ` W ) x -> v ( le ` W ) x ) ) )
24 23 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 ) ) )
25 21 24 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 ) ) ) )
26 25 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 ) ) )
27 20 26 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 ) ) ) -> E. v e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) v /\ A. x e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> v ( le ` W ) x ) ) )
28 19 27 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 )
29 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 )
30 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 )
31 eqid 
 |-  ( +g ` W ) = ( +g ` W )
32 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 )
33 simpr 
 |-  ( ( ( 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. u e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) u /\ A. x e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> u ( le ` W ) x ) ) )
34 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 ) ) )
35 33 34 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 /\ A. x e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> u ( le ` W ) x ) ) )
36 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 ) )
37 36 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 ) ) )
38 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 ) ) )
39 37 38 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 ) ) )
40 39 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 ) ) )
41 35 40 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 ) ) )
42 22 notbid 
 |-  ( u = v -> ( -. u ( le ` W ) x <-> -. v ( le ` W ) x ) )
43 42 anbi2d 
 |-  ( u = v -> ( ( ( 0g ` W ) ( lt ` W ) x /\ -. u ( le ` W ) x ) <-> ( ( 0g ` W ) ( lt ` W ) x /\ -. v ( le ` W ) x ) ) )
44 43 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 ) ) )
45 21 44 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 ) ) ) )
46 45 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 ) ) )
47 41 46 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 ) ) )
48 47 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 ) ) )
49 14 notbid 
 |-  ( x = y -> ( -. v ( le ` W ) x <-> -. v ( le ` W ) y ) )
50 13 49 anbi12d 
 |-  ( x = y -> ( ( ( 0g ` W ) ( lt ` W ) x /\ -. v ( le ` W ) x ) <-> ( ( 0g ` W ) ( lt ` W ) y /\ -. v ( le ` W ) y ) ) )
51 50 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 ) )
52 48 51 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 ) ) )
53 52 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 ) )
54 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 )
55 isogrp 
 |-  ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
56 55 simprbi 
 |-  ( W e. oGrp -> W e. oMnd )
57 omndtos 
 |-  ( W e. oMnd -> W e. Toset )
58 54 56 57 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 )
59 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 ) )
60 1 3 4 tltnle 
 |-  ( ( W e. Toset /\ y e. ( Base ` W ) /\ v e. ( Base ` W ) ) -> ( y ( lt ` W ) v <-> -. v ( le ` W ) y ) )
61 60 bicomd 
 |-  ( ( W e. Toset /\ y e. ( Base ` W ) /\ v e. ( Base ` W ) ) -> ( -. v ( le ` W ) y <-> y ( lt ` W ) v ) )
62 61 3com23 
 |-  ( ( W e. Toset /\ v e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( -. v ( le ` W ) y <-> y ( lt ` W ) v ) )
63 62 3expa 
 |-  ( ( ( W e. Toset /\ v e. ( Base ` W ) ) /\ y e. ( Base ` W ) ) -> ( -. v ( le ` W ) y <-> y ( lt ` W ) v ) )
64 63 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 ) ) )
65 64 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 ) ) )
66 58 59 65 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 ) ) )
67 53 66 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 ) )
68 1 2 3 4 5 29 30 31 32 67 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 )
69 28 68 pm2.61dan 
 |-  ( ( W e. oGrp /\ ( oppG ` W ) e. oGrp /\ W e. Archi ) -> W e. Abel )