Metamath Proof Explorer

Theorem aks5lem3a

Description: Lemma for AKS section 5. (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 ) )
aks5lem3a.4 
|- F = ( p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( G o. p ) )
aks5lem3a.5 
|- G = ( q e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " q ) )
aks5lem3a.6 
|- H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) )
aks5lem3a.7 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks5lem3a.8 
|- I = ( s e. ( Base ` B ) |-> U. ( ( H o. F ) " s ) )
aks5lem3a.12 
|- ( ph -> A e. ZZ )
aks5lem3a.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 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 ) ) )

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 aks5lem3a.4 
 |-  F = ( p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( G o. p ) )
10 aks5lem3a.5 
 |-  G = ( q e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " q ) )
11 aks5lem3a.6 
 |-  H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) )
12 aks5lem3a.7 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
13 aks5lem3a.8 
 |-  I = ( s e. ( Base ` B ) |-> U. ( ( H o. F ) " s ) )
14 aks5lem3a.12 
 |-  ( ph -> A e. ZZ )
15 aks5lem3a.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 ) )
16 1 fldcrngd 
 |-  ( ph -> K e. CRing )
17 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
18 17 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
19 16 18 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
20 6 nnnn0d 
 |-  ( ph -> R e. NN0 )
21 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
22 19 20 21 isprimroot 
 |-  ( ph -> ( M e. ( ( mulGrp ` K ) PrimRoots R ) <-> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. d e. NN0 ( ( d ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || d ) ) ) )
23 12 22 mpbid 
 |-  ( ph -> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. d e. NN0 ( ( d ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || d ) ) )
24 23 simp1d 
 |-  ( ph -> M e. ( Base ` ( mulGrp ` K ) ) )
25 eqid 
 |-  ( Base ` K ) = ( Base ` K )
26 17 25 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
27 26 eqcomi 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` K )
28 24 27 eleqtrdi 
 |-  ( ph -> M e. ( Base ` K ) )
29 1 2 3 9 10 11 28 aks5lem1 
 |-  ( ph -> ( H o. F ) e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom K ) )
30 eqid 
 |-  ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) )
31 30 17 rhmmhm 
 |-  ( ( H o. F ) e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom K ) -> ( H o. F ) e. ( ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) MndHom ( mulGrp ` K ) ) )
32 29 31 syl 
 |-  ( ph -> ( H o. F ) e. ( ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) MndHom ( mulGrp ` K ) ) )
33 3 simp2d 
 |-  ( ph -> N e. NN )
34 33 nnnn0d 
 |-  ( ph -> N e. NN0 )
35 eqid 
 |-  ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) )
36 eqid 
 |-  ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) )
37 eqid 
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
38 37 zncrng 
 |-  ( N e. NN0 -> ( Z/nZ ` N ) e. CRing )
39 34 38 syl 
 |-  ( ph -> ( Z/nZ ` N ) e. CRing )
40 eqid 
 |-  ( Poly1 ` ( Z/nZ ` N ) ) = ( Poly1 ` ( Z/nZ ` N ) )
41 40 ply1crng 
 |-  ( ( Z/nZ ` N ) e. CRing -> ( Poly1 ` ( Z/nZ ` N ) ) e. CRing )
42 39 41 syl 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. CRing )
43 42 crngringd 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. Ring )
44 ringgrp 
 |-  ( ( Poly1 ` ( Z/nZ ` N ) ) e. Ring -> ( Poly1 ` ( Z/nZ ` N ) ) e. Grp )
45 43 44 syl 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. Grp )
46 39 crngringd 
 |-  ( ph -> ( Z/nZ ` N ) e. Ring )
47 eqid 
 |-  ( var1 ` ( Z/nZ ` N ) ) = ( var1 ` ( Z/nZ ` N ) )
48 47 40 35 vr1cl 
 |-  ( ( Z/nZ ` N ) e. Ring -> ( var1 ` ( Z/nZ ` N ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
49 46 48 syl 
 |-  ( ph -> ( var1 ` ( Z/nZ ` N ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
50 eqid 
 |-  ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) )
51 eqid 
 |-  ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) )
52 eqid 
 |-  ( ZRHom ` ( Z/nZ ` N ) ) = ( ZRHom ` ( Z/nZ ` N ) )
