Metamath Proof Explorer

Theorem aks6d1c1rh

Description: Claim 1 of AKS primality proof with collapsed definitions since their ease of use is no longer needed. (Contributed by metakunt, 1-May-2025)

Ref Expression
Hypotheses aks6d1c1rh.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
aks6d1c1rh.2 
|- P = ( chr ` K )
aks6d1c1rh.3 
|- ( ph -> K e. Field )
aks6d1c1rh.4 
|- ( ph -> P e. Prime )
aks6d1c1rh.5 
|- ( ph -> R e. NN )
aks6d1c1rh.6 
|- ( ph -> N e. NN )
aks6d1c1rh.7 
|- ( ph -> P || N )
aks6d1c1rh.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c1rh.9 
|- ( ph -> F : ( 0 ... A ) --> NN0 )
aks6d1c1rh.10 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c1rh.11 
|- ( ph -> A e. NN0 )
aks6d1c1rh.12 
|- ( ph -> U e. NN0 )
aks6d1c1rh.13 
|- ( ph -> L e. NN0 )
aks6d1c1rh.14 
|- E = ( ( P ^ U ) x. ( ( N / P ) ^ L ) )
aks6d1c1rh.15 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c1rh.16 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
Assertion aks6d1c1rh 
|- ( ph -> E .~ ( G ` F ) )

Proof

Step Hyp Ref Expression
1 aks6d1c1rh.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2 aks6d1c1rh.2 
 |-  P = ( chr ` K )
3 aks6d1c1rh.3 
 |-  ( ph -> K e. Field )
4 aks6d1c1rh.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c1rh.5 
 |-  ( ph -> R e. NN )
6 aks6d1c1rh.6 
 |-  ( ph -> N e. NN )
7 aks6d1c1rh.7 
 |-  ( ph -> P || N )
8 aks6d1c1rh.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c1rh.9 
 |-  ( ph -> F : ( 0 ... A ) --> NN0 )
10 aks6d1c1rh.10 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
11 aks6d1c1rh.11 
 |-  ( ph -> A e. NN0 )
12 aks6d1c1rh.12 
 |-  ( ph -> U e. NN0 )
13 aks6d1c1rh.13 
 |-  ( ph -> L e. NN0 )
14 aks6d1c1rh.14 
 |-  E = ( ( P ^ U ) x. ( ( N / P ) ^ L ) )
15 aks6d1c1rh.15 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
16 aks6d1c1rh.16 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
17 nfv 
 |-  F/ z ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) )
18 nfv 
 |-  F/ y ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` z ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) z ) )
19 fveq2 
 |-  ( y = z -> ( ( ( eval1 ` K ) ` f ) ` y ) = ( ( ( eval1 ` K ) ` f ) ` z ) )
20 19 oveq2d 
 |-  ( y = z -> ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` z ) ) )
21 oveq2 
 |-  ( y = z -> ( e ( .g ` ( mulGrp ` K ) ) y ) = ( e ( .g ` ( mulGrp ` K ) ) z ) )
22 21 fveq2d 
 |-  ( y = z -> ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) z ) ) )
23 20 22 eqeq12d 
 |-  ( y = z -> ( ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) <-> ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` z ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) z ) ) ) )
24 17 18 23 cbvralw 
 |-  ( A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) <-> A. z e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` z ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) z ) ) )
25 24 3anbi3i 
 |-  ( ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) <-> ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. z e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` z ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) z ) ) ) )
26 25 opabbii 
 |-  { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) } = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. z e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` z ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) z ) ) ) }
27 1 26 eqtri 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. z e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` z ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) z ) ) ) }
28 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
29 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
30 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
31 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
32 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
33 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
34 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
35 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
36 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
37 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
38 27 28 29 30 31 32 33 34 35 2 36 37 3 4 5 6 7 8 9 10 11 12 13 14 15 16 aks6d1c1 
 |-  ( ph -> E .~ ( G ` F ) )