archiabllem1

Description: Archimedean ordered groups with a minimal positive value are abelian. (Contributed by Thierry Arnoux, 13-Apr-2018)

	Ref	Expression
Hypotheses	archiabllem.b	$⊢ B = {Base}_{W}$
	archiabllem.0	$⊢ \underset{˙}{0} = 0_{W}$
	archiabllem.e	$⊢ \underset{˙}{\leq} = \leq_{W}$
	archiabllem.t	$⊢ \underset{˙}{<} = <_{W}$
	archiabllem.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	archiabllem.g	$⊢ φ \to W \in oGrp$
	archiabllem.a	$⊢ φ \to W \in Archi$
	archiabllem1.u	$⊢ φ \to U \in B$
	archiabllem1.p	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} U$
	archiabllem1.s	$⊢ (φ \land x \in B \land \underset{˙}{0} \underset{˙}{<} x) \to U \underset{˙}{\leq} x$
Assertion	archiabllem1	$⊢ φ \to W \in Abel$

Proof

Step	Hyp	Ref	Expression
1		archiabllem.b	$⊢ B = {Base}_{W}$
2		archiabllem.0	$⊢ \underset{˙}{0} = 0_{W}$
3		archiabllem.e	$⊢ \underset{˙}{\leq} = \leq_{W}$
4		archiabllem.t	$⊢ \underset{˙}{<} = <_{W}$
5		archiabllem.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		archiabllem.g	$⊢ φ \to W \in oGrp$
7		archiabllem.a	$⊢ φ \to W \in Archi$
8		archiabllem1.u	$⊢ φ \to U \in B$
9		archiabllem1.p	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} U$
10		archiabllem1.s	$⊢ (φ \land x \in B \land \underset{˙}{0} \underset{˙}{<} x) \to U \underset{˙}{\leq} x$
11		ogrpgrp	$⊢ W \in oGrp \to W \in Grp$
12	6 11	syl	$⊢ φ \to W \in Grp$
13		simplr	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to m \in ℤ$
14	13	zcnd	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to m \in ℂ$
15		simpr	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to n \in ℤ$
16	15	zcnd	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to n \in ℂ$
17	14 16	addcomd	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to m + n = n + m$
18	17	oveq1d	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to (m + n) \underset{˙}{\cdot} U = (n + m) \underset{˙}{\cdot} U$
19	12	ad2antrr	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to W \in Grp$
20	8	ad2antrr	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to U \in B$
21		eqid	$⊢ +_{W} = +_{W}$
22	1 5 21	mulgdir	$⊢ (W \in Grp \land (m \in ℤ \land n \in ℤ \land U \in B)) \to (m + n) \underset{˙}{\cdot} U = (m \underset{˙}{\cdot} U) +_{W} (n \underset{˙}{\cdot} U)$
23	19 13 15 20 22	syl13anc	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to (m + n) \underset{˙}{\cdot} U = (m \underset{˙}{\cdot} U) +_{W} (n \underset{˙}{\cdot} U)$
24	1 5 21	mulgdir	$⊢ (W \in Grp \land (n \in ℤ \land m \in ℤ \land U \in B)) \to (n + m) \underset{˙}{\cdot} U = (n \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
25	19 15 13 20 24	syl13anc	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to (n + m) \underset{˙}{\cdot} U = (n \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
26	18 23 25	3eqtr3d	$⊢ ((φ \land m \in ℤ) \land n \in ℤ) \to (m \underset{˙}{\cdot} U) +_{W} (n \underset{˙}{\cdot} U) = (n \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
27	26	adantllr	$⊢ (((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land n \in ℤ) \to (m \underset{˙}{\cdot} U) +_{W} (n \underset{˙}{\cdot} U) = (n \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
28	27	adantlr	$⊢ ((((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \land n \in ℤ) \to (m \underset{˙}{\cdot} U) +_{W} (n \underset{˙}{\cdot} U) = (n \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
29	28	adantr	$⊢ (((((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \land n \in ℤ) \land z = n \underset{˙}{\cdot} U) \to (m \underset{˙}{\cdot} U) +_{W} (n \underset{˙}{\cdot} U) = (n \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
30		simpllr	$⊢ (((((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \land n \in ℤ) \land z = n \underset{˙}{\cdot} U) \to y = m \underset{˙}{\cdot} U$
31		simpr	$⊢ (((((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \land n \in ℤ) \land z = n \underset{˙}{\cdot} U) \to z = n \underset{˙}{\cdot} U$
32	30 31	oveq12d	$⊢ (((((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \land n \in ℤ) \land z = n \underset{˙}{\cdot} U) \to y +_{W} z = (m \underset{˙}{\cdot} U) +_{W} (n \underset{˙}{\cdot} U)$
33	31 30	oveq12d	$⊢ (((((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \land n \in ℤ) \land z = n \underset{˙}{\cdot} U) \to z +_{W} y = (n \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
34	29 32 33	3eqtr4d	$⊢ (((((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \land n \in ℤ) \land z = n \underset{˙}{\cdot} U) \to y +_{W} z = z +_{W} y$
35		simplll	$⊢ (((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \to φ$
36		simpr1r	$⊢ (φ \land ((y \in B \land z \in B) \land m \in ℤ \land y = m \underset{˙}{\cdot} U)) \to z \in B$
37	36	3anassrs	$⊢ (((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \to z \in B$
38	1 2 3 4 5 6 7 8 9 10	archiabllem1b	$⊢ (φ \land z \in B) \to \exists n \in ℤ z = n \underset{˙}{\cdot} U$
39	35 37 38	syl2anc	$⊢ (((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \to \exists n \in ℤ z = n \underset{˙}{\cdot} U$
40	34 39	r19.29a	$⊢ (((φ \land (y \in B \land z \in B)) \land m \in ℤ) \land y = m \underset{˙}{\cdot} U) \to y +_{W} z = z +_{W} y$
41	1 2 3 4 5 6 7 8 9 10	archiabllem1b	$⊢ (φ \land y \in B) \to \exists m \in ℤ y = m \underset{˙}{\cdot} U$
42	41	adantrr	$⊢ (φ \land (y \in B \land z \in B)) \to \exists m \in ℤ y = m \underset{˙}{\cdot} U$
43	40 42	r19.29a	$⊢ (φ \land (y \in B \land z \in B)) \to y +_{W} z = z +_{W} y$
44	43	ralrimivva	$⊢ φ \to \forall y \in B \forall z \in B y +_{W} z = z +_{W} y$
45	1 21	isabl2	$⊢ W \in Abel \leftrightarrow (W \in Grp \land \forall y \in B \forall z \in B y +_{W} z = z +_{W} y)$
46	12 44 45	sylanbrc	$⊢ φ \to W \in Abel$

Metamath Proof Explorer

Theorem archiabllem1

Proof