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	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1p5.2	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c5.3	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c5.4	$$⊢\phi \to A\in {\mathbb{N}}_0$$
	aks6d1c5.5	$$⊢\phi \to A<P$$
	aks6d1c5.6	$$⊢X={\mathrm{var}}_1\left(K\right)$$
	aks6d1c5.7	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
	aks6d1c5.8	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$
Assertion	aks6d1c5lem0	$$⊢\phi \to G:{{\mathbb{N}}_0}^{\left(0\dots A\right)}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1p5.1	$$⊢\phi \to K\in \mathrm{Field}$$
2		aks6d1p5.2	$$⊢\phi \to P\in \mathbb{P}$$
3		aks6d1c5.3	$$⊢P=\mathrm{chr}\left(K\right)$$
4		aks6d1c5.4	$$⊢\phi \to A\in {\mathbb{N}}_0$$
5		aks6d1c5.5	$$⊢\phi \to A<P$$
6		aks6d1c5.6	$$⊢X={\mathrm{var}}_1\left(K\right)$$
7		aks6d1c5.7	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
8		aks6d1c5.8	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
10	1	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
11		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
12	11	ply1crng	$$⊢K\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
13	10 12	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
14		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
15	14	crngmgp	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{CMnd}$$
16	13 15	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{CMnd}$$
17	16	adantr	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{CMnd}$$
18		fzfid	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to \left(0\dots A\right)\in \mathrm{Fin}$$
19	17	cmnmndd	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
20	19	adantr	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
21		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
23		ovexd	$$⊢\phi \to \left(0\dots A\right)\in \mathrm{V}$$
24	22 23	elmapd	$$⊢\phi \to \left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\leftrightarrow g:\left(0\dots A\right)⟶{\mathbb{N}}_0\right)$$
25	24	biimpd	$$⊢\phi \to \left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\to g:\left(0\dots A\right)⟶{\mathbb{N}}_0\right)$$
26	25	imp	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to g:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
27	26	ffvelcdmda	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to g\left(i\right)\in {\mathbb{N}}_0$$
28	13	crngringd	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
29	28	ringcmnd	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CMnd}$$
30		cmnmnd	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CMnd}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
31	29 30	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
32	31	adantr	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
33	32	adantr	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}$$
34	10	crngringd	$$⊢\phi \to K\in \mathrm{Ring}$$
35	34	adantr	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to K\in \mathrm{Ring}$$
36	35	adantr	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to K\in \mathrm{Ring}$$
37		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
38	6 11 37	vr1cl	$$⊢K\in \mathrm{Ring}\to X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
39	36 38	syl	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
40		simpl	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to \left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)$$
41		elfzelz	$$⊢i\in \left(0\dots A\right)\to i\in \mathbb{Z}$$
42	41	adantl	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to i\in \mathbb{Z}$$
43	40 42	jca	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to \left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \mathbb{Z}\right)$$
44		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)$$
45	44	zrhrhm	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
46		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
47		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
48	46 47	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
49	45 48	syl	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
50	35 49	syl	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
51	50	ffvelcdmda	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \mathbb{Z}\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\in {\mathrm{Base}}_K$$
52	43 51	syl	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\in {\mathrm{Base}}_K$$
53		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
54	11 53 47 37	ply1sclcl	$$⊢\left(K\in \mathrm{Ring}\wedge \mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\in {\mathrm{Base}}_K\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
55	36 52 54	syl2anc	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
56		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{Poly}}_1\left(K\right)}$$
57	37 56	mndcl	$$⊢\left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{Mnd}\wedge X\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
58	33 39 55 57	syl3anc	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
59	14 37	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
60	59	a1i	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
61	58 60	eleqtrd	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
62	9 7 20 27 61	mulgnn0cld	$$⊢\left(\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\wedge i\in \left(0\dots A\right)\right)\to g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
63	62	ralrimiva	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to \forall i\in \left(0\dots A\right)g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
64	9 17 18 63	gsummptcl	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to \underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
65	59	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
66	65	a1i	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
67	64 66	eleqtrd	$$⊢\left(\phi \wedge g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)\right)\to \underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right)\underset{\dot{}}{\times }\left(X{+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
68	67 8	fmptd	$$⊢\phi \to G:{{\mathbb{N}}_0}^{\left(0\dots A\right)}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$