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𝑦 < 00 < 𝑦 ) )
83 78 79 81 82 syl3anc ( ( 𝜑𝑦𝐵 ) → ( 𝑦 = 0𝑦 < 00 < 𝑦 ) )
84 19 60 73 83 mpjao3dan ( ( 𝜑𝑦𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑈 ) )