Metamath Proof Explorer

Theorem archiabllem1b

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 13-Apr-2018)

Ref Expression
Hypotheses archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
archiabllem1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
archiabllem1.p ⊢ ( 𝜑 → 0 < 𝑈 )
archiabllem1.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
Assertion archiabllem1b ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
4 archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
5 archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
6 archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
7 archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
8 archiabllem1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
9 archiabllem1.p ⊢ ( 𝜑 → 0 < 𝑈 )
10 archiabllem1.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
11 0zd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 0 ) → 0 ∈ ℤ )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 0 ) → 𝑦 = 0 )
13 1 2 5 mulg0 ⊢ ( 𝑈 ∈ 𝐵 → ( 0 · 𝑈 ) = 0 )
14 8 13 syl ⊢ ( 𝜑 → ( 0 · 𝑈 ) = 0 )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 0 ) → ( 0 · 𝑈 ) = 0 )
16 12 15 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 0 ) → 𝑦 = ( 0 · 𝑈 ) )
17 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 · 𝑈 ) = ( 0 · 𝑈 ) )
18 17 rspceeqv ⊢ ( ( 0 ∈ ℤ ∧ 𝑦 = ( 0 · 𝑈 ) ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )
19 11 16 18 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 0 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → 𝑚 ∈ ℕ )
21 20 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → 𝑚 ∈ ℤ )
22 21 znegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → - 𝑚 ∈ ℤ )
23 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑈 ∈ 𝐵 )
24 23 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → 𝑈 ∈ 𝐵 )
25 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
26 1 5 25 mulgnegnn ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑈 ∈ 𝐵 ) → ( - 𝑚 · 𝑈 ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝑚 · 𝑈 ) ) )
27 20 24 26 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → ( - 𝑚 · 𝑈 ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝑚 · 𝑈 ) ) )
28 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) )
29 28 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝑚 · 𝑈 ) ) )
30 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ oGrp )
31 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ Grp )
33 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑦 ∈ 𝐵 )
34 1 25 grpinvinv ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = 𝑦 )
35 32 33 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = 𝑦 )
36 35 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = 𝑦 )
37 27 29 36 3eqtr2rd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → 𝑦 = ( - 𝑚 · 𝑈 ) )
38 oveq1 ⊢ ( 𝑛 = - 𝑚 → ( 𝑛 · 𝑈 ) = ( - 𝑚 · 𝑈 ) )
39 38 rspceeqv ⊢ ( ( - 𝑚 ∈ ℤ ∧ 𝑦 = ( - 𝑚 · 𝑈 ) ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )
40 22 37 39 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑚 ∈ ℕ ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )
41 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑊 ∈ Archi )
42 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 < 𝑈 )
43 simp1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝜑 )
44 43 10 syl3an1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
45 1 25 grpinvcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ∈ 𝐵 )
46 32 33 45 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ∈ 𝐵 )
47 1 2 grpidcl ⊢ ( 𝑊 ∈ Grp → 0 ∈ 𝐵 )
48 32 47 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 ∈ 𝐵 )
49 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 𝑦 < 0 )
50 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
51 1 4 50 ogrpaddlt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( 𝑦 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ∈ 𝐵 ) ∧ 𝑦 < 0 ) → ( 𝑦 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) < ( 0 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) )
52 30 33 48 46 49 51 syl131anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ( 𝑦 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) < ( 0 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) )
53 1 50 2 25 grprinv ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = 0 )
54 32 33 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ( 𝑦 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = 0 )
55 1 50 2 grplid ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) )
56 32 46 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ( 0 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) ) = ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) )
57 52 54 56 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → 0 < ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) )
58 1 2 3 4 5 30 41 23 42 44 46 57 archiabllem1a ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ∃ 𝑚 ∈ ℕ ( ( invg ‘ 𝑊 ) ‘ 𝑦 ) = ( 𝑚 · 𝑈 ) )
59 40 58 r19.29a ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 < 0 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )
60 59 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 < 0 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )
61 nnssz ⊢ ℕ ⊆ ℤ
62 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → 𝑊 ∈ oGrp )
63 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → 𝑊 ∈ Archi )
64 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → 𝑈 ∈ 𝐵 )
65 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → 0 < 𝑈 )
66 simp1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → 𝜑 )
67 66 10 syl3an1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
68 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → 𝑦 ∈ 𝐵 )
69 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → 0 < 𝑦 )
70 1 2 3 4 5 62 63 64 65 67 68 69 archiabllem1a ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 0 < 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝑛 · 𝑈 ) )
71 70 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝑛 · 𝑈 ) )
72 ssrexv ⊢ ( ℕ ⊆ ℤ → ( ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝑛 · 𝑈 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) ) )
73 61 71 72 mpsyl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑦 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )
74 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
75 74 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
76 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
77 6 75 76 3syl ⊢ ( 𝜑 → 𝑊 ∈ Toset )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ Toset )
79 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
80 6 31 47 3syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 0 ∈ 𝐵 )
82 1 4 tlt3 ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑦 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑦 = 0 ∨ 𝑦 < 0 ∨ 0 < 𝑦 ) )
83 78 79 81 82 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 = 0 ∨ 𝑦 < 0 ∨ 0 < 𝑦 ) )
84 19 60 73 83 mpjao3dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )