Theorem fidomncyc

Description: Version of odcl2 for multiplicative groups of finite domains (that is, a finite monoid where nonzero elements are cancellable): one ( .1. ) is a multiple of any nonzero element. (Contributed by SN, 3-Jul-2025)

	Ref	Expression
Hypotheses	fidomncyc.b	$$⊢B={\mathrm{Base}}_R$$
	fidomncyc.0	$$⊢\underset{\dot{}}{0}=0_R$$
	fidomncyc.1	$$⊢\underset{\dot{}}{1}=1_R$$
	fidomncyc.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	fidomncyc.r	$$⊢\phi \to R\in \mathrm{Domn}$$
	fidomncyc.f	$$⊢\phi \to B\in \mathrm{Fin}$$
	fidomncyc.a	$$⊢\phi \to A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	fidomncyc	$$⊢\phi \to \exists n\in \mathbb{N}n\underset{\dot{}}{\times }A=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		fidomncyc.b	$$⊢B={\mathrm{Base}}_R$$
2		fidomncyc.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		fidomncyc.1	$$⊢\underset{\dot{}}{1}=1_R$$
4		fidomncyc.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
5		fidomncyc.r	$$⊢\phi \to R\in \mathrm{Domn}$$
6		fidomncyc.f	$$⊢\phi \to B\in \mathrm{Fin}$$
7		fidomncyc.a	$$⊢\phi \to A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
8		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
9	8 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
10		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
11	5 10	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
12	8	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
13	11 12	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
14		mndmgm	$$⊢{\mathrm{mulGrp}}_R\in \mathrm{Mnd}\to {\mathrm{mulGrp}}_R\in \mathrm{Mgm}$$
15	13 14	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mgm}$$
16	7	eldifad	$$⊢\phi \to A\in B$$
17	9 4 15 6 16	fimgmcyc	$$⊢\phi \to \exists o\in \mathbb{N}\exists p\in \mathbb{N}o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A$$
18		simplrr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to p\in \mathbb{N}$$
19		eqid	$$⊢{\cdot }_R={\cdot }_R$$
20	5	adantr	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to R\in \mathrm{Domn}$$
21		nnnn0	$$⊢o\in \mathbb{N}\to o\in {\mathbb{N}}_0$$
22	21	ad2antrl	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to o\in {\mathbb{N}}_0$$
23	7	adantr	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
24	1 2 4 20 22 23	domnexpgn0cl	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to o\underset{\dot{}}{\times }A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
25	24	adantr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to o\underset{\dot{}}{\times }A\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
26	15	adantr	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Mgm}$$
27		simprr	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to p\in \mathbb{N}$$
28	16	adantr	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to A\in B$$
29	9 4	mulgnncl	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mgm}\wedge p\in \mathbb{N}\wedge A\in B\right)\to p\underset{\dot{}}{\times }A\in B$$
30	26 27 28 29	syl3anc	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to p\underset{\dot{}}{\times }A\in B$$
31	30	adantr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to p\underset{\dot{}}{\times }A\in B$$
32	1 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
33	11 32	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
34	33	ad2antrr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to \underset{\dot{}}{1}\in B$$
35	5	ad2antrr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to R\in \mathrm{Domn}$$
36	11	adantr	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to R\in \mathrm{Ring}$$
37	24	eldifad	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to o\underset{\dot{}}{\times }A\in B$$
38	1 19 3 36 37	ringridmd	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to \left(o\underset{\dot{}}{\times }A\right){\cdot }_R\underset{\dot{}}{1}=o\underset{\dot{}}{\times }A$$
39	38	adantr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to \left(o\underset{\dot{}}{\times }A\right){\cdot }_R\underset{\dot{}}{1}=o\underset{\dot{}}{\times }A$$
40		simpr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A$$
41		mndsgrp	$$⊢{\mathrm{mulGrp}}_R\in \mathrm{Mnd}\to {\mathrm{mulGrp}}_R\in \mathrm{Smgrp}$$
42	13 41	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Smgrp}$$
43	42	ad2antrr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Smgrp}$$
44		simplrl	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to o\in \mathbb{N}$$
45	28	adantr	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to A\in B$$
46	8 19	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
47	9 4 46	mulgnndir	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Smgrp}\wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\wedge A\in B\right)\right)\to \left(o+p\right)\underset{\dot{}}{\times }A=\left(o\underset{\dot{}}{\times }A\right){\cdot }_R\left(p\underset{\dot{}}{\times }A\right)$$
48	43 44 18 45 47	syl13anc	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to \left(o+p\right)\underset{\dot{}}{\times }A=\left(o\underset{\dot{}}{\times }A\right){\cdot }_R\left(p\underset{\dot{}}{\times }A\right)$$
49	39 40 48	3eqtrrd	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to \left(o\underset{\dot{}}{\times }A\right){\cdot }_R\left(p\underset{\dot{}}{\times }A\right)=\left(o\underset{\dot{}}{\times }A\right){\cdot }_R\underset{\dot{}}{1}$$
50	1 2 19 25 31 34 35 49	domnlcan	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to p\underset{\dot{}}{\times }A=\underset{\dot{}}{1}$$
51		oveq1	$$⊢n=p\to n\underset{\dot{}}{\times }A=p\underset{\dot{}}{\times }A$$
52	51	eqeq1d	$$⊢n=p\to \left(n\underset{\dot{}}{\times }A=\underset{\dot{}}{1}\leftrightarrow p\underset{\dot{}}{\times }A=\underset{\dot{}}{1}\right)$$
53	52	rspcev	$$⊢\left(p\in \mathbb{N}\wedge p\underset{\dot{}}{\times }A=\underset{\dot{}}{1}\right)\to \exists n\in \mathbb{N}n\underset{\dot{}}{\times }A=\underset{\dot{}}{1}$$
54	18 50 53	syl2anc	$$⊢\left(\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\wedge o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\right)\to \exists n\in \mathbb{N}n\underset{\dot{}}{\times }A=\underset{\dot{}}{1}$$
55	54	ex	$$⊢\left(\phi \wedge \left(o\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to \left(o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\to \exists n\in \mathbb{N}n\underset{\dot{}}{\times }A=\underset{\dot{}}{1}\right)$$
56	55	rexlimdvva	$$⊢\phi \to \left(\exists o\in \mathbb{N}\exists p\in \mathbb{N}o\underset{\dot{}}{\times }A=\left(o+p\right)\underset{\dot{}}{\times }A\to \exists n\in \mathbb{N}n\underset{\dot{}}{\times }A=\underset{\dot{}}{1}\right)$$
57	17 56	mpd	$$⊢\phi \to \exists n\in \mathbb{N}n\underset{\dot{}}{\times }A=\underset{\dot{}}{1}$$