This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
fidomncyc.0 ⊢ 0 = ( 0g ‘ 𝑅 )
fidomncyc.1 ⊢ 1 = ( 1r ‘ 𝑅 )
fidomncyc.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
fidomncyc.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
fidomncyc.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
fidomncyc.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ { 0 } ) )
Assertion fidomncyc ( 𝜑 → ∃ 𝑛 ∈ ℕ ( 𝑛 ↑ 𝐴 ) = 1 )

Proof

Step Hyp Ref Expression
1 fidomncyc.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 fidomncyc.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 fidomncyc.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 fidomncyc.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
5 fidomncyc.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
6 fidomncyc.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
7 fidomncyc.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ { 0 } ) )
8 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
9 8 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
10 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
11 5 10 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
12 8 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
13 11 12 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
14 mndmgm ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
15 13 14 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
16 7 eldifad ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
17 9 4 15 6 16 fimgmcyc ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) )
18 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → 𝑝 ∈ ℕ )
19 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
20 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → 𝑅 ∈ Domn )
21 nnnn0 ⊢ ( 𝑜 ∈ ℕ → 𝑜 ∈ ℕ0 )
22 21 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → 𝑜 ∈ ℕ0 )
23 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → 𝐴 ∈ ( 𝐵 ∖ { 0 } ) )
24 1 2 4 20 22 23 domnexpgn0cl ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( 𝑜 ↑ 𝐴 ) ∈ ( 𝐵 ∖ { 0 } ) )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( 𝑜 ↑ 𝐴 ) ∈ ( 𝐵 ∖ { 0 } ) )
26 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
27 simprr ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → 𝑝 ∈ ℕ )
28 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → 𝐴 ∈ 𝐵 )
29 9 4 mulgnncl ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mgm ∧ 𝑝 ∈ ℕ ∧ 𝐴 ∈ 𝐵 ) → ( 𝑝 ↑ 𝐴 ) ∈ 𝐵 )
30 26 27 28 29 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( 𝑝 ↑ 𝐴 ) ∈ 𝐵 )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( 𝑝 ↑ 𝐴 ) ∈ 𝐵 )
32 1 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
33 11 32 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → 1 ∈ 𝐵 )
35 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → 𝑅 ∈ Domn )
36 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → 𝑅 ∈ Ring )
37 24 eldifad ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( 𝑜 ↑ 𝐴 ) ∈ 𝐵 )
38 1 19 3 36 37 ringridmd ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( ( 𝑜 ↑ 𝐴 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑜 ↑ 𝐴 ) )
39 38 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( ( 𝑜 ↑ 𝐴 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑜 ↑ 𝐴 ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) )
41 mndsgrp ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( mulGrp ‘ 𝑅 ) ∈ Smgrp )
42 13 41 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Smgrp )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Smgrp )
44 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → 𝑜 ∈ ℕ )
45 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → 𝐴 ∈ 𝐵 )
46 8 19 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
47 9 4 46 mulgnndir ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Smgrp ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) = ( ( 𝑜 ↑ 𝐴 ) ( .r ‘ 𝑅 ) ( 𝑝 ↑ 𝐴 ) ) )
48 43 44 18 45 47 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) = ( ( 𝑜 ↑ 𝐴 ) ( .r ‘ 𝑅 ) ( 𝑝 ↑ 𝐴 ) ) )
49 39 40 48 3eqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( ( 𝑜 ↑ 𝐴 ) ( .r ‘ 𝑅 ) ( 𝑝 ↑ 𝐴 ) ) = ( ( 𝑜 ↑ 𝐴 ) ( .r ‘ 𝑅 ) 1 ) )
50 1 2 19 25 31 34 35 49 domnlcan ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ( 𝑝 ↑ 𝐴 ) = 1 )
51 oveq1 ⊢ ( 𝑛 = 𝑝 → ( 𝑛 ↑ 𝐴 ) = ( 𝑝 ↑ 𝐴 ) )
52 51 eqeq1d ⊢ ( 𝑛 = 𝑝 → ( ( 𝑛 ↑ 𝐴 ) = 1 ↔ ( 𝑝 ↑ 𝐴 ) = 1 ) )
53 52 rspcev ⊢ ( ( 𝑝 ∈ ℕ ∧ ( 𝑝 ↑ 𝐴 ) = 1 ) → ∃ 𝑛 ∈ ℕ ( 𝑛 ↑ 𝐴 ) = 1 )
54 18 50 53 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) ∧ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( 𝑛 ↑ 𝐴 ) = 1 )
55 54 ex ⊢ ( ( 𝜑 ∧ ( 𝑜 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) → ∃ 𝑛 ∈ ℕ ( 𝑛 ↑ 𝐴 ) = 1 ) )
56 55 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑜 ↑ 𝐴 ) = ( ( 𝑜 + 𝑝 ) ↑ 𝐴 ) → ∃ 𝑛 ∈ ℕ ( 𝑛 ↑ 𝐴 ) = 1 ) )
57 17 56 mpd ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ( 𝑛 ↑ 𝐴 ) = 1 )