Metamath Proof Explorer

Theorem aks5lem2

Description: Lemma for section 5 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. Construct the quotient for the AKS reduction. (Contributed by metakunt, 7-Jun-2025)

Ref Expression
Hypotheses aks5lem1.1 
|- ( ph -> K e. Field )
aks5lem1.2 
|- P = ( chr ` K )
aks5lem1.3 
|- ( ph -> ( P e. Prime /\ N e. NN /\ P || N ) )
aks5lem1.4 
|- F = ( p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( G o. p ) )
aks5lem1.5 
|- G = ( q e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " q ) )
aks5lem1.6 
|- H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) )
aks5lem2.1 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks5lem2.2 
|- I = ( s e. ( Base ` A ) |-> U. ( ( H o. F ) " s ) )
aks5lem2.3 
|- A = ( ( Poly1 ` ( Z/nZ ` N ) ) /s ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
aks5lem2.4 
|- 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 ) ) ) ) } )
aks5lem2.5 
|- ( ph -> R e. NN )
Assertion aks5lem2 
|- ( ph -> ( I e. ( A RingHom K ) /\ A. g e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( I ` [ g ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` g ) ) )

Proof

Step Hyp Ref Expression
1 aks5lem1.1 
 |-  ( ph -> K e. Field )
2 aks5lem1.2 
 |-  P = ( chr ` K )
3 aks5lem1.3 
 |-  ( ph -> ( P e. Prime /\ N e. NN /\ P || N ) )
4 aks5lem1.4 
 |-  F = ( p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( G o. p ) )
5 aks5lem1.5 
 |-  G = ( q e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " q ) )
6 aks5lem1.6 
 |-  H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) )
7 aks5lem2.1 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
8 aks5lem2.2 
 |-  I = ( s e. ( Base ` A ) |-> U. ( ( H o. F ) " s ) )
9 aks5lem2.3 
 |-  A = ( ( Poly1 ` ( Z/nZ ` N ) ) /s ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) )
10 aks5lem2.4 
 |-  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 ) ) ) ) } )
11 aks5lem2.5 
 |-  ( ph -> R e. NN )
12 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
13 1 fldcrngd 
 |-  ( ph -> K e. CRing )
14 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
15 14 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
16 13 15 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
17 11 nnnn0d 
 |-  ( ph -> R e. NN0 )