53 40 50 51 52 39 14 ply1asclzrhval 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) = ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) )
54 51 zrhrhm 
 |-  ( ( Poly1 ` ( Z/nZ ` N ) ) e. Ring -> ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. ( ZZring RingHom ( Poly1 ` ( Z/nZ ` N ) ) ) )
55 zringbas 
 |-  ZZ = ( Base ` ZZring )
56 55 35 rhmf 
 |-  ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. ( ZZring RingHom ( Poly1 ` ( Z/nZ ` N ) ) ) -> ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) : ZZ --> ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
57 54 56 syl 
 |-  ( ( Poly1 ` ( Z/nZ ` N ) ) e. Ring -> ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) : ZZ --> ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
58 43 57 syl 
 |-  ( ph -> ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) : ZZ --> ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
59 58 14 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
60 53 59 eqeltrd 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
61 35 36 45 49 60 grpcld 
 |-  ( ph -> ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
62 30 35 mgpbas 
 |-  ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
63 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
64 62 63 21 mhmmulg 
 |-  ( ( ( H o. F ) e. ( ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) MndHom ( mulGrp ` K ) ) /\ N e. NN0 /\ ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( N ( .g ` ( mulGrp ` K ) ) ( ( H o. F ) ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
65 32 34 61 64 syl3anc 
 |-  ( ph -> ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( N ( .g ` ( mulGrp ` K ) ) ( ( H o. F ) ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
66 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
67 16 crngringd 
 |-  ( ph -> K e. Ring )
68 2 eqcomi 
 |-  ( chr ` K ) = P
69 3 simp1d 
 |-  ( ph -> P e. Prime )
70 prmnn 
 |-  ( P e. Prime -> P e. NN )
71 69 70 syl 
 |-  ( ph -> P e. NN )
72 71 nnzd 
 |-  ( ph -> P e. ZZ )
73 68 72 eqeltrid 
 |-  ( ph -> ( chr ` K ) e. ZZ )
74 68 a1i 
 |-  ( ph -> ( chr ` K ) = P )
75 3 simp3d 
 |-  ( ph -> P || N )
76 74 75 eqbrtrd 
 |-  ( ph -> ( chr ` K ) || N )
77 67 33 73 76 37 10 zndvdchrrhm 
 |-  ( ph -> G e. ( ( Z/nZ ` N ) RingHom K ) )
78 40 66 35 9 77 rhmply1 
 |-  ( ph -> F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) )
79 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
80 35 79 rhmf 
 |-  ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) -> F : ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) --> ( Base ` ( Poly1 ` K ) ) )
81 78 80 syl 
 |-  ( ph -> F : ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) --> ( Base ` ( Poly1 ` K ) ) )
82 81 61 fvco3d 
 |-  ( ph -> ( ( H o. F ) ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( H ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
83 11 a1i 
 |-  ( ph -> H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) ) )
84 simpr 
 |-  ( ( ph /\ r = ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) -> r = ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
85 84 fveq2d 
 |-  ( ( ph /\ r = ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) -> ( ( eval1 ` K ) ` r ) = ( ( eval1 ` K ) ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
86 85 fveq1d 
 |-  ( ( ph /\ r = ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) -> ( ( ( eval1 ` K ) ` r ) ` M ) = ( ( ( eval1 ` K ) ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) )
87 81 61 ffvelcdmd 
 |-  ( ph -> ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
88 fvexd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) e. _V )
89 83 86 87 88 fvmptd 
 |-  ( ph -> ( H ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( ( eval1 ` K ) ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) )
90 rhmghm 
 |-  ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) -> F e. ( ( Poly1 ` ( Z/nZ ` N ) ) GrpHom ( Poly1 ` K ) ) )
91 78 90 syl 
 |-  ( ph -> F e. ( ( Poly1 ` ( Z/nZ ` N ) ) GrpHom ( Poly1 ` K ) ) )
92 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
93 35 36 92 ghmlin 
 |-  ( ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) GrpHom ( Poly1 ` K ) ) /\ ( var1 ` ( Z/nZ ` N ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) /\ ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
94 91 49 60 93 syl3anc 
 |-  ( ph -> ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
95 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
96 40 66 35 9 47 95 77 rhmply1vr1 
 |-  ( ph -> ( F ` ( var1 ` ( Z/nZ ` N ) ) ) = ( var1 ` K ) )
97 53 fveq2d 
 |-  ( ph -> ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) = ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) )
98 eqid 
 |-  ( ZRHom ` ( Poly1 ` K ) ) = ( ZRHom ` ( Poly1 ` K ) )
99 78 14 51 98 rhmzrhval 
 |-  ( ph -> ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) = ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) )
100 97 99 eqtrd 
 |-  ( ph -> ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) = ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) )
101 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
102 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
103 66 101 98 102 16 14 ply1asclzrhval 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) = ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) )
104 100 103 eqtr4d 
 |-  ( ph -> ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) = ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) )
