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 
|- .x. = ( .g ` M )
fimgmcyc.s 
|- ( ph -> M e. Mgm )
fimgmcyc.f 
|- ( ph -> B e. Fin )
fimgmcyc.a 
|- ( ph -> A e. B )
Assertion fimgmcyc 
|- ( ph -> E. o e. NN E. p e. NN ( o .x. A ) = ( ( o + p ) .x. A ) )

Proof

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