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	⊢ ( 𝜑 → 𝐾 ∈ Field )
	aks5lem1.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
	aks5lem1.3	⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
	aks5lem1.4	⊢ 𝐹 = ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( 𝐺 ∘ 𝑝 ) )
	aks5lem1.5	⊢ 𝐺 = ( 𝑞 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑞 ) )
	aks5lem1.6	⊢ 𝐻 = ( 𝑟 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) )
	aks5lem2.1	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
	aks5lem2.2	⊢ 𝐼 = ( 𝑠 ∈ ( Base ‘ 𝐴 ) ↦ ∪ ( ( 𝐻 ∘ 𝐹 ) “ 𝑠 ) )
	aks5lem2.3	⊢ 𝐴 = ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) /s ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
	aks5lem2.4	⊢ 𝐿 = ( ( RSpan ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) } )
	aks5lem2.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
Assertion	aks5lem2	⊢ ( 𝜑 → ( 𝐼 ∈ ( 𝐴 RingHom 𝐾 ) ∧ ∀ 𝑔 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 𝐼 ‘ [ 𝑔 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑔 ) ) )

Proof

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