Theorem archiabl 32385

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

Assertion

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

Proof of Theorem archiabl

Dummy variables 𝑣 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2732	. . . . 5 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2732	. . . . 5 ⊢ (0g‘𝑊) = (0g‘𝑊)
3		eqid 2732	. . . . 5 ⊢ (le‘𝑊) = (le‘𝑊)
4		eqid 2732	. . . . 5 ⊢ (lt‘𝑊) = (lt‘𝑊)
5		eqid 2732	. . . . 5 ⊢ (.g‘𝑊) = (.g‘𝑊)
6		simpll1 1212	. . . . 5 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) → 𝑊 ∈ oGrp)
7		simpll3 1214	. . . . 5 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) → 𝑊 ∈ Archi)
8		simplr 767	. . . . 5 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) → 𝑣 ∈ (Base‘𝑊))
9		simprl 769	. . . . 5 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) → (0g‘𝑊)(lt‘𝑊)𝑣)
10		simp2 1137	. . . . . 6 ⊢ (((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) ∧ 𝑦 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑦) → 𝑦 ∈ (Base‘𝑊))
11		simp1rr 1239	. . . . . 6 ⊢ (((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) ∧ 𝑦 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑦) → ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))
12		simp3 1138	. . . . . 6 ⊢ (((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) ∧ 𝑦 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑦) → (0g‘𝑊)(lt‘𝑊)𝑦)
13		breq2 5152	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((0g‘𝑊)(lt‘𝑊)𝑥 ↔ (0g‘𝑊)(lt‘𝑊)𝑦))
14		breq2 5152	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑣(le‘𝑊)𝑥 ↔ 𝑣(le‘𝑊)𝑦))
15	13, 14	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥) ↔ ((0g‘𝑊)(lt‘𝑊)𝑦 → 𝑣(le‘𝑊)𝑦)))
16	15	rspcv 3608	. . . . . 6 ⊢ (𝑦 ∈ (Base‘𝑊) → (∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥) → ((0g‘𝑊)(lt‘𝑊)𝑦 → 𝑣(le‘𝑊)𝑦)))
17	10, 11, 12, 16	syl3c 66	. . . . 5 ⊢ (((((𝑊 ∈ 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 32380	. . . 4 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) → 𝑊 ∈ Abel)
19	18	adantllr 717	. . 3 ⊢ (((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))) → 𝑊 ∈ Abel)
20		simpr 485	. . . 4 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
21		breq2 5152	. . . . . 6 ⊢ (𝑢 = 𝑣 → ((0g‘𝑊)(lt‘𝑊)𝑢 ↔ (0g‘𝑊)(lt‘𝑊)𝑣))
22		breq1 5151	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → (𝑢(le‘𝑊)𝑥 ↔ 𝑣(le‘𝑊)𝑥))
23	22	imbi2d 340	. . . . . . 7 ⊢ (𝑢 = 𝑣 → (((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥) ↔ ((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥)))
24	23	ralbidv 3177	. . . . . 6 ⊢ (𝑢 = 𝑣 → (∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥) ↔ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥)))
25	21, 24	anbi12d 631	. . . . 5 ⊢ (𝑢 = 𝑣 → (((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)) ↔ ((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥))))
26	25	cbvrexvw 3235	. . . 4 ⊢ (∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)) ↔ ∃𝑣 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥)))
27	20, 26	sylib 217	. . 3 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → ∃𝑣 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑣 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑣(le‘𝑊)𝑥)))
28	19, 27	r19.29a 3162	. 2 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → 𝑊 ∈ Abel)
29		simpl1 1191	. . 3 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → 𝑊 ∈ oGrp)
30		simpl3 1193	. . 3 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → 𝑊 ∈ Archi)
31		eqid 2732	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
32		simpl2 1192	. . 3 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → (oppg‘𝑊) ∈ oGrp)
33		simpr 485	. . . . . . . . . 10 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
34		ralnex 3072	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ (Base‘𝑊) ¬ ((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)) ↔ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
35	33, 34	sylibr 233	. . . . . . . . 9 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → ∀𝑢 ∈ (Base‘𝑊) ¬ ((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
36		rexanali 3102	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥) ↔ ¬ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))
37	36	imbi2i 335	. . . . . . . . . . 11 ⊢ (((0g‘𝑊)(lt‘𝑊)𝑢 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥)) ↔ ((0g‘𝑊)(lt‘𝑊)𝑢 → ¬ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
38		imnan 400	. . . . . . . . . . 11 ⊢ (((0g‘𝑊)(lt‘𝑊)𝑢 → ¬ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)) ↔ ¬ ((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
39	37, 38	bitri 274	. . . . . . . . . 10 ⊢ (((0g‘𝑊)(lt‘𝑊)𝑢 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥)) ↔ ¬ ((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
40	39	ralbii 3093	. . . . . . . . 9 ⊢ (∀𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥)) ↔ ∀𝑢 ∈ (Base‘𝑊) ¬ ((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥)))
41	35, 40	sylibr 233	. . . . . . . 8 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → ∀𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥)))
42	22	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → (¬ 𝑢(le‘𝑊)𝑥 ↔ ¬ 𝑣(le‘𝑊)𝑥))
43	42	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → (((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥) ↔ ((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥)))
44	43	rexbidv 3178	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥) ↔ ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥)))
45	21, 44	imbi12d 344	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (((0g‘𝑊)(lt‘𝑊)𝑢 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥)) ↔ ((0g‘𝑊)(lt‘𝑊)𝑣 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥))))
46	45	cbvralvw 3234	. . . . . . . 8 ⊢ (∀𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑢(le‘𝑊)𝑥)) ↔ ∀𝑣 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑣 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥)))
47	41, 46	sylib 217	. . . . . . 7 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → ∀𝑣 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑣 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥)))
48	47	r19.21bi 3248	. . . . . 6 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊)) → ((0g‘𝑊)(lt‘𝑊)𝑣 → ∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥)))
49	14	notbid 317	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (¬ 𝑣(le‘𝑊)𝑥 ↔ ¬ 𝑣(le‘𝑊)𝑦))
50	13, 49	anbi12d 631	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥) ↔ ((0g‘𝑊)(lt‘𝑊)𝑦 ∧ ¬ 𝑣(le‘𝑊)𝑦)))
51	50	cbvrexvw 3235	. . . . . 6 ⊢ (∃𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 ∧ ¬ 𝑣(le‘𝑊)𝑥) ↔ ∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ ¬ 𝑣(le‘𝑊)𝑦))
52	48, 51	imbitrdi 250	. . . . 5 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊)) → ((0g‘𝑊)(lt‘𝑊)𝑣 → ∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ ¬ 𝑣(le‘𝑊)𝑦)))
53	52	3impia 1117	. . . 4 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑣) → ∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ ¬ 𝑣(le‘𝑊)𝑦))
54		simp1l1 1266	. . . . . 6 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑣) → 𝑊 ∈ oGrp)
55		isogrp 32261	. . . . . . 7 ⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd))
56	55	simprbi 497	. . . . . 6 ⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd)
57		omndtos 32264	. . . . . 6 ⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset)
58	54, 56, 57	3syl 18	. . . . 5 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑣) → 𝑊 ∈ Toset)
59		simp2 1137	. . . . 5 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑣) → 𝑣 ∈ (Base‘𝑊))
60	1, 3, 4	tltnle 18377	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Toset ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑣 ∈ (Base‘𝑊)) → (𝑦(lt‘𝑊)𝑣 ↔ ¬ 𝑣(le‘𝑊)𝑦))
61	60	bicomd 222	. . . . . . . . 9 ⊢ ((𝑊 ∈ Toset ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑣 ∈ (Base‘𝑊)) → (¬ 𝑣(le‘𝑊)𝑦 ↔ 𝑦(lt‘𝑊)𝑣))
62	61	3com23 1126	. . . . . . . 8 ⊢ ((𝑊 ∈ Toset ∧ 𝑣 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (¬ 𝑣(le‘𝑊)𝑦 ↔ 𝑦(lt‘𝑊)𝑣))
63	62	3expa 1118	. . . . . . 7 ⊢ (((𝑊 ∈ Toset ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → (¬ 𝑣(le‘𝑊)𝑦 ↔ 𝑦(lt‘𝑊)𝑣))
64	63	anbi2d 629	. . . . . 6 ⊢ (((𝑊 ∈ Toset ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → (((0g‘𝑊)(lt‘𝑊)𝑦 ∧ ¬ 𝑣(le‘𝑊)𝑦) ↔ ((0g‘𝑊)(lt‘𝑊)𝑦 ∧ 𝑦(lt‘𝑊)𝑣)))
65	64	rexbidva 3176	. . . . 5 ⊢ ((𝑊 ∈ Toset ∧ 𝑣 ∈ (Base‘𝑊)) → (∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ ¬ 𝑣(le‘𝑊)𝑦) ↔ ∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ 𝑦(lt‘𝑊)𝑣)))
66	58, 59, 65	syl2anc 584	. . . 4 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑣) → (∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ ¬ 𝑣(le‘𝑊)𝑦) ↔ ∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ 𝑦(lt‘𝑊)𝑣)))
67	53, 66	mpbid 231	. . 3 ⊢ ((((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) ∧ 𝑣 ∈ (Base‘𝑊) ∧ (0g‘𝑊)(lt‘𝑊)𝑣) → ∃𝑦 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑦 ∧ 𝑦(lt‘𝑊)𝑣))
68	1, 2, 3, 4, 5, 29, 30, 31, 32, 67	archiabllem2 32384	. 2 ⊢ (((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) ∧ ¬ ∃𝑢 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑢 ∧ ∀𝑥 ∈ (Base‘𝑊)((0g‘𝑊)(lt‘𝑊)𝑥 → 𝑢(le‘𝑊)𝑥))) → 𝑊 ∈ Abel)
69	28, 68	pm2.61dan 811	1 ⊢ ((𝑊 ∈ oGrp ∧ (oppg‘𝑊) ∈ oGrp ∧ 𝑊 ∈ Archi) → 𝑊 ∈ Abel)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070   class class class wbr 5148  ‘cfv 6543  Basecbs 17146  +_gcplusg 17199  lecple 17206  0_gc0g 17387  ltcplt 18263  Tosetctos 18371  Grpcgrp 18821  ._gcmg 18952  opp_gcoppg 19211  Abelcabl 19651  oMndcomnd 32256  oGrpcogrp 32257  Archicarchi 32364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-fz 13487  df-seq 13969  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-plusg 17212  df-ple 17219  df-0g 17389  df-proset 18250  df-poset 18268  df-plt 18285  df-toset 18372  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-grp 18824  df-minusg 18825  df-sbg 18826  df-mulg 18953  df-oppg 19212  df-cmn 19652  df-abl 19653  df-omnd 32258  df-ogrp 32259  df-inftm 32365  df-archi 32366

This theorem is referenced by: (None)