105 96 104 oveq12d 
 |-  ( ph -> ( ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) )
106 94 105 eqtrd 
 |-  ( ph -> ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) )
107 106 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) )
108 107 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` M ) )
109 89 108 eqtrd 
 |-  ( ph -> ( H ` ( F ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` M ) )
110 82 109 eqtrd 
 |-  ( ph -> ( ( H o. F ) ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` M ) )
111 110 oveq2d 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` K ) ) ( ( H o. F ) ` ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( N ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` M ) ) )
112 65 111 eqtr2d 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` M ) ) = ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
113 eceq1 
 |-  ( u = ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) -> [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) = [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
114 113 fveq2d 
 |-  ( u = ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) -> ( I ` [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( I ` [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) )
115 fveq2 
 |-  ( u = ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) -> ( ( H o. F ) ` u ) = ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
116 114 115 eqeq12d 
 |-  ( u = ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) -> ( ( I ` [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` u ) <-> ( I ` [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ) )
117 8 oveq1i 
 |-  ( S ~QG L ) = ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L )
118 8 117 oveq12i 
 |-  ( S /s ( S ~QG L ) ) = ( ( Poly1 ` ( Z/nZ ` N ) ) /s ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
119 4 118 eqtri 
 |-  B = ( ( Poly1 ` ( Z/nZ ` N ) ) /s ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
120 8 fveq2i 
 |-  ( RSpan ` S ) = ( RSpan ` ( Poly1 ` ( Z/nZ ` N ) ) )
121 8 fveq2i 
 |-  ( mulGrp ` S ) = ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) )
122 121 fveq2i 
 |-  ( .g ` ( mulGrp ` S ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
123 122 oveqi 
 |-  ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) = ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) )
124 8 fveq2i 
 |-  ( 1r ` S ) = ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) )
125 8 fveq2i 
 |-  ( -g ` S ) = ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) )
126 123 124 125 oveq123i 
 |-  ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) = ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
127 126 sneqi 
 |-  { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } = { ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) }
128 120 127 fveq12i 
 |-  ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } ) = ( ( RSpan ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` { ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) } )
129 5 128 eqtri 
 |-  L = ( ( RSpan ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` { ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) } )
130 1 2 3 9 10 11 12 13 119 129 6 aks5lem2 
 |-  ( ph -> ( I e. ( B RingHom K ) /\ A. u e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( I ` [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` u ) ) )
131 130 simprd 
 |-  ( ph -> A. u e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( I ` [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` u ) )
132 30 ringmgp 
 |-  ( ( Poly1 ` ( Z/nZ ` N ) ) e. Ring -> ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. Mnd )
133 43 132 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. Mnd )
134 62 63 133 34 61 mulgnn0cld 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
135 116 131 134 rspcdva 
 |-  ( ph -> ( I ` [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
136 135 eqcomd 
 |-  ( ph -> ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( I ` [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) )
137 8 eqcomi 
 |-  ( Poly1 ` ( Z/nZ ` N ) ) = S
138 137 a1i 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) = S )
139 138 fveq2d 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( mulGrp ` S ) )
140 139 fveq2d 
 |-  ( ph -> ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) = ( .g ` ( mulGrp ` S ) ) )
141 eqidd 
 |-  ( ph -> N = N )
142 138 fveq2d 
 |-  ( ph -> ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( +g ` S ) )
143 eqidd 
 |-  ( ph -> ( var1 ` ( Z/nZ ` N ) ) = ( var1 ` ( Z/nZ ` N ) ) )
144 138 fveq2d 
 |-  ( ph -> ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( algSc ` S ) )
145 144 fveq1d 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) = ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) )
146 142 143 145 oveq123d 
 |-  ( ph -> ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) = ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) )
147 140 141 146 oveq123d 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
148 147 eceq1d 
 |-  ( ph -> [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) = [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
149 138 oveq1d 
 |-  ( ph -> ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) = ( S ~QG L ) )
150 149 eceq2d 
 |-  ( ph -> [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) = [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( S ~QG L ) )
151 148 150 eqtrd 
 |-  ( ph -> [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) = [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( S ~QG L ) )
152 eqcom 
 |-  ( ( Poly1 ` ( Z/nZ ` N ) ) = S <-> S = ( Poly1 ` ( Z/nZ ` N ) ) )
153 152 imbi2i 
 |-  ( ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) = S ) <-> ( ph -> S = ( Poly1 ` ( Z/nZ ` N ) ) ) )