18 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
19 16 17 18 isprimroot 
 |-  ( ph -> ( M e. ( ( mulGrp ` K ) PrimRoots R ) <-> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. l e. NN0 ( ( l ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || l ) ) ) )
20 7 19 mpbid 
 |-  ( ph -> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. l e. NN0 ( ( l ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || l ) ) )
21 20 simp1d 
 |-  ( ph -> M e. ( Base ` ( mulGrp ` K ) ) )
22 eqid 
 |-  ( Base ` K ) = ( Base ` K )
23 14 22 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
24 23 eqcomi 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` K )
25 21 24 eleqtrdi 
 |-  ( ph -> M e. ( Base ` K ) )
26 1 2 3 4 5 6 25 aks5lem1 
 |-  ( ph -> ( H o. F ) e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom K ) )
27 eqid 
 |-  ( `' ( H o. F ) " { ( 0g ` K ) } ) = ( `' ( H o. F ) " { ( 0g ` K ) } )
28 3 simp2d 
 |-  ( ph -> N e. NN )
29 28 nnnn0d 
 |-  ( ph -> N e. NN0 )
30 eqid 
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
31 30 zncrng 
 |-  ( N e. NN0 -> ( Z/nZ ` N ) e. CRing )
32 29 31 syl 
 |-  ( ph -> ( Z/nZ ` N ) e. CRing )
33 eqid 
 |-  ( Poly1 ` ( Z/nZ ` N ) ) = ( Poly1 ` ( Z/nZ ` N ) )
34 33 ply1crng 
 |-  ( ( Z/nZ ` N ) e. CRing -> ( Poly1 ` ( Z/nZ ` N ) ) e. CRing )
35 32 34 syl 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. CRing )
36 35 crnggrpd 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. Grp )
37 eqid 
 |-  ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) )
38 eqid 
 |-  ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) )
39 37 38 mgpbas 
 |-  ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
40 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
41 35 crngringd 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. Ring )
42 37 ringmgp 
 |-  ( ( Poly1 ` ( Z/nZ ` N ) ) e. Ring -> ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. Mnd )
43 41 42 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. Mnd )
44 32 crngringd 
 |-  ( ph -> ( Z/nZ ` N ) e. Ring )
45 eqid 
 |-  ( var1 ` ( Z/nZ ` N ) ) = ( var1 ` ( Z/nZ ` N ) )
46 45 33 38 vr1cl 
 |-  ( ( Z/nZ ` N ) e. Ring -> ( var1 ` ( Z/nZ ` N ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
47 44 46 syl 
 |-  ( ph -> ( var1 ` ( Z/nZ ` N ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
48 39 40 43 17 47 mulgnn0cld 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
49 eqid 
 |-  ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) )
50 38 49 ringidcl 
 |-  ( ( Poly1 ` ( Z/nZ ` N ) ) e. Ring -> ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
51 41 50 syl 
 |-  ( ph -> ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
52 eqid 
 |-  ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) )
53 38 52 grpsubcl 
 |-  ( ( ( Poly1 ` ( Z/nZ ` N ) ) e. Grp /\ ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) /\ ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( 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 ) ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
54 36 48 51 53 syl3anc 
 |-  ( ph -> ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
55 fvexd 
 |-  ( ph -> ( Base ` ( Z/nZ ` N ) ) e. _V )
56 55 mptexd 
 |-  ( ph -> ( q e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " q ) ) e. _V )
57 5 56 eqeltrid 
 |-  ( ph -> G e. _V )
58 57 adantr 
 |-  ( ( ph /\ p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> G e. _V )
59 vex 
 |-  p e. _V
60 59 a1i 
 |-  ( ( ph /\ p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> p e. _V )
61 58 60 coexd 
 |-  ( ( ph /\ p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> ( G o. p ) e. _V )
62 61 4 fmptd 
 |-  ( ph -> F : ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) --> _V )
63 62 ffund 
 |-  ( ph -> Fun F )
64 62 fdmd 
 |-  ( ph -> dom F = ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
65 54 64 eleqtrrd 
 |-  ( ph -> ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) e. dom F )
66 fvco 
 |-  ( ( Fun F /\ ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) e. dom F ) -> ( ( H o. F ) ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( H ` ( F ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) )
67 63 65 66 syl2anc 
 |-  ( ph -> ( ( H o. F ) ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( H ` ( F ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) )
68 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
69 13 crngringd 
 |-  ( ph -> K e. Ring )
70 3 simp1d 
 |-  ( ph -> P e. Prime )
71 prmnn 
 |-  ( P e. Prime -> P e. NN )
72 70 71 syl 
 |-  ( ph -> P e. NN )
73 2 72 eqeltrrid 
 |-  ( ph -> ( chr ` K ) e. NN )
74 73 nnzd 
 |-  ( ph -> ( chr ` K ) e. ZZ )
75 3 simp3d 
 |-  ( ph -> P || N )
76 2 75 eqbrtrrid 
 |-  ( ph -> ( chr ` K ) || N )
77 69 28 74 76 30 5 zndvdchrrhm 
 |-  ( ph -> G e. ( ( Z/nZ ` N ) RingHom K ) )
78 33 68 38 4 77 rhmply1 
 |-  ( ph -> F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) )
79 rhmghm 
 |-  ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) -> F e. ( ( Poly1 ` ( Z/nZ ` N ) ) GrpHom ( Poly1 ` K ) ) )
80 78 79 syl 
 |-  ( ph -> F e. ( ( Poly1 ` ( Z/nZ ` N ) ) GrpHom ( Poly1 ` K ) ) )
81 eqid 
 |-  ( -g ` ( Poly1 ` K ) ) = ( -g ` ( Poly1 ` K ) )
82 38 52 81 ghmsub 
 |-  ( ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) GrpHom ( Poly1 ` K ) ) /\ ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) /\ ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> ( F ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( -g ` ( Poly1 ` K ) ) ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) )
83 80 48 51 82 syl3anc 
 |-  ( ph -> ( F ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( -g ` ( Poly1 ` K ) ) ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) )
84 83 fveq2d 
 |-  ( ph -> ( H ` ( F ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) = ( H ` ( ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( -g ` ( Poly1 ` K ) ) ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) )
85 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
86 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
87 85 68 22 86 13 25 6 evl1maprhm 
 |-  ( ph -> H e. ( ( Poly1 ` K ) RingHom K ) )
88 rhmghm 
 |-  ( H e. ( ( Poly1 ` K ) RingHom K ) -> H e. ( ( Poly1 ` K ) GrpHom K ) )
89 87 88 syl 
 |-  ( ph -> H e. ( ( Poly1 ` K ) GrpHom K ) )
90 38 86 rhmf 
 |-  ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) -> F : ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) --> ( Base ` ( Poly1 ` K ) ) )
91 78 90 syl 
 |-  ( ph -> F : ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) --> ( Base ` ( Poly1 ` K ) ) )
92 91 48 ffvelcdmd 
 |-  ( ph -> ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
93 91 51 ffvelcdmd 
 |-  ( ph -> ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
94 eqid 
 |-  ( -g ` K ) = ( -g ` K )
95 86 81 94 ghmsub 
 |-  ( ( H e. ( ( Poly1 ` K ) GrpHom K ) /\ ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( H ` ( ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( -g ` ( Poly1 ` K ) ) ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) = ( ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) ( -g ` K ) ( H ` ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) )
96 89 92 93 95 syl3anc 
 |-  ( ph -> ( H ` ( ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( -g ` ( Poly1 ` K ) ) ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) = ( ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) ( -g ` K ) ( H ` ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) )
97 eqid 
 |-  ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) )
98 38 97 49 41 48 ringlidmd 
 |-  ( ph -> ( ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) )
99 98 eqcomd 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) = ( ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) )
100 32 elexd 
 |-  ( ph -> ( Z/nZ ` N ) e. _V )
101 33 ply1sca 
 |-  ( ( Z/nZ ` N ) e. _V -> ( Z/nZ ` N ) = ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
102 100 101 syl 
 |-  ( ph -> ( Z/nZ ` N ) = ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
103 102 fveq2d 
 |-  ( ph -> ( 1r ` ( Z/nZ ` N ) ) = ( 1r ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) )
104 103 fveq2d 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Z/nZ ` N ) ) ) = ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) )
105 eqid 
 |-  ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) )
106 eqid 
 |-  ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) )
107 33 ply1lmod 
 |-  ( ( Z/nZ ` N ) e. Ring -> ( Poly1 ` ( Z/nZ ` N ) ) e. LMod )
108 44 107 syl 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. LMod )
109 105 106 108 41 ascl1 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
110 104 109 eqtrd 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Z/nZ ` N ) ) ) = ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
111 110 eqcomd 
 |-  ( ph -> ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Z/nZ ` N ) ) ) )
112 111 oveq1d 
 |-  ( ph -> ( ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Z/nZ ` N ) ) ) ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) )
