Theorem archiabl 28528

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

Assertion

Ref	Expression
archiabl	|- ( ( W e. oGrp /\ (oppg ` W ) e. oGrp /\ W e. Archi ) -> W e. Abel )

Proof of Theorem archiabl

Dummy variables v u x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2423	. . . . 5 |- ( Base ` W ) = ( Base ` W )
2		eqid 2423	. . . . 5 |- ( 0g ` W ) = ( 0g ` W )
3		eqid 2423	. . . . 5 |- ( le ` W ) = ( le ` W )
4		eqid 2423	. . . . 5 |- ( lt ` W ) = ( lt ` W )
5		eqid 2423	. . . . 5 |- (.g ` W ) = (.g ` W )
6		simpll1 1045	. . . . 5 |- ( ( ( ( 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 1047	. . . . 5 |- ( ( ( ( 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 761	. . . . 5 |- ( ( ( ( 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 763	. . . . 5 |- ( ( ( ( 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 1007	. . . . . 6 |- ( ( ( ( ( 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 1072	. . . . . 6 |- ( ( ( ( ( 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 1008	. . . . . 6 |- ( ( ( ( ( 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 4433	. . . . . . . 8 |- ( x = y -> ( ( 0g ` W ) ( lt ` W ) x <-> ( 0g ` W ) ( lt ` W ) y ) )
14		breq2 4433	. . . . . . . 8 |- ( x = y -> ( v ( le ` W ) x <-> v ( le ` W ) y ) )
15	13, 14	imbi12d 322	. . . . . . 7 |- ( x = y -> ( ( ( 0g ` W ) ( lt ` W ) x -> v ( le ` W ) x ) <-> ( ( 0g ` W ) ( lt ` W ) y -> v ( le ` W ) y ) ) )
16	15	rspcv 3184	. . . . . 6 |- ( 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 64	. . . . 5 |- ( ( ( ( ( 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 28523	. . . 4 |- ( ( ( ( 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 724	. . 3 |- ( ( ( ( ( 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 463	. . . 4 |- ( ( ( 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 4433	. . . . . 6 |- ( u = v -> ( ( 0g ` W ) ( lt ` W ) u <-> ( 0g ` W ) ( lt ` W ) v ) )
22		breq1 4432	. . . . . . . 8 |- ( u = v -> ( u ( le ` W ) x <-> v ( le ` W ) x ) )
23	22	imbi2d 318	. . . . . . 7 |- ( u = v -> ( ( ( 0g ` W ) ( lt ` W ) x -> u ( le ` W ) x ) <-> ( ( 0g ` W ) ( lt ` W ) x -> v ( le ` W ) x ) ) )
24	23	ralbidv 2866	. . . . . 6 |- ( 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 716	. . . . 5 |- ( 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	cbvrexv 3060	. . . 4 |- ( 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 200	. . 3 |- ( ( ( 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 2972	. 2 |- ( ( ( 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 1009	. . 3 |- ( ( ( 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 1011	. . 3 |- ( ( ( 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 2423	. . 3 |- ( +g ` W ) = ( +g ` W )
32		simpl2 1010	. . 3 |- ( ( ( 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 463	. . . . . . . . . 10 |- ( ( ( 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 2873	. . . . . . . . . 10 |- ( 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 216	. . . . . . . . 9 |- ( ( ( 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 2880	. . . . . . . . . . . 12 |- ( 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 314	. . . . . . . . . . 11 |- ( ( ( 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 424	. . . . . . . . . . 11 |- ( ( ( 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 253	. . . . . . . . . 10 |- ( ( ( 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 2858	. . . . . . . . 9 |- ( 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 216	. . . . . . . 8 |- ( ( ( 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 296	. . . . . . . . . . . 12 |- ( u = v -> ( -. u ( le ` W ) x <-> -. v ( le ` W ) x ) )
43	42	anbi2d 709	. . . . . . . . . . 11 |- ( u = v -> ( ( ( 0g ` W ) ( lt ` W ) x /\ -. u ( le ` W ) x ) <-> ( ( 0g ` W ) ( lt ` W ) x /\ -. v ( le ` W ) x ) ) )
44	43	rexbidv 2941	. . . . . . . . . 10 |- ( 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 322	. . . . . . . . 9 |- ( 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	cbvralv 3059	. . . . . . . 8 |- ( 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 200	. . . . . . 7 |- ( ( ( 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 2796	. . . . . 6 |- ( ( ( ( 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 296	. . . . . . . 8 |- ( x = y -> ( -. v ( le ` W ) x <-> -. v ( le ` W ) y ) )
50	13, 49	anbi12d 716	. . . . . . 7 |- ( x = y -> ( ( ( 0g ` W ) ( lt ` W ) x /\ -. v ( le ` W ) x ) <-> ( ( 0g ` W ) ( lt ` W ) y /\ -. v ( le ` W ) y ) ) )
51	50	cbvrexv 3060	. . . . . 6 |- ( 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	syl6ib 230	. . . . 5 |- ( ( ( ( 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 1203	. . . 4 |- ( ( ( ( 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 1099	. . . . . 6 |- ( ( ( ( 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 28478	. . . . . . 7 |- ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
56	55	simprbi 466	. . . . . 6 |- ( W e. oGrp -> W e. oMnd )
57		omndtos 28481	. . . . . 6 |- ( W e. oMnd -> W e. Toset )
58	54, 56, 57	3syl 18	. . . . 5 |- ( ( ( ( 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 1007	. . . . 5 |- ( ( ( ( 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 28436	. . . . . . . . . 10 |- ( ( W e. Toset /\ y e. ( Base ` W ) /\ v e. ( Base ` W ) ) -> ( y ( lt ` W ) v <-> -. v ( le ` W ) y ) )
61	60	bicomd 205	. . . . . . . . 9 |- ( ( W e. Toset /\ y e. ( Base ` W ) /\ v e. ( Base ` W ) ) -> ( -. v ( le ` W ) y <-> y ( lt ` W ) v ) )
62	61	3com23 1212	. . . . . . . 8 |- ( ( W e. Toset /\ v e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( -. v ( le ` W ) y <-> y ( lt ` W ) v ) )
63	62	3expa 1206	. . . . . . 7 |- ( ( ( W e. Toset /\ v e. ( Base ` W ) ) /\ y e. ( Base ` W ) ) -> ( -. v ( le ` W ) y <-> y ( lt ` W ) v ) )
64	63	anbi2d 709	. . . . . 6 |- ( ( ( 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 2938	. . . . 5 |- ( ( 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 666	. . . 4 |- ( ( ( ( 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 214	. . 3 |- ( ( ( ( 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 28527	. 2 |- ( ( ( 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 799	1 |- ( ( W e. oGrp /\ (oppg ` W ) e. oGrp /\ W e. Archi ) -> W e. Abel )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 983   = wceq 1438   e. wcel 1873   A.wral 2776   E.wrex 2777   class class class wbr 4429   ` cfv 5607   Basecbs 15126   +g cplusg 15195   lecple 15202   0gc0g 15343   ltcplt 16191  Tosetctos 16284   Grpcgrp 16674  ._gcmg 16677  opp_gcoppg 17001   Abelcabl 17436  oMndcomnd 28473  oGrpcogrp 28474  Archicarchi 28507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-rep 4542  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603  ax-inf2 8161  ax-cnex 9608  ax-resscn 9609  ax-1cn 9610  ax-icn 9611  ax-addcl 9612  ax-addrcl 9613  ax-mulcl 9614  ax-mulrcl 9615  ax-mulcom 9616  ax-addass 9617  ax-mulass 9618  ax-distr 9619  ax-i2m1 9620  ax-1ne0 9621  ax-1rid 9622  ax-rnegex 9623  ax-rrecex 9624  ax-cnre 9625  ax-pre-lttri 9626  ax-pre-lttrn 9627  ax-pre-ltadd 9628  ax-pre-mulgt0 9629

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-tp 4009  df-op 4011  df-uni 4226  df-iun 4307  df-br 4430  df-opab 4489  df-mpt 4490  df-tr 4525  df-eprel 4770  df-id 4774  df-po 4780  df-so 4781  df-fr 4818  df-we 4820  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-pred 5405  df-ord 5451  df-on 5452  df-lim 5453  df-suc 5454  df-iota 5571  df-fun 5609  df-fn 5610  df-f 5611  df-f1 5612  df-fo 5613  df-f1o 5614  df-fv 5615  df-riota 6273  df-ov 6314  df-oprab 6315  df-mpt2 6316  df-om 6713  df-1st 6813  df-2nd 6814  df-tpos 6990  df-wrecs 7045  df-recs 7107  df-rdg 7145  df-er 7380  df-en 7587  df-dom 7588  df-sdom 7589  df-pnf 9690  df-mnf 9691  df-xr 9692  df-ltxr 9693  df-le 9694  df-sub 9875  df-neg 9876  df-nn 10623  df-2 10681  df-3 10682  df-4 10683  df-5 10684  df-6 10685  df-7 10686  df-8 10687  df-9 10688  df-10 10689  df-n0 10883  df-z 10951  df-uz 11173  df-fz 11798  df-seq 12226  df-ndx 15129  df-slot 15130  df-base 15131  df-sets 15132  df-plusg 15208  df-ple 15215  df-0g 15345  df-preset 16178  df-poset 16196  df-plt 16209  df-toset 16285  df-mgm 16493  df-sgrp 16532  df-mnd 16542  df-grp 16678  df-minusg 16679  df-sbg 16680  df-mulg 16681  df-oppg 17002  df-cmn 17437  df-abl 17438  df-omnd 28475  df-ogrp 28476  df-inftm 28508  df-archi 28509

This theorem is referenced by: (None)