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	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	fimgmcyc.s	$⊢ φ \to M \in Mgm$
	fimgmcyc.f	$⊢ φ \to B \in Fin$
	fimgmcyc.a	$⊢ φ \to A \in B$
Assertion	fimgmcyc	$⊢ φ \to \exists o \in ℕ \exists p \in ℕ o \underset{˙}{\cdot} A = (o + p) \underset{˙}{\cdot} A$

Proof

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

Metamath Proof Explorer

Theorem fimgmcyc

Proof