Metamath Proof Explorer

Theorem aks6d1c1p7

Description: X is introspective to all positive integers. (Contributed by metakunt, 30-Apr-2025)

Ref Expression
Hypotheses aks6d1c1p7.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
aks6d1c1p7.2 
|- S = ( Poly1 ` K )
aks6d1c1p7.3 
|- B = ( Base ` S )
aks6d1c1p7.4 
|- X = ( var1 ` K )
aks6d1c1p7.5 
|- V = ( mulGrp ` K )
aks6d1c1p7.6 
|- .^ = ( .g ` V )
aks6d1c1p7.7 
|- P = ( chr ` K )
aks6d1c1p7.8 
|- O = ( eval1 ` K )
aks6d1c1p7.9 
|- ( ph -> K e. Field )
aks6d1c1p7.10 
|- ( ph -> P e. Prime )
aks6d1c1p7.11 
|- ( ph -> R e. NN )
aks6d1c1p7.12 
|- ( ph -> N e. NN )
aks6d1c1p7.13 
|- ( ph -> P || N )
aks6d1c1p7.14 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c1p7.15 
|- ( ph -> L e. NN )
Assertion aks6d1c1p7 
|- ( ph -> L .~ X )

Proof

Step Hyp Ref Expression
1 aks6d1c1p7.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1p7.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1p7.3 
 |-  B = ( Base ` S )
4 aks6d1c1p7.4 
 |-  X = ( var1 ` K )
5 aks6d1c1p7.5 
 |-  V = ( mulGrp ` K )
6 aks6d1c1p7.6 
 |-  .^ = ( .g ` V )
7 aks6d1c1p7.7 
 |-  P = ( chr ` K )
8 aks6d1c1p7.8 
 |-  O = ( eval1 ` K )
9 aks6d1c1p7.9 
 |-  ( ph -> K e. Field )
10 aks6d1c1p7.10 
 |-  ( ph -> P e. Prime )
11 aks6d1c1p7.11 
 |-  ( ph -> R e. NN )
12 aks6d1c1p7.12 
 |-  ( ph -> N e. NN )
13 aks6d1c1p7.13 
 |-  ( ph -> P || N )
14 aks6d1c1p7.14 
 |-  ( ph -> ( N gcd R ) = 1 )
15 aks6d1c1p7.15 
 |-  ( ph -> L e. NN )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 9 fldcrngd 
 |-  ( ph -> K e. CRing )
18 17 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> K e. CRing )
19 5 crngmgp 
 |-  ( K e. CRing -> V e. CMnd )
20 17 19 syl 
 |-  ( ph -> V e. CMnd )
21 11 nnnn0d 
 |-  ( ph -> R e. NN0 )
22 20 21 6 isprimroot 
 |-  ( ph -> ( y e. ( V PrimRoots R ) <-> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) ) )
23 22 biimpd 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) ) )
24 23 imp 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) )
25 24 simp1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
26 5 16 mgpbas 
 |-  ( Base ` K ) = ( Base ` V )
27 25 26 eleqtrrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` K ) )
28 8 4 16 2 3 18 27 evl1vard 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( X e. B /\ ( ( O ` X ) ` y ) = y ) )
29 28 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` X ) ` y ) = y )
30 29 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( L .^ ( ( O ` X ) ` y ) ) = ( L .^ y ) )
31 20 cmnmndd 
 |-  ( ph -> V e. Mnd )
32 31 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> V e. Mnd )
33 15 nnnn0d 
 |-  ( ph -> L e. NN0 )
34 33 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> L e. NN0 )
35 27 26 eleqtrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
36 eqid 
 |-  ( Base ` V ) = ( Base ` V )
37 36 6 mulgnn0cl 
 |-  ( ( V e. Mnd /\ L e. NN0 /\ y e. ( Base ` V ) ) -> ( L .^ y ) e. ( Base ` V ) )
38 32 34 35 37 syl3anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( L .^ y ) e. ( Base ` V ) )
39 38 26 eleqtrrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( L .^ y ) e. ( Base ` K ) )
40 8 4 16 2 3 18 39 evl1vard 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( X e. B /\ ( ( O ` X ) ` ( L .^ y ) ) = ( L .^ y ) ) )
41 40 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` X ) ` ( L .^ y ) ) = ( L .^ y ) )
42 eqidd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( L .^ y ) = ( L .^ y ) )
43 41 42 eqtr2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( L .^ y ) = ( ( O ` X ) ` ( L .^ y ) ) )
44 30 43 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( L .^ ( ( O ` X ) ` y ) ) = ( ( O ` X ) ` ( L .^ y ) ) )
45 44 ralrimiva 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( L .^ ( ( O ` X ) ` y ) ) = ( ( O ` X ) ` ( L .^ y ) ) )
46 crngring 
 |-  ( K e. CRing -> K e. Ring )
47 17 46 syl 
 |-  ( ph -> K e. Ring )
48 eqid 
 |-  ( Base ` S ) = ( Base ` S )
49 4 2 48 vr1cl 
 |-  ( K e. Ring -> X e. ( Base ` S ) )
50 47 49 syl 
 |-  ( ph -> X e. ( Base ` S ) )
51 50 3 eleqtrrdi 
 |-  ( ph -> X e. B )
52 1 51 15 aks6d1c1p1 
 |-  ( ph -> ( L .~ X <-> A. y e. ( V PrimRoots R ) ( L .^ ( ( O ` X ) ` y ) ) = ( ( O ` X ) ` ( L .^ y ) ) ) )
53 45 52 mpbird 
 |-  ( ph -> L .~ X )