Metamath Proof Explorer

Theorem aks5lem5a

Description: Lemma for AKS, section 5, connect to Theorem 6.1. (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 ) )
aks5lem5a.13 
|- ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
Assertion aks5lem5a 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )

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 aks5lem5a.13 
 |-  ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
10 1 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) /\ y e. ( ( mulGrp ` K ) PrimRoots R ) ) -> K e. Field )
11 3 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) /\ y e. ( ( mulGrp ` K ) PrimRoots R ) ) -> ( P e. Prime /\ N e. NN /\ P || N ) )
12 6 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) /\ y e. ( ( mulGrp ` K ) PrimRoots R ) ) -> R e. NN )
13 simpr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) /\ y e. ( ( mulGrp ` K ) PrimRoots R ) ) -> y e. ( ( mulGrp ` K ) PrimRoots R ) )
14 elfzelz 
 |-  ( a e. ( 1 ... A ) -> a e. ZZ )
15 14 adantl 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> a e. ZZ )
16 15 adantr 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> a e. ZZ )
17 16 adantr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) /\ y e. ( ( mulGrp ` K ) PrimRoots R ) ) -> a e. ZZ )
18 eqid 
 |-  ( algSc ` S ) = ( algSc ` S )
19 eqid 
 |-  ( ZRHom ` S ) = ( ZRHom ` S )
20 eqid 
 |-  ( ZRHom ` ( Z/nZ ` N ) ) = ( ZRHom ` ( Z/nZ ` N ) )
21 3 simp2d 
 |-  ( ph -> N e. NN )
22 21 adantr 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> N e. NN )
23 22 nnnn0d 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> N e. NN0 )
24 eqid 
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
25 24 zncrng 
 |-  ( N e. NN0 -> ( Z/nZ ` N ) e. CRing )
26 23 25 syl 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( Z/nZ ` N ) e. CRing )
27 8 18 19 20 26 15 ply1asclzrhval 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` a ) ) = ( ( ZRHom ` S ) ` a ) )
28 27 oveq2d 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` a ) ) ) = ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) )
29 28 oveq2d 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` a ) ) ) ) = ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) )
30 29 eceq1d 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> [ ( 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 ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) )
31 30 adantr 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( 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 ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) )
32 simpr 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
33 27 eqcomd 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( ZRHom ` S ) ` a ) = ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` a ) ) )
34 33 oveq2d 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) = ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` a ) ) ) )
35 34 eceq1d 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` a ) ) ) ] ( S ~QG L ) )
36 35 adantr 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` a ) ) ) ] ( S ~QG L ) )
37 31 32 36 3eqtrd 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( 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 ) )
38 37 adantr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) /\ y e. ( ( mulGrp ` K ) PrimRoots R ) ) -> [ ( 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 ) )
39 10 2 11 4 5 12 7 8 13 17 38 aks5lem4a 
 |-  ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) /\ y e. ( ( mulGrp ` K ) PrimRoots R ) ) -> ( N ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) y ) ) )
40 39 ralrimiva 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( N ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) y ) ) )
41 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
42 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
43 eqid 
 |-  ( ZRHom ` ( Poly1 ` K ) ) = ( ZRHom ` ( Poly1 ` K ) )
44 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
45 1 fldcrngd 
 |-  ( ph -> K e. CRing )
46 45 adantr 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> K e. CRing )
47 41 42 43 44 46 15 ply1asclzrhval 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) = ( ( ZRHom ` ( Poly1 ` K ) ) ` a ) )
48 47 oveq2d 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) = ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` a ) ) )
49 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
50 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
51 41 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
52 45 51 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
53 52 adantr 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( Poly1 ` K ) e. CRing )
54 crngring 
 |-  ( ( Poly1 ` K ) e. CRing -> ( Poly1 ` K ) e. Ring )
55 53 54 syl 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( Poly1 ` K ) e. Ring )
56 55 ringgrpd 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( Poly1 ` K ) e. Grp )
57 46 crngringd 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> K e. Ring )
58 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
59 58 41 49 vr1cl 
 |-  ( K e. Ring -> ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) )
60 57 59 syl 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) )
61 43 zrhrhm 
 |-  ( ( Poly1 ` K ) e. Ring -> ( ZRHom ` ( Poly1 ` K ) ) e. ( ZZring RingHom ( Poly1 ` K ) ) )
62 55 61 syl 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ZRHom ` ( Poly1 ` K ) ) e. ( ZZring RingHom ( Poly1 ` K ) ) )
63 zringbas 
 |-  ZZ = ( Base ` ZZring )
64 63 49 rhmf 
 |-  ( ( ZRHom ` ( Poly1 ` K ) ) e. ( ZZring RingHom ( Poly1 ` K ) ) -> ( ZRHom ` ( Poly1 ` K ) ) : ZZ --> ( Base ` ( Poly1 ` K ) ) )
65 62 64 syl 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ZRHom ` ( Poly1 ` K ) ) : ZZ --> ( Base ` ( Poly1 ` K ) ) )
66 65 15 ffvelcdmd 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( ZRHom ` ( Poly1 ` K ) ) ` a ) e. ( Base ` ( Poly1 ` K ) ) )
67 49 50 56 60 66 grpcld 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` a ) ) e. ( Base ` ( Poly1 ` K ) ) )
68 48 67 eqeltrd 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
69 68 adantr 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
70 22 adantr 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> N e. NN )
71 7 69 70 aks6d1c1p1 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) <-> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( N ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) y ) ) ) )
72 40 71 mpbird 
 |-  ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
73 72 ex 
 |-  ( ( ph /\ a e. ( 1 ... A ) ) -> ( [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) -> N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) )
74 73 ralimdva 
 |-  ( ph -> ( A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) ) )
75 9 74 mpd 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )