Metamath Proof Explorer

Theorem aks6d1c5lem0

Description: Lemma for Claim 5 of Theorem 6.1, G defines a map into the polynomials. (Contributed by metakunt, 5-May-2025)

Ref Expression
Hypotheses aks6d1p5.1 
|- ( ph -> K e. Field )
aks6d1p5.2 
|- ( ph -> P e. Prime )
aks6d1c5.3 
|- P = ( chr ` K )
aks6d1c5.4 
|- ( ph -> A e. NN0 )
aks6d1c5.5 
|- ( ph -> A < P )
aks6d1c5.6 
|- X = ( var1 ` K )
aks6d1c5.7 
|- .^ = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
aks6d1c5.8 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
Assertion aks6d1c5lem0 
|- ( ph -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1p5.1 
 |-  ( ph -> K e. Field )
2 aks6d1p5.2 
 |-  ( ph -> P e. Prime )
3 aks6d1c5.3 
 |-  P = ( chr ` K )
4 aks6d1c5.4 
 |-  ( ph -> A e. NN0 )
5 aks6d1c5.5 
 |-  ( ph -> A < P )
6 aks6d1c5.6 
 |-  X = ( var1 ` K )
7 aks6d1c5.7 
 |-  .^ = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
8 aks6d1c5.8 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
9 eqid 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
10 1 fldcrngd 
 |-  ( ph -> K e. CRing )
11 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
12 11 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
13 10 12 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
14 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
15 14 crngmgp 
 |-  ( ( Poly1 ` K ) e. CRing -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
16 13 15 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
17 16 adantr 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
18 fzfid 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( 0 ... A ) e. Fin )
19 17 cmnmndd 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
20 19 adantr 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
21 nn0ex 
 |-  NN0 e. _V
22 21 a1i 
 |-  ( ph -> NN0 e. _V )
23 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
24 22 23 elmapd 
 |-  ( ph -> ( g e. ( NN0 ^m ( 0 ... A ) ) <-> g : ( 0 ... A ) --> NN0 ) )
25 24 biimpd 
 |-  ( ph -> ( g e. ( NN0 ^m ( 0 ... A ) ) -> g : ( 0 ... A ) --> NN0 ) )
26 25 imp 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> g : ( 0 ... A ) --> NN0 )
27 26 ffvelcdmda 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( g ` i ) e. NN0 )
28 13 crngringd 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
29 28 ringcmnd 
 |-  ( ph -> ( Poly1 ` K ) e. CMnd )
30 cmnmnd 
 |-  ( ( Poly1 ` K ) e. CMnd -> ( Poly1 ` K ) e. Mnd )
31 29 30 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Mnd )
32 31 adantr 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( Poly1 ` K ) e. Mnd )
33 32 adantr 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( Poly1 ` K ) e. Mnd )
34 10 crngringd 
 |-  ( ph -> K e. Ring )
35 34 adantr 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> K e. Ring )
36 35 adantr 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> K e. Ring )
37 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
38 6 11 37 vr1cl 
 |-  ( K e. Ring -> X e. ( Base ` ( Poly1 ` K ) ) )
39 36 38 syl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> X e. ( Base ` ( Poly1 ` K ) ) )
40 simpl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) )
41 elfzelz 
 |-  ( i e. ( 0 ... A ) -> i e. ZZ )
42 41 adantl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> i e. ZZ )
43 40 42 jca 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ZZ ) )
44 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
45 44 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
46 zringbas 
 |-  ZZ = ( Base ` ZZring )
47 eqid 
 |-  ( Base ` K ) = ( Base ` K )
48 46 47 rhmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
49 45 48 syl 
 |-  ( K e. Ring -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
50 35 49 syl 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
51 50 ffvelcdmda 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ZZ ) -> ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) )
52 43 51 syl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) )
53 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
54 11 53 47 37 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
55 36 52 54 syl2anc 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
56 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
57 37 56 mndcl 
 |-  ( ( ( Poly1 ` K ) e. Mnd /\ X e. ( Base ` ( Poly1 ` K ) ) /\ ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
58 33 39 55 57 syl3anc 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
59 14 37 mgpbas 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
60 59 a1i 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
61 58 60 eleqtrd 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
62 9 7 20 27 61 mulgnn0cld 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
63 62 ralrimiva 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> A. i e. ( 0 ... A ) ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
64 9 17 18 63 gsummptcl 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
65 59 eqcomi 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) )
66 65 a1i 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) ) )
67 64 66 eleqtrd 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
68 67 8 fmptd 
 |-  ( ph -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )