archiabllem1b

	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	archiabllem1b	$⊢ (φ \land y \in B) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$

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		0zd	$⊢ ((φ \land y \in B) \land y = \underset{˙}{0}) \to 0 \in ℤ$
12		simpr	$⊢ ((φ \land y \in B) \land y = \underset{˙}{0}) \to y = \underset{˙}{0}$
13	1 2 5	mulg0	$⊢ U \in B \to 0 \underset{˙}{\cdot} U = \underset{˙}{0}$
14	8 13	syl	$⊢ φ \to 0 \underset{˙}{\cdot} U = \underset{˙}{0}$
15	14	ad2antrr	$⊢ ((φ \land y \in B) \land y = \underset{˙}{0}) \to 0 \underset{˙}{\cdot} U = \underset{˙}{0}$
16	12 15	eqtr4d	$⊢ ((φ \land y \in B) \land y = \underset{˙}{0}) \to y = 0 \underset{˙}{\cdot} U$
17		oveq1	$⊢ n = 0 \to n \underset{˙}{\cdot} U = 0 \underset{˙}{\cdot} U$
18	17	rspceeqv	$⊢ (0 \in ℤ \land y = 0 \underset{˙}{\cdot} U) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$
19	11 16 18	syl2anc	$⊢ ((φ \land y \in B) \land y = \underset{˙}{0}) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$
20		simplr	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to m \in ℕ$
21	20	nnzd	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to m \in ℤ$
22	21	znegcld	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to - m \in ℤ$
23	8	3ad2ant1	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to U \in B$
24	23	ad2antrr	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to U \in B$
25		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
26	1 5 25	mulgnegnn	$⊢ (m \in ℕ \land U \in B) \to (- m) \underset{˙}{\cdot} U = {inv}_{g} (W) (m \underset{˙}{\cdot} U)$
27	20 24 26	syl2anc	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to (- m) \underset{˙}{\cdot} U = {inv}_{g} (W) (m \underset{˙}{\cdot} U)$
28		simpr	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U$
29	28	fveq2d	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to {inv}_{g} (W) ({inv}_{g} (W) (y)) = {inv}_{g} (W) (m \underset{˙}{\cdot} U)$
30	6	3ad2ant1	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to W \in oGrp$
31		ogrpgrp	$⊢ W \in oGrp \to W \in Grp$
32	30 31	syl	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to W \in Grp$
33		simp2	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to y \in B$
34	1 25	grpinvinv	$⊢ (W \in Grp \land y \in B) \to {inv}_{g} (W) ({inv}_{g} (W) (y)) = y$
35	32 33 34	syl2anc	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to {inv}_{g} (W) ({inv}_{g} (W) (y)) = y$
36	35	ad2antrr	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to {inv}_{g} (W) ({inv}_{g} (W) (y)) = y$
37	27 29 36	3eqtr2rd	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to y = (- m) \underset{˙}{\cdot} U$
38		oveq1	$⊢ n = - m \to n \underset{˙}{\cdot} U = (- m) \underset{˙}{\cdot} U$
39	38	rspceeqv	$⊢ (- m \in ℤ \land y = (- m) \underset{˙}{\cdot} U) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$
40	22 37 39	syl2anc	$⊢ (((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land m \in ℕ) \land {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$
41	7	3ad2ant1	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to W \in Archi$
42	9	3ad2ant1	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{<} U$
43		simp1	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to φ$
44	43 10	syl3an1	$⊢ ((φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \land x \in B \land \underset{˙}{0} \underset{˙}{<} x) \to U \underset{˙}{\leq} x$
45	1 25	grpinvcl	$⊢ (W \in Grp \land y \in B) \to {inv}_{g} (W) (y) \in B$
46	32 33 45	syl2anc	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to {inv}_{g} (W) (y) \in B$
47	1 2	grpidcl	$⊢ W \in Grp \to \underset{˙}{0} \in B$
48	32 47	syl	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to \underset{˙}{0} \in B$
49		simp3	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to y \underset{˙}{<} \underset{˙}{0}$
50		eqid	$⊢ +_{W} = +_{W}$
51	1 4 50	ogrpaddlt	$⊢ (W \in oGrp \land (y \in B \land \underset{˙}{0} \in B \land {inv}_{g} (W) (y) \in B) \land y \underset{˙}{<} \underset{˙}{0}) \to (y +_{W} {inv}_{g} (W) (y)) \underset{˙}{<} (\underset{˙}{0} +_{W} {inv}_{g} (W) (y))$
52	30 33 48 46 49 51	syl131anc	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to (y +_{W} {inv}_{g} (W) (y)) \underset{˙}{<} (\underset{˙}{0} +_{W} {inv}_{g} (W) (y))$
53	1 50 2 25	grprinv	$⊢ (W \in Grp \land y \in B) \to y +_{W} {inv}_{g} (W) (y) = \underset{˙}{0}$
54	32 33 53	syl2anc	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to y +_{W} {inv}_{g} (W) (y) = \underset{˙}{0}$
55	1 50 2	grplid	$⊢ (W \in Grp \land {inv}_{g} (W) (y) \in B) \to \underset{˙}{0} +_{W} {inv}_{g} (W) (y) = {inv}_{g} (W) (y)$
56	32 46 55	syl2anc	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to \underset{˙}{0} +_{W} {inv}_{g} (W) (y) = {inv}_{g} (W) (y)$
57	52 54 56	3brtr3d	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{<} {inv}_{g} (W) (y)$
58	1 2 3 4 5 30 41 23 42 44 46 57	archiabllem1a	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to \exists m \in ℕ {inv}_{g} (W) (y) = m \underset{˙}{\cdot} U$
59	40 58	r19.29a	$⊢ (φ \land y \in B \land y \underset{˙}{<} \underset{˙}{0}) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$
60	59	3expa	$⊢ ((φ \land y \in B) \land y \underset{˙}{<} \underset{˙}{0}) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$
61		nnssz	$⊢ ℕ \subseteq ℤ$
62	6	3ad2ant1	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to W \in oGrp$
63	7	3ad2ant1	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to W \in Archi$
64	8	3ad2ant1	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to U \in B$
65	9	3ad2ant1	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to \underset{˙}{0} \underset{˙}{<} U$
66		simp1	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to φ$
67	66 10	syl3an1	$⊢ ((φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \land x \in B \land \underset{˙}{0} \underset{˙}{<} x) \to U \underset{˙}{\leq} x$
68		simp2	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to y \in B$
69		simp3	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to \underset{˙}{0} \underset{˙}{<} y$
70	1 2 3 4 5 62 63 64 65 67 68 69	archiabllem1a	$⊢ (φ \land y \in B \land \underset{˙}{0} \underset{˙}{<} y) \to \exists n \in ℕ y = n \underset{˙}{\cdot} U$
71	70	3expa	$⊢ ((φ \land y \in B) \land \underset{˙}{0} \underset{˙}{<} y) \to \exists n \in ℕ y = n \underset{˙}{\cdot} U$
72		ssrexv	$⊢ ℕ \subseteq ℤ \to (\exists n \in ℕ y = n \underset{˙}{\cdot} U \to \exists n \in ℤ y = n \underset{˙}{\cdot} U)$
73	61 71 72	mpsyl	$⊢ ((φ \land y \in B) \land \underset{˙}{0} \underset{˙}{<} y) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$
74		isogrp	$⊢ W \in oGrp \leftrightarrow (W \in Grp \land W \in oMnd)$
75	74	simprbi	$⊢ W \in oGrp \to W \in oMnd$
76		omndtos	$⊢ W \in oMnd \to W \in Toset$
77	6 75 76	3syl	$⊢ φ \to W \in Toset$
78	77	adantr	$⊢ (φ \land y \in B) \to W \in Toset$
79		simpr	$⊢ (φ \land y \in B) \to y \in B$
80	6 31 47	3syl	$⊢ φ \to \underset{˙}{0} \in B$
81	80	adantr	$⊢ (φ \land y \in B) \to \underset{˙}{0} \in B$
82	1 4	tlt3	$⊢ (W \in Toset \land y \in B \land \underset{˙}{0} \in B) \to (y = \underset{˙}{0} \lor y \underset{˙}{<} \underset{˙}{0} \lor \underset{˙}{0} \underset{˙}{<} y)$
83	78 79 81 82	syl3anc	$⊢ (φ \land y \in B) \to (y = \underset{˙}{0} \lor y \underset{˙}{<} \underset{˙}{0} \lor \underset{˙}{0} \underset{˙}{<} y)$
84	19 60 73 83	mpjao3dan	$⊢ (φ \land y \in B) \to \exists n \in ℤ y = n \underset{˙}{\cdot} U$

Metamath Proof Explorer

Theorem archiabllem1b

Proof