113 99 112 eqtrd 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) = ( ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Z/nZ ` N ) ) ) ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) )
114 33 ply1assa 
 |-  ( ( Z/nZ ` N ) e. CRing -> ( Poly1 ` ( Z/nZ ` N ) ) e. AssAlg )
115 32 114 syl 
 |-  ( ph -> ( Poly1 ` ( Z/nZ ` N ) ) e. AssAlg )
116 eqid 
 |-  ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) )
117 eqid 
 |-  ( 1r ` ( Z/nZ ` N ) ) = ( 1r ` ( Z/nZ ` N ) )
118 116 117 ringidcl 
 |-  ( ( Z/nZ ` N ) e. Ring -> ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) )
119 44 118 syl 
 |-  ( ph -> ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) )
120 102 fveq2d 
 |-  ( ph -> ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) )
121 119 120 eleqtrd 
 |-  ( ph -> ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) )
122 eqid 
 |-  ( Base ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) )
123 eqid 
 |-  ( .s ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( .s ` ( Poly1 ` ( Z/nZ ` N ) ) )
124 105 106 122 38 97 123 asclmul1 
 |-  ( ( ( Poly1 ` ( Z/nZ ` N ) ) e. AssAlg /\ ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Scalar ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) /\ ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) -> ( ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Z/nZ ` N ) ) ) ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( ( 1r ` ( Z/nZ ` N ) ) ( .s ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) )
125 115 121 48 124 syl3anc 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` ( Z/nZ ` N ) ) ) ` ( 1r ` ( Z/nZ ` N ) ) ) ( .r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( ( 1r ` ( Z/nZ ` N ) ) ( .s ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) )
126 113 125 eqtrd 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) = ( ( 1r ` ( Z/nZ ` N ) ) ( .s ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) )
127 126 fveq2d 
 |-  ( ph -> ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( F ` ( ( 1r ` ( Z/nZ ` N ) ) ( .s ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) )
128 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
129 eqid 
 |-  ( .s ` ( Poly1 ` K ) ) = ( .s ` ( Poly1 ` K ) )
130 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
131 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
132 33 68 38 116 4 45 128 123 129 37 130 40 131 77 119 17 rhmply1mon 
 |-  ( ph -> ( F ` ( ( 1r ` ( Z/nZ ` N ) ) ( .s ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) = ( ( G ` ( 1r ` ( Z/nZ ` N ) ) ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
133 127 132 eqtrd 
 |-  ( ph -> ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) = ( ( G ` ( 1r ` ( Z/nZ ` N ) ) ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
134 133 fveq2d 
 |-  ( ph -> ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) = ( H ` ( ( G ` ( 1r ` ( Z/nZ ` N ) ) ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) )
135 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
136 117 135 rhm1 
 |-  ( G e. ( ( Z/nZ ` N ) RingHom K ) -> ( G ` ( 1r ` ( Z/nZ ` N ) ) ) = ( 1r ` K ) )
137 77 136 syl 
 |-  ( ph -> ( G ` ( 1r ` ( Z/nZ ` N ) ) ) = ( 1r ` K ) )
138 137 oveq1d 
 |-  ( ph -> ( ( G ` ( 1r ` ( Z/nZ ` N ) ) ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( ( 1r ` K ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
139 138 fveq2d 
 |-  ( ph -> ( H ` ( ( G ` ( 1r ` ( Z/nZ ` N ) ) ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( H ` ( ( 1r ` K ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) )
140 68 ply1assa 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. AssAlg )
141 13 140 syl 
 |-  ( ph -> ( Poly1 ` K ) e. AssAlg )
142 22 135 ringidcl 
 |-  ( K e. Ring -> ( 1r ` K ) e. ( Base ` K ) )
143 69 142 syl 
 |-  ( ph -> ( 1r ` K ) e. ( Base ` K ) )
144 68 ply1sca 
 |-  ( K e. Field -> K = ( Scalar ` ( Poly1 ` K ) ) )
145 1 144 syl 
 |-  ( ph -> K = ( Scalar ` ( Poly1 ` K ) ) )
146 145 fveq2d 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( Scalar ` ( Poly1 ` K ) ) ) )
147 143 146 eleqtrd 
 |-  ( ph -> ( 1r ` K ) e. ( Base ` ( Scalar ` ( Poly1 ` K ) ) ) )
148 130 86 mgpbas 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
149 68 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
150 13 149 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
151 crngring 
 |-  ( ( Poly1 ` K ) e. CRing -> ( Poly1 ` K ) e. Ring )
152 150 151 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
153 130 ringmgp 
 |-  ( ( Poly1 ` K ) e. Ring -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
154 152 153 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
155 128 68 86 vr1cl 
 |-  ( K e. Ring -> ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) )
156 69 155 syl 
 |-  ( ph -> ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) )
157 148 131 154 17 156 mulgnn0cld 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) e. ( Base ` ( Poly1 ` K ) ) )
158 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
159 eqid 
 |-  ( Scalar ` ( Poly1 ` K ) ) = ( Scalar ` ( Poly1 ` K ) )
160 eqid 
 |-  ( Base ` ( Scalar ` ( Poly1 ` K ) ) ) = ( Base ` ( Scalar ` ( Poly1 ` K ) ) )
161 eqid 
 |-  ( .r ` ( Poly1 ` K ) ) = ( .r ` ( Poly1 ` K ) )
162 158 159 160 86 161 129 asclmul1 
 |-  ( ( ( Poly1 ` K ) e. AssAlg /\ ( 1r ` K ) e. ( Base ` ( Scalar ` ( Poly1 ` K ) ) ) /\ ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( ( 1r ` K ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
163 141 147 157 162 syl3anc 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( ( 1r ` K ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
164 163 eqcomd 
 |-  ( ph -> ( ( 1r ` K ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
165 164 fveq2d 
 |-  ( ph -> ( H ` ( ( 1r ` K ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( H ` ( ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) )
166 eqid 
 |-  ( 1r ` ( Poly1 ` K ) ) = ( 1r ` ( Poly1 ` K ) )
167 68 158 135 166 69 ply1ascl1 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) = ( 1r ` ( Poly1 ` K ) ) )
168 167 oveq1d 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( ( 1r ` ( Poly1 ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
169 168 fveq2d 
 |-  ( ph -> ( H ` ( ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( H ` ( ( 1r ` ( Poly1 ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) )
170 86 161 166 152 157 ringlidmd 
 |-  ( ph -> ( ( 1r ` ( Poly1 ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) )
171 170 fveq2d 
 |-  ( ph -> ( H ` ( ( 1r ` ( Poly1 ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( H ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
172 6 a1i 
 |-  ( ph -> H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) ) )
173 simpr 
 |-  ( ( ph /\ r = ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) -> r = ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) )
174 173 fveq2d 
 |-  ( ( ph /\ r = ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) -> ( ( eval1 ` K ) ` r ) = ( ( eval1 ` K ) ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
175 174 fveq1d 
 |-  ( ( ph /\ r = ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) -> ( ( ( eval1 ` K ) ` r ) ` M ) = ( ( ( eval1 ` K ) ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ` M ) )
176 fvexd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ` M ) e. _V )
177 172 175 157 176 fvmptd 
 |-  ( ph -> ( H ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( ( ( eval1 ` K ) ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ` M ) )
178 85 128 22 68 86 13 25 evl1vard 
 |-  ( ph -> ( ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( var1 ` K ) ) ` M ) = M ) )
179 85 68 22 86 13 25 178 131 18 17 evl1expd 
 |-  ( ph -> ( ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ` M ) = ( R ( .g ` ( mulGrp ` K ) ) M ) ) )
180 179 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ` M ) = ( R ( .g ` ( mulGrp ` K ) ) M ) )
181 20 simp2d 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) )
182 14 135 ringidval 
 |-  ( 1r ` K ) = ( 0g ` ( mulGrp ` K ) )
183 182 eqcomi 
 |-  ( 0g ` ( mulGrp ` K ) ) = ( 1r ` K )
184 183 a1i 
 |-  ( ph -> ( 0g ` ( mulGrp ` K ) ) = ( 1r ` K ) )
185 181 184 eqtrd 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 1r ` K ) )
186 180 185 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ` M ) = ( 1r ` K ) )
187 177 186 eqtrd 
 |-  ( ph -> ( H ` ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( 1r ` K ) )
188 171 187 eqtrd 
 |-  ( ph -> ( H ` ( ( 1r ` ( Poly1 ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( 1r ` K ) )
189 169 188 eqtrd 
 |-  ( ph -> ( H ` ( ( ( algSc ` ( Poly1 ` K ) ) ` ( 1r ` K ) ) ( .r ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( 1r ` K ) )
190 165 189 eqtrd 
 |-  ( ph -> ( H ` ( ( 1r ` K ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( 1r ` K ) )
191 139 190 eqtrd 
 |-  ( ph -> ( H ` ( ( G ` ( 1r ` ( Z/nZ ` N ) ) ) ( .s ` ( Poly1 ` K ) ) ( R ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) ) = ( 1r ` K ) )
192 134 191 eqtrd 
 |-  ( ph -> ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) = ( 1r ` K ) )
193 166 135 rhm1 
 |-  ( H e. ( ( Poly1 ` K ) RingHom K ) -> ( H ` ( 1r ` ( Poly1 ` K ) ) ) = ( 1r ` K ) )
194 87 193 syl 
 |-  ( ph -> ( H ` ( 1r ` ( Poly1 ` K ) ) ) = ( 1r ` K ) )
195 194 eqcomd 
 |-  ( ph -> ( 1r ` K ) = ( H ` ( 1r ` ( Poly1 ` K ) ) ) )
196 192 195 eqtrd 
 |-  ( ph -> ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) = ( H ` ( 1r ` ( Poly1 ` K ) ) ) )
197 196 194 eqtrd 
 |-  ( ph -> ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) = ( 1r ` K ) )
198 49 166 rhm1 
 |-  ( F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) -> ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) = ( 1r ` ( Poly1 ` K ) ) )
199 78 198 syl 
 |-  ( ph -> ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) = ( 1r ` ( Poly1 ` K ) ) )
200 199 fveq2d 
 |-  ( ph -> ( H ` ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( H ` ( 1r ` ( Poly1 ` K ) ) ) )
201 200 194 eqtrd 
 |-  ( ph -> ( H ` ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( 1r ` K ) )
202 197 201 oveq12d 
 |-  ( ph -> ( ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) ( -g ` K ) ( H ` ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) = ( ( 1r ` K ) ( -g ` K ) ( 1r ` K ) ) )
203 69 ringgrpd 
 |-  ( ph -> K e. Grp )
204 22 12 94 grpsubid 
 |-  ( ( K e. Grp /\ ( 1r ` K ) e. ( Base ` K ) ) -> ( ( 1r ` K ) ( -g ` K ) ( 1r ` K ) ) = ( 0g ` K ) )
205 203 143 204 syl2anc 
 |-  ( ph -> ( ( 1r ` K ) ( -g ` K ) ( 1r ` K ) ) = ( 0g ` K ) )
206 202 205 eqtrd 
 |-  ( ph -> ( ( H ` ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ) ( -g ` K ) ( H ` ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) = ( 0g ` K ) )
207 96 206 eqtrd 
 |-  ( ph -> ( H ` ( ( F ` ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ) ( -g ` ( Poly1 ` K ) ) ( F ` ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) = ( 0g ` K ) )
208 84 207 eqtrd 
 |-  ( ph -> ( H ` ( F ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) ) = ( 0g ` K ) )
209 67 208 eqtrd 
 |-  ( ph -> ( ( H o. F ) ` ( ( R ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` N ) ) ) ) ) = ( 0g ` K ) )
210 12 26 27 9 8 35 10 54 209 rhmqusspan 
 |-  ( ph -> ( I e. ( A RingHom K ) /\ A. g e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) ( I ` [ g ] ( ( Poly1 ` ( Z/nZ ` N ) ) ~QG L ) ) = ( ( H o. F ) ` g ) ) )