154 138 153 mpbi 
 |-  ( ph -> S = ( Poly1 ` ( Z/nZ ` N ) ) )
155 154 fveq2d 
 |-  ( ph -> ( +g ` S ) = ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
156 154 fveq2d 
 |-  ( ph -> ( mulGrp ` S ) = ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
157 156 fveq2d 
 |-  ( ph -> ( .g ` ( mulGrp ` S ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) )
158 157 oveqd 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) = ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) )
159 154 fveq2d 
 |-  ( ph -> ( algSc ` S ) = ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
160 159 fveq1d 
 |-  ( ph -> ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) = ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) )
161 155 158 160 oveq123d 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) = ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) )
162 161 eceq1d 
 |-  ( ph -> [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( S ~QG L ) )
163 149 eqcomd 
 |-  ( ph -> ( S ~QG L ) = ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
164 163 eceq2d 
 |-  ( ph -> [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
165 162 164 eqtrd 
 |-  ( ph -> [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( algSc ` S ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
166 151 15 165 3eqtrd 
 |-  ( ph -> [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
167 166 fveq2d 
 |-  ( ph -> ( I ` [ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( I ` [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) )
168 eceq1 
 |-  ( u = ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) -> [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
169 168 fveq2d 
 |-  ( u = ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) -> ( I ` [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( I ` [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) )
170 fveq2 
 |-  ( u = ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) -> ( ( H o. F ) ` u ) = ( ( H o. F ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
171 169 170 eqeq12d 
 |-  ( u = ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) -> ( ( I ` [ u ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` u ) <-> ( I ` [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
172 62 63 133 34 49 mulgnn0cld 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
173 35 36 45 172 60 grpcld 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
174 171 131 173 rspcdva 
 |-  ( ph -> ( I ` [ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
175 136 167 174 3eqtrd 
 |-  ( ph -> ( ( H o. F ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( H o. F ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
176 81 173 fvco3d 
 |-  ( ph -> ( ( H o. F ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( H ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
177 simpr 
 |-  ( ( ph /\ r = ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) -> r = ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
178 177 fveq2d 
 |-  ( ( ph /\ r = ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) -> ( ( eval1 ` K ) ` r ) = ( ( eval1 ` K ) ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
179 178 fveq1d 
 |-  ( ( ph /\ r = ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) -> ( ( ( eval1 ` K ) ` r ) ` M ) = ( ( ( eval1 ` K ) ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) )
180 81 173 ffvelcdmd 
 |-  ( ph -> ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
181 fvexd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) e. _V )
182 83 179 180 181 fvmptd 
 |-  ( ph -> ( H ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( ( eval1 ` K ) ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) )
183 35 36 92 ghmlin 
 |-  ( ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) GrpHom ( Poly1 ` K ) ) /\ ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) /\ ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
184 91 172 60 183 syl3anc 
 |-  ( ph -> ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) )
185 184 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( eval1 ` K ) ` ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) )
186 185 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) )
187 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
188 30 187 rhmmhm 
 |-  ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) -> F e. ( ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) MndHom ( mulGrp ` ( Poly1 ` K ) ) ) )
189 78 188 syl 
 |-  ( ph -> F e. ( ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) MndHom ( mulGrp ` ( Poly1 ` K ) ) ) )
190 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
191 62 63 190 mhmmulg 
 |-  ( ( F e. ( ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) MndHom ( mulGrp ` ( Poly1 ` K ) ) ) /\ N e. NN0 /\ ( var1 ` ( Z/nZ ` N ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) )
192 189 34 49 191 syl3anc 
 |-  ( ph -> ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) )
