archiabl

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

		Ref	Expression
	Assertion	archiabl	$⊢ (W \in oGrp \land {opp}_{𝑔} (W) \in oGrp \land W \in Archi) \to W \in Abel$

Proof

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

Metamath Proof Explorer

Theorem archiabl

Proof