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 
|- B = ( Base ` R )
fidomncyc.0 
|- .0. = ( 0g ` R )
fidomncyc.1 
|- .1. = ( 1r ` R )
fidomncyc.e 
|- .^ = ( .g ` ( mulGrp ` R ) )
fidomncyc.r 
|- ( ph -> R e. Domn )
fidomncyc.f 
|- ( ph -> B e. Fin )
fidomncyc.a 
|- ( ph -> A e. ( B \ { .0. } ) )
Assertion fidomncyc 
|- ( ph -> E. n e. NN ( n .^ A ) = .1. )

Proof

Step Hyp Ref Expression
1 fidomncyc.b 
 |-  B = ( Base ` R )
2 fidomncyc.0 
 |-  .0. = ( 0g ` R )
3 fidomncyc.1 
 |-  .1. = ( 1r ` R )
4 fidomncyc.e 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
5 fidomncyc.r 
 |-  ( ph -> R e. Domn )
6 fidomncyc.f 
 |-  ( ph -> B e. Fin )
7 fidomncyc.a 
 |-  ( ph -> A e. ( B \ { .0. } ) )
8 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
9 8 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
10 domnring 
 |-  ( R e. Domn -> R e. Ring )
11 5 10 syl 
 |-  ( ph -> R e. Ring )
12 8 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
13 11 12 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
14 mndmgm 
 |-  ( ( mulGrp ` R ) e. Mnd -> ( mulGrp ` R ) e. Mgm )
15 13 14 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mgm )
16 7 eldifad 
 |-  ( ph -> A e. B )
17 9 4 15 6 16 fimgmcyc 
 |-  ( ph -> E. o e. NN E. p e. NN ( o .^ A ) = ( ( o + p ) .^ A ) )
18 simplrr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> p e. NN )
19 eqid 
 |-  ( .r ` R ) = ( .r ` R )
20 5 adantr 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> R e. Domn )
21 nnnn0 
 |-  ( o e. NN -> o e. NN0 )
22 21 ad2antrl 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> o e. NN0 )
23 7 adantr 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> A e. ( B \ { .0. } ) )
24 1 2 4 20 22 23 domnexpgn0cl 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> ( o .^ A ) e. ( B \ { .0. } ) )
25 24 adantr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( o .^ A ) e. ( B \ { .0. } ) )
26 15 adantr 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> ( mulGrp ` R ) e. Mgm )
27 simprr 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> p e. NN )
28 16 adantr 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> A e. B )
29 9 4 mulgnncl 
 |-  ( ( ( mulGrp ` R ) e. Mgm /\ p e. NN /\ A e. B ) -> ( p .^ A ) e. B )
30 26 27 28 29 syl3anc 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> ( p .^ A ) e. B )
31 30 adantr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( p .^ A ) e. B )
32 1 3 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
33 11 32 syl 
 |-  ( ph -> .1. e. B )
34 33 ad2antrr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> .1. e. B )
35 5 ad2antrr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> R e. Domn )
36 11 adantr 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> R e. Ring )
37 24 eldifad 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> ( o .^ A ) e. B )
38 1 19 3 36 37 ringridmd 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> ( ( o .^ A ) ( .r ` R ) .1. ) = ( o .^ A ) )
39 38 adantr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( ( o .^ A ) ( .r ` R ) .1. ) = ( o .^ A ) )
40 simpr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( o .^ A ) = ( ( o + p ) .^ A ) )
41 mndsgrp 
 |-  ( ( mulGrp ` R ) e. Mnd -> ( mulGrp ` R ) e. Smgrp )
42 13 41 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Smgrp )
43 42 ad2antrr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( mulGrp ` R ) e. Smgrp )
44 simplrl 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> o e. NN )
45 28 adantr 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> A e. B )
46 8 19 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
47 9 4 46 mulgnndir 
 |-  ( ( ( mulGrp ` R ) e. Smgrp /\ ( o e. NN /\ p e. NN /\ A e. B ) ) -> ( ( o + p ) .^ A ) = ( ( o .^ A ) ( .r ` R ) ( p .^ A ) ) )
48 43 44 18 45 47 syl13anc 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( ( o + p ) .^ A ) = ( ( o .^ A ) ( .r ` R ) ( p .^ A ) ) )
49 39 40 48 3eqtrrd 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( ( o .^ A ) ( .r ` R ) ( p .^ A ) ) = ( ( o .^ A ) ( .r ` R ) .1. ) )
50 1 2 19 25 31 34 35 49 domnlcan 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> ( p .^ A ) = .1. )
51 oveq1 
 |-  ( n = p -> ( n .^ A ) = ( p .^ A ) )
52 51 eqeq1d 
 |-  ( n = p -> ( ( n .^ A ) = .1. <-> ( p .^ A ) = .1. ) )
53 52 rspcev 
 |-  ( ( p e. NN /\ ( p .^ A ) = .1. ) -> E. n e. NN ( n .^ A ) = .1. )
54 18 50 53 syl2anc 
 |-  ( ( ( ph /\ ( o e. NN /\ p e. NN ) ) /\ ( o .^ A ) = ( ( o + p ) .^ A ) ) -> E. n e. NN ( n .^ A ) = .1. )
55 54 ex 
 |-  ( ( ph /\ ( o e. NN /\ p e. NN ) ) -> ( ( o .^ A ) = ( ( o + p ) .^ A ) -> E. n e. NN ( n .^ A ) = .1. ) )
56 55 rexlimdvva 
 |-  ( ph -> ( E. o e. NN E. p e. NN ( o .^ A ) = ( ( o + p ) .^ A ) -> E. n e. NN ( n .^ A ) = .1. ) )
57 17 56 mpd 
 |-  ( ph -> E. n e. NN ( n .^ A ) = .1. )