193 192 97 oveq12d 
 |-  ( ph -> ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) )
194 193 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) ) )
195 194 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) ) ` M ) )
196 96 oveq2d 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) = ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) )
197 196 99 oveq12d 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) = ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) )
198 197 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) ) = ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ) )
199 198 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ) ` M ) )
200 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
201 200 95 25 66 79 16 28 evl1vard 
 |-  ( ph -> ( ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( var1 ` K ) ) ` M ) = M ) )
202 200 66 25 79 16 28 201 190 21 34 evl1expd 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ` M ) = ( N ( .g ` ( mulGrp ` K ) ) M ) ) )
203 66 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
204 16 203 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
205 204 crngringd 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
206 98 zrhrhm 
 |-  ( ( Poly1 ` K ) e. Ring -> ( ZRHom ` ( Poly1 ` K ) ) e. ( ZZring RingHom ( Poly1 ` K ) ) )
207 55 79 rhmf 
 |-  ( ( ZRHom ` ( Poly1 ` K ) ) e. ( ZZring RingHom ( Poly1 ` K ) ) -> ( ZRHom ` ( Poly1 ` K ) ) : ZZ --> ( Base ` ( Poly1 ` K ) ) )
208 206 207 syl 
 |-  ( ( Poly1 ` K ) e. Ring -> ( ZRHom ` ( Poly1 ` K ) ) : ZZ --> ( Base ` ( Poly1 ` K ) ) )
209 205 208 syl 
 |-  ( ph -> ( ZRHom ` ( Poly1 ` K ) ) : ZZ --> ( Base ` ( Poly1 ` K ) ) )
210 209 14 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) e. ( Base ` ( Poly1 ` K ) ) )
211 eqidd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) )
212 210 211 jca 
 |-  ( ph -> ( ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) ) )
213 eqid 
 |-  ( +g ` K ) = ( +g ` K )
214 200 66 25 79 16 28 202 212 92 213 evl1addd 
 |-  ( ph -> ( ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ) ` M ) = ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) ) ) )
215 214 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ) ` M ) = ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) ) )
216 102 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
217 55 25 rhmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
218 216 217 syl 
 |-  ( K e. Ring -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
219 67 218 syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
220 219 14 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) )
221 200 66 25 101 79 16 220 28 evl1scad 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ` M ) = ( ( ZRHom ` K ) ` A ) ) )
222 221 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ` M ) = ( ( ZRHom ` K ) ` A ) )
223 222 eqcomd 
 |-  ( ph -> ( ( ZRHom ` K ) ` A ) = ( ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ` M ) )
224 103 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) = ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) )
225 224 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) )
226 223 225 eqtr2d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) = ( ( ZRHom ` K ) ` A ) )
227 226 oveq2d 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ( eval1 ` K ) ` ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ` M ) ) = ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
228 215 227 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( +g ` ( Poly1 ` K ) ) ( ( ZRHom ` ( Poly1 ` K ) ) ` A ) ) ) ` M ) = ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
229 199 228 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) ) ` M ) = ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
230 19 cmnmndd 
 |-  ( ph -> ( mulGrp ` K ) e. Mnd )
231 26 21 230 34 28 mulgnn0cld 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` K ) ) M ) e. ( Base ` K ) )
232 200 95 25 66 79 16 231 evl1vard 
 |-  ( ph -> ( ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( var1 ` K ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) = ( N ( .g ` ( mulGrp ` K ) ) M ) ) )
233 200 66 25 101 79 16 220 231 evl1scad 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ZRHom ` K ) ` A ) ) )
234 200 66 25 79 16 231 232 233 92 213 evl1addd 
 |-  ( ph -> ( ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
235 234 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( N ( .g ` ( mulGrp ` K ) ) M ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
236 229 235 eqtr4d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( F ` ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( ZRHom ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` A ) ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) )
237 195 236 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( F ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( +g ` ( Poly1 ` K ) ) ( F ` ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) )
238 186 237 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) )
239 182 238 eqtrd 
 |-  ( ph -> ( H ` ( F ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) )
240 176 239 eqtrd 
 |-  ( ph -> ( ( H o. F ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) = ( ( ( eval1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N ( .g ` ( mulGrp ` K ) ) M ) ) )
241 112 175 240 3eqtrd 
 |-  ( 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 ) ) )