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 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
Assertion aks6d1c5lem0 ( 𝜑 → 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1p5.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
2 aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3 aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
4 aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
5 aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
6 aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
7 aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
8 aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
9 eqid ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
10 1 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
11 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
12 11 ply1crng ⊢ ( 𝐾 ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ CRing )
13 10 12 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CRing )
14 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
15 14 crngmgp ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CRing → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
16 13 15 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
18 fzfid ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( 0 ... 𝐴 ) ∈ Fin )
19 17 cmnmndd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
21 nn0ex ⊢ ℕ0 ∈ V
22 21 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
23 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ V )
24 22 23 elmapd ⊢ ( 𝜑 → ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑔 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
25 24 biimpd ⊢ ( 𝜑 → ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) → 𝑔 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
26 25 imp ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → 𝑔 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
27 26 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑔 ‘ 𝑖 ) ∈ ℕ0 )
28 13 crngringd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Ring )
29 28 ringcmnd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CMnd )
30 cmnmnd ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CMnd → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
31 29 30 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
34 10 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → 𝐾 ∈ Ring )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝐾 ∈ Ring )
37 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
38 6 11 37 vr1cl ⊢ ( 𝐾 ∈ Ring → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
39 36 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
40 simpl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) )
41 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → 𝑖 ∈ ℤ )
42 41 adantl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑖 ∈ ℤ )
43 40 42 jca ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ℤ ) )
44 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
45 44 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
46 zringbas ⊢ ℤ = ( Base ‘ ℤring )
47 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
48 46 47 rhmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
49 45 48 syl ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
50 35 49 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
51 50 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ℤ ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
52 43 51 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
53 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
54 11 53 47 37 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
55 36 52 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
56 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
57 37 56 mndcl ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Mnd ∧ 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
58 33 39 55 57 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
59 14 37 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
60 59 a1i ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
61 58 60 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
62 9 7 20 27 61 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
63 62 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ∀ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
64 9 17 18 63 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
65 59 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
67 64 66 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
68 67 8 fmptd ⊢ ( 𝜑 → 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )