Metamath Proof Explorer

Theorem aks5lem4a

Description: Lemma for AKS section 5, reduce hypotheses. (Contributed by metakunt, 17-Jun-2025)

Ref Expression
Hypotheses aks5lema.1 
|- ( ph -> K e. Field )
aks5lema.2 
|- P = ( chr ` K )
aks5lema.3 
|- ( ph -> ( P e. Prime /\ N e. NN /\ P || N ) )
aks5lema.9 
|- B = ( S /s ( S ~QG L ) )
aks5lema.10 
|- L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } )
aks5lema.11 
|- ( ph -> R e. NN )
aks5lema.14 
|- .~ = { <. 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 ) ) ) }
aks5lema.15 
|- S = ( Poly1 ` ( Z/nZ ` N ) )
aks5lem4a.7 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks5lem4a.12 
|- ( ph -> A e. ZZ )
aks5lem4a.13 
|- ( ph -> [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( S ~QG L ) )
Assertion aks5lem4a 
|- ( ph -> ( N ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) )

Proof

Step Hyp Ref Expression
1 aks5lema.1 
 |-  ( ph -> K e. Field )
2 aks5lema.2 
 |-  P = ( chr ` K )
3 aks5lema.3 
 |-  ( ph -> ( P e. Prime /\ N e. NN /\ P || N ) )
4 aks5lema.9 
 |-  B = ( S /s ( S ~QG L ) )
5 aks5lema.10 
 |-  L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } )
6 aks5lema.11 
 |-  ( ph -> R e. NN )
7 aks5lema.14 
 |-  .~ = { <. 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 ) ) ) }
8 aks5lema.15 
 |-  S = ( Poly1 ` ( Z/nZ ` N ) )
9 aks5lem4a.7 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
10 aks5lem4a.12 
 |-  ( ph -> A e. ZZ )
11 aks5lem4a.13 
 |-  ( ph -> [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( S ~QG L ) )
12 eqid 
 |-  ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) = ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) )
13 eqid 
 |-  ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) = ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) )
14 eqid 
 |-  ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) = ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) )
15 nfcv 
 |-  F/_ d U. ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " e )
16 nfcv 
 |-  F/_ e U. ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " d )
17 imaeq2 
 |-  ( e = d -> ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " e ) = ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " d ) )
18 17 unieqd 
 |-  ( e = d -> U. ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " e ) = U. ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " d ) )
19 15 16 18 cbvmpt 
 |-  ( e e. ( Base ` B ) |-> U. ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " e ) ) = ( d e. ( Base ` B ) |-> U. ( ( ( c e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` c ) ` M ) ) o. ( b e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( ( a e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " a ) ) o. b ) ) ) " d ) )
20 1 2 3 4 5 6 7 8 12 13 14 9 19 10 11 aks5lem3a 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) )