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		breq2	$⊢ u = v \to (0_{W} <_{W} u \leftrightarrow 0_{W} <_{W} v)$
21		breq1	$⊢ u = v \to (u \leq_{W} x \leftrightarrow v \leq_{W} x)$
22	21	imbi2d	$⊢ u = v \to ((0_{W} <_{W} x \to u \leq_{W} x) \leftrightarrow (0_{W} <_{W} x \to v \leq_{W} x))$
23	22	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))$
24	20 23	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)))$
25	24	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))$
26	25	bilani	$⊢ ((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))$
27	19 26	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$
28		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$
29		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$
30		eqid	$⊢ +_{W} = +_{W}$
31		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$
32		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))$
33	32	bilanri	$⊢ ((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))$
34		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)$
35	34	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))$
36		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))$
37	35 36	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))$
38	37	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))$
39	33 38	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))$
40	21	notbid	$⊢ u = v \to (\neg u \leq_{W} x \leftrightarrow \neg v \leq_{W} x)$
41	40	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))$
42	41	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))$
43	20 42	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)))$
44	43	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))$
45	39 44	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))$
46	45	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))$
47	14	notbid	$⊢ x = y \to (\neg v \leq_{W} x \leftrightarrow \neg v \leq_{W} y)$
48	13 47	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))$
49	48	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)$
50	46 49	imbitrdi	$⊢ (((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))$
51	50	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)$
52		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$
53		isogrp	$⊢ W \in oGrp \leftrightarrow (W \in Grp \land W \in oMnd)$
54	53	simprbi	$⊢ W \in oGrp \to W \in oMnd$
55		omndtos	$⊢ W \in oMnd \to W \in Toset$
56	52 54 55	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$
57		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}$
58	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)$
59	58	bicomd	$⊢ (W \in Toset \land y \in {Base}_{W} \land v \in {Base}_{W}) \to (\neg v \leq_{W} y \leftrightarrow y <_{W} v)$
60	59	3com23	$⊢ (W \in Toset \land v \in {Base}_{W} \land y \in {Base}_{W}) \to (\neg v \leq_{W} y \leftrightarrow y <_{W} v)$
61	60	3expa	$⊢ ((W \in Toset \land v \in {Base}_{W}) \land y \in {Base}_{W}) \to (\neg v \leq_{W} y \leftrightarrow y <_{W} v)$
62	61	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))$
63	62	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))$
64	56 57 63	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))$
65	51 64	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)$
66	1 2 3 4 5 28 29 30 31 65	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$
67	27 66	pm2.61dan	$⊢ (W \in oGrp \land {opp}_{𝑔} (W) \in oGrp \land W \in Archi) \to W \in Abel$

Metamath Proof Explorer

Theorem archiabl

Proof