Metamath Proof Explorer

Theorem fimgmcyc

Description: Version of odcl2 for finite magmas: the multiples of an element A e. B are eventually periodic. (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses fimgmcyc.b ⊢ B = Base M
fimgmcyc.m ⊢ · ˙ = ⋅ M
fimgmcyc.s ⊢ φ → M ∈ Mgm
fimgmcyc.f ⊢ φ → B ∈ Fin
fimgmcyc.a ⊢ φ → A ∈ B
Assertion fimgmcyc ⊢ φ → ∃ o ∈ ℕ ∃ p ∈ ℕ o · ˙ A = o + p · ˙ A

Proof

Step Hyp Ref Expression
1 fimgmcyc.b ⊢ B = Base M
2 fimgmcyc.m ⊢ · ˙ = ⋅ M
3 fimgmcyc.s ⊢ φ → M ∈ Mgm
4 fimgmcyc.f ⊢ φ → B ∈ Fin
5 fimgmcyc.a ⊢ φ → A ∈ B
6 domnsym ⊢ ℕ ≼ B → ¬ B ≺ ℕ
7 fisdomnn ⊢ B ∈ Fin → B ≺ ℕ
8 4 7 syl ⊢ φ → B ≺ ℕ
9 6 8 nsyl3 ⊢ φ → ¬ ℕ ≼ B
10 1 fvexi ⊢ B ∈ V
11 10 f1dom ⊢ n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ 1-1 B → ℕ ≼ B
12 9 11 nsyl ⊢ φ → ¬ n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ 1-1 B
13 3 adantr ⊢ φ ∧ n ∈ ℕ → M ∈ Mgm
14 simpr ⊢ φ ∧ n ∈ ℕ → n ∈ ℕ
15 5 adantr ⊢ φ ∧ n ∈ ℕ → A ∈ B
16 1 2 mulgnncl ⊢ M ∈ Mgm ∧ n ∈ ℕ ∧ A ∈ B → n · ˙ A ∈ B
17 13 14 15 16 syl3anc ⊢ φ ∧ n ∈ ℕ → n · ˙ A ∈ B
18 17 fmpttd ⊢ φ → n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ B
19 dff13 ⊢ n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ 1-1 B ↔ n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ B ∧ ∀ o ∈ ℕ ∀ q ∈ ℕ n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q → o = q
20 19 baib ⊢ n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ B → n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ 1-1 B ↔ ∀ o ∈ ℕ ∀ q ∈ ℕ n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q → o = q
21 18 20 syl ⊢ φ → n ∈ ℕ ⟼ n · ˙ A : ℕ ⟶ 1-1 B ↔ ∀ o ∈ ℕ ∀ q ∈ ℕ n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q → o = q
22 12 21 mtbid ⊢ φ → ¬ ∀ o ∈ ℕ ∀ q ∈ ℕ n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q → o = q
23 oveq1 ⊢ n = o → n · ˙ A = o · ˙ A
24 eqid ⊢ n ∈ ℕ ⟼ n · ˙ A = n ∈ ℕ ⟼ n · ˙ A
25 ovex ⊢ o · ˙ A ∈ V
26 23 24 25 fvmpt ⊢ o ∈ ℕ → n ∈ ℕ ⟼ n · ˙ A ⁡ o = o · ˙ A
27 oveq1 ⊢ n = q → n · ˙ A = q · ˙ A
28 ovex ⊢ q · ˙ A ∈ V
29 27 24 28 fvmpt ⊢ q ∈ ℕ → n ∈ ℕ ⟼ n · ˙ A ⁡ q = q · ˙ A
30 26 29 eqeqan12d ⊢ o ∈ ℕ ∧ q ∈ ℕ → n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q ↔ o · ˙ A = q · ˙ A
31 30 imbi1d ⊢ o ∈ ℕ ∧ q ∈ ℕ → n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q → o = q ↔ o · ˙ A = q · ˙ A → o = q
32 31 ralbidva ⊢ o ∈ ℕ → ∀ q ∈ ℕ n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q → o = q ↔ ∀ q ∈ ℕ o · ˙ A = q · ˙ A → o = q
33 32 ralbiia ⊢ ∀ o ∈ ℕ ∀ q ∈ ℕ n ∈ ℕ ⟼ n · ˙ A ⁡ o = n ∈ ℕ ⟼ n · ˙ A ⁡ q → o = q ↔ ∀ o ∈ ℕ ∀ q ∈ ℕ o · ˙ A = q · ˙ A → o = q
34 22 33 sylnib ⊢ φ → ¬ ∀ o ∈ ℕ ∀ q ∈ ℕ o · ˙ A = q · ˙ A → o = q
35 df-ne ⊢ o ≠ q ↔ ¬ o = q
36 35 anbi1i ⊢ o ≠ q ∧ o · ˙ A = q · ˙ A ↔ ¬ o = q ∧ o · ˙ A = q · ˙ A
37 ancom ⊢ ¬ o = q ∧ o · ˙ A = q · ˙ A ↔ o · ˙ A = q · ˙ A ∧ ¬ o = q
38 annim ⊢ o · ˙ A = q · ˙ A ∧ ¬ o = q ↔ ¬ o · ˙ A = q · ˙ A → o = q
39 36 37 38 3bitri ⊢ o ≠ q ∧ o · ˙ A = q · ˙ A ↔ ¬ o · ˙ A = q · ˙ A → o = q
40 39 2rexbii ⊢ ∃ o ∈ ℕ ∃ q ∈ ℕ o ≠ q ∧ o · ˙ A = q · ˙ A ↔ ∃ o ∈ ℕ ∃ q ∈ ℕ ¬ o · ˙ A = q · ˙ A → o = q
41 rexnal2 ⊢ ∃ o ∈ ℕ ∃ q ∈ ℕ ¬ o · ˙ A = q · ˙ A → o = q ↔ ¬ ∀ o ∈ ℕ ∀ q ∈ ℕ o · ˙ A = q · ˙ A → o = q
42 40 41 bitri ⊢ ∃ o ∈ ℕ ∃ q ∈ ℕ o ≠ q ∧ o · ˙ A = q · ˙ A ↔ ¬ ∀ o ∈ ℕ ∀ q ∈ ℕ o · ˙ A = q · ˙ A → o = q
43 34 42 sylibr ⊢ φ → ∃ o ∈ ℕ ∃ q ∈ ℕ o ≠ q ∧ o · ˙ A = q · ˙ A
44 43 fimgmcyclem ⊢ φ → ∃ o ∈ ℕ ∃ q ∈ ℕ o < q ∧ o · ˙ A = q · ˙ A
45 nnz ⊢ o ∈ ℕ → o ∈ ℤ
46 eluzp1 ⊢ o ∈ ℤ → q ∈ ℤ ≥ o + 1 ↔ q ∈ ℤ ∧ o < q
47 45 46 syl ⊢ o ∈ ℕ → q ∈ ℤ ≥ o + 1 ↔ q ∈ ℤ ∧ o < q
48 idd ⊢ o ∈ ℕ ∧ o < q → q ∈ ℤ → q ∈ ℤ
49 nnz ⊢ q ∈ ℕ → q ∈ ℤ
50 49 a1i ⊢ o ∈ ℕ ∧ o < q → q ∈ ℕ → q ∈ ℤ
51 0red ⊢ o ∈ ℕ ∧ o < q ∧ q ∈ ℤ → 0 ∈ ℝ
52 nnre ⊢ o ∈ ℕ → o ∈ ℝ
53 52 ad2antrr ⊢ o ∈ ℕ ∧ o < q ∧ q ∈ ℤ → o ∈ ℝ
54 zre ⊢ q ∈ ℤ → q ∈ ℝ
55 54 adantl ⊢ o ∈ ℕ ∧ o < q ∧ q ∈ ℤ → q ∈ ℝ
56 nngt0 ⊢ o ∈ ℕ → 0 < o
57 56 ad2antrr ⊢ o ∈ ℕ ∧ o < q ∧ q ∈ ℤ → 0 < o
58 simplr ⊢ o ∈ ℕ ∧ o < q ∧ q ∈ ℤ → o < q
59 51 53 55 57 58 lttrd ⊢ o ∈ ℕ ∧ o < q ∧ q ∈ ℤ → 0 < q
60 elnnz ⊢ q ∈ ℕ ↔ q ∈ ℤ ∧ 0 < q
61 60 rbaibr ⊢ 0 < q → q ∈ ℤ ↔ q ∈ ℕ
62 59 61 syl ⊢ o ∈ ℕ ∧ o < q ∧ q ∈ ℤ → q ∈ ℤ ↔ q ∈ ℕ
63 62 ex ⊢ o ∈ ℕ ∧ o < q → q ∈ ℤ → q ∈ ℤ ↔ q ∈ ℕ
64 48 50 63 pm5.21ndd ⊢ o ∈ ℕ ∧ o < q → q ∈ ℤ ↔ q ∈ ℕ
65 64 ex ⊢ o ∈ ℕ → o < q → q ∈ ℤ ↔ q ∈ ℕ
66 65 pm5.32rd ⊢ o ∈ ℕ → q ∈ ℤ ∧ o < q ↔ q ∈ ℕ ∧ o < q
67 47 66 bitrd ⊢ o ∈ ℕ → q ∈ ℤ ≥ o + 1 ↔ q ∈ ℕ ∧ o < q
68 67 anbi1d ⊢ o ∈ ℕ → q ∈ ℤ ≥ o + 1 ∧ o · ˙ A = q · ˙ A ↔ q ∈ ℕ ∧ o < q ∧ o · ˙ A = q · ˙ A
69 anass ⊢ q ∈ ℕ ∧ o < q ∧ o · ˙ A = q · ˙ A ↔ q ∈ ℕ ∧ o < q ∧ o · ˙ A = q · ˙ A
70 68 69 bitrdi ⊢ o ∈ ℕ → q ∈ ℤ ≥ o + 1 ∧ o · ˙ A = q · ˙ A ↔ q ∈ ℕ ∧ o < q ∧ o · ˙ A = q · ˙ A
71 70 exbidv ⊢ o ∈ ℕ → ∃ q q ∈ ℤ ≥ o + 1 ∧ o · ˙ A = q · ˙ A ↔ ∃ q q ∈ ℕ ∧ o < q ∧ o · ˙ A = q · ˙ A
72 df-rex ⊢ ∃ q ∈ ℤ ≥ o + 1 o · ˙ A = q · ˙ A ↔ ∃ q q ∈ ℤ ≥ o + 1 ∧ o · ˙ A = q · ˙ A
73 df-rex ⊢ ∃ q ∈ ℕ o < q ∧ o · ˙ A = q · ˙ A ↔ ∃ q q ∈ ℕ ∧ o < q ∧ o · ˙ A = q · ˙ A
74 71 72 73 3bitr4g ⊢ o ∈ ℕ → ∃ q ∈ ℤ ≥ o + 1 o · ˙ A = q · ˙ A ↔ ∃ q ∈ ℕ o < q ∧ o · ˙ A = q · ˙ A
75 74 rexbiia ⊢ ∃ o ∈ ℕ ∃ q ∈ ℤ ≥ o + 1 o · ˙ A = q · ˙ A ↔ ∃ o ∈ ℕ ∃ q ∈ ℕ o < q ∧ o · ˙ A = q · ˙ A
76 44 75 sylibr ⊢ φ → ∃ o ∈ ℕ ∃ q ∈ ℤ ≥ o + 1 o · ˙ A = q · ˙ A
77 simplr ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o ∈ ℕ
78 77 peano2nnd ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o + 1 ∈ ℕ
79 78 nnzd ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o + 1 ∈ ℤ
80 simpr ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → p ∈ ℕ
81 77 80 nnaddcld ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o + p ∈ ℕ
82 81 nnzd ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o + p ∈ ℤ
83 1red ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → 1 ∈ ℝ
84 80 nnred ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → p ∈ ℝ
85 77 nnred ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o ∈ ℝ
86 80 nnge1d ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → 1 ≤ p
87 83 84 85 86 leadd2dd ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o + 1 ≤ o + p
88 eluz2 ⊢ o + p ∈ ℤ ≥ o + 1 ↔ o + 1 ∈ ℤ ∧ o + p ∈ ℤ ∧ o + 1 ≤ o + p
89 79 82 87 88 syl3anbrc ⊢ φ ∧ o ∈ ℕ ∧ p ∈ ℕ → o + p ∈ ℤ ≥ o + 1
90 simpr ⊢ φ ∧ o ∈ ℕ → o ∈ ℕ
91 90 nnzd ⊢ φ ∧ o ∈ ℕ → o ∈ ℤ
92 eluzp1l ⊢ o ∈ ℤ ∧ q ∈ ℤ ≥ o + 1 → o < q
93 91 92 sylan ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 → o < q
94 simplr ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 → o ∈ ℕ
95 peano2nn ⊢ o ∈ ℕ → o + 1 ∈ ℕ
96 95 adantl ⊢ φ ∧ o ∈ ℕ → o + 1 ∈ ℕ
97 eluznn ⊢ o + 1 ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 → q ∈ ℕ
98 96 97 sylan ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 → q ∈ ℕ
99 nnsub ⊢ o ∈ ℕ ∧ q ∈ ℕ → o < q ↔ q − o ∈ ℕ
100 94 98 99 syl2anc ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 → o < q ↔ q − o ∈ ℕ
101 93 100 mpbid ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 → q − o ∈ ℕ
102 eluzelcn ⊢ q ∈ ℤ ≥ o + 1 → q ∈ ℂ
103 102 ad2antlr ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 ∧ p = q − o → q ∈ ℂ
104 nncn ⊢ o ∈ ℕ → o ∈ ℂ
105 104 adantl ⊢ φ ∧ o ∈ ℕ → o ∈ ℂ
106 105 ad2antrr ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 ∧ p = q − o → o ∈ ℂ
107 simpr ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 ∧ p = q − o → p = q − o
108 103 106 107 rsubrotld ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 ∧ p = q − o → q = o + p
109 101 108 rspcedeq2vd ⊢ φ ∧ o ∈ ℕ ∧ q ∈ ℤ ≥ o + 1 → ∃ p ∈ ℕ q = o + p
110 oveq1 ⊢ q = o + p → q · ˙ A = o + p · ˙ A
111 110 eqeq2d ⊢ q = o + p → o · ˙ A = q · ˙ A ↔ o · ˙ A = o + p · ˙ A
112 111 adantl ⊢ φ ∧ o ∈ ℕ ∧ q = o + p → o · ˙ A = q · ˙ A ↔ o · ˙ A = o + p · ˙ A
113 89 109 112 rexxfrd ⊢ φ ∧ o ∈ ℕ → ∃ q ∈ ℤ ≥ o + 1 o · ˙ A = q · ˙ A ↔ ∃ p ∈ ℕ o · ˙ A = o + p · ˙ A
114 113 rexbidva ⊢ φ → ∃ o ∈ ℕ ∃ q ∈ ℤ ≥ o + 1 o · ˙ A = q · ˙ A ↔ ∃ o ∈ ℕ ∃ p ∈ ℕ o · ˙ A = o + p · ˙ A
115 76 114 mpbid ⊢ φ → ∃ o ∈ ℕ ∃ p ∈ ℕ o · ˙ A = o + p · ˙ A