aks5lem2 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aks5lem2		Structured version Visualization version GIF version

Theorem aks5lem2 42144

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.)

**Hypotheses**
Ref	Expression
aks5lem1.1	⊢ (𝜑 → 𝐾 ∈ Field)
aks5lem1.2	⊢ 𝑃 = (chr‘𝐾)
aks5lem1.3	⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁))
aks5lem1.4	⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝))
aks5lem1.5	⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞))
aks5lem1.6	⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly₁‘𝐾)) ↦ (((eval₁‘𝐾)‘𝑟)‘𝑀))
aks5lem2.1	⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
aks5lem2.2	⊢ 𝐼 = (𝑠 ∈ (Base‘𝐴) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠))
aks5lem2.3	⊢ 𝐴 = ((Poly₁‘(ℤ/nℤ‘𝑁)) /_s ((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿))
aks5lem2.4	⊢ 𝐿 = ((RSpan‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘{((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))})
aks5lem2.5	⊢ (𝜑 → 𝑅 ∈ ℕ)

**Assertion**
Ref	Expression
aks5lem2	⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔)))

Distinct variable groups: 𝐴,𝑠 𝐹,𝑠 𝐺,𝑝 𝐻,𝑠 𝐼,𝑠 𝐾,𝑝 𝐾,𝑞 𝐾,𝑟 𝐾,𝑠 𝐿,𝑠 𝑀,𝑟 𝑁,𝑝 𝑁,𝑞 𝑁,𝑠 𝑅,𝑝 𝑅,𝑟 𝜑,𝑔,𝑠 𝜑,𝑝 𝜑,𝑟 Allowed substitution hints: 𝜑(𝑞) 𝐴(𝑔,𝑟,𝑞,𝑝) 𝑃(𝑔,𝑠,𝑟,𝑞,𝑝) 𝑅(𝑔,𝑠,𝑞) 𝐹(𝑔,𝑟,𝑞,𝑝) 𝐺(𝑔,𝑠,𝑟,𝑞) 𝐻(𝑔,𝑟,𝑞,𝑝) 𝐼(𝑔,𝑟,𝑞,𝑝) 𝐾(𝑔) 𝐿(𝑔,𝑟,𝑞,𝑝) 𝑀(𝑔,𝑠,𝑞,𝑝) 𝑁(𝑔,𝑟)

Proof of Theorem aks5lem2 Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2740	. 2 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
2		aks5lem1.1	. . 3 ⊢ (𝜑 → 𝐾 ∈ Field)
3		aks5lem1.2	. . 3 ⊢ 𝑃 = (chr‘𝐾)
4		aks5lem1.3	. . 3 ⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁))
5		aks5lem1.4	. . 3 ⊢ 𝐹 = (𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝))
6		aks5lem1.5	. . 3 ⊢ 𝐺 = (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞))
7		aks5lem1.6	. . 3 ⊢ 𝐻 = (𝑟 ∈ (Base‘(Poly₁‘𝐾)) ↦ (((eval₁‘𝐾)‘𝑟)‘𝑀))
8		aks5lem2.1	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
9	2	fldcrngd 20764	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
10		eqid 2740	. . . . . . . . 9 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
11	10	crngmgp 20268	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
12	9, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
13		aks5lem2.5	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ ℕ)
14	13	nnnn0d 12613	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
15		eqid 2740	. . . . . . 7 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
16	12, 14, 15	isprimroot 42050	. . . . . 6 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑙))))
17	8, 16	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑙)))
18	17	simp1d 1142	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
19		eqid 2740	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
20	10, 19	mgpbas 20167	. . . . 5 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
21	20	eqcomi 2749	. . . 4 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
22	18, 21	eleqtrdi 2854	. . 3 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
23	2, 3, 4, 5, 6, 7, 22	aks5lem1 42143	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom 𝐾))
24		eqid 2740	. 2 ⊢ (^◡(𝐻 ∘ 𝐹) “ {(0_g‘𝐾)}) = (^◡(𝐻 ∘ 𝐹) “ {(0_g‘𝐾)})
25		aks5lem2.3	. 2 ⊢ 𝐴 = ((Poly₁‘(ℤ/nℤ‘𝑁)) /_s ((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿))
26		aks5lem2.2	. 2 ⊢ 𝐼 = (𝑠 ∈ (Base‘𝐴) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠))
27	4	simp2d 1143	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
28	27	nnnn0d 12613	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
29		eqid 2740	. . . . 5 ⊢ (ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁)
30	29	zncrng 21586	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (ℤ/nℤ‘𝑁) ∈ CRing)
31	28, 30	syl 17	. . 3 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ CRing)
32		eqid 2740	. . . 4 ⊢ (Poly₁‘(ℤ/nℤ‘𝑁)) = (Poly₁‘(ℤ/nℤ‘𝑁))
33	32	ply1crng 22221	. . 3 ⊢ ((ℤ/nℤ‘𝑁) ∈ CRing → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ CRing)
34	31, 33	syl 17	. 2 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ CRing)
35		aks5lem2.4	. 2 ⊢ 𝐿 = ((RSpan‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘{((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))})
36	34	crnggrpd 20274	. . 3 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Grp)
37		eqid 2740	. . . . 5 ⊢ (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))
38		eqid 2740	. . . . 5 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))
39	37, 38	mgpbas 20167	. . . 4 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
40		eqid 2740	. . . 4 ⊢ (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
41	34	crngringd 20273	. . . . 5 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring)
42	37	ringmgp 20266	. . . . 5 ⊢ ((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
43	41, 42	syl 17	. . . 4 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
44	31	crngringd 20273	. . . . 5 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ Ring)
45		eqid 2740	. . . . . 6 ⊢ (var₁‘(ℤ/nℤ‘𝑁)) = (var₁‘(ℤ/nℤ‘𝑁))
46	45, 32, 38	vr1cl 22240	. . . . 5 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (var₁‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
47	44, 46	syl 17	. . . 4 ⊢ (𝜑 → (var₁‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
48	39, 40, 43, 14, 47	mulgnn0cld 19135	. . 3 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
49		eqid 2740	. . . . 5 ⊢ (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
50	38, 49	ringidcl 20289	. . . 4 ⊢ ((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring → (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
51	41, 50	syl 17	. . 3 ⊢ (𝜑 → (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
52		eqid 2740	. . . 4 ⊢ (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))
53	38, 52	grpsubcl 19060	. . 3 ⊢ (((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Grp ∧ (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∧ (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
54	36, 48, 51, 53	syl3anc 1371	. 2 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
55		fvexd 6935	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) ∈ V)
56	55	mptexd 7261	. . . . . . . . 9 ⊢ (𝜑 → (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) ∈ V)
57	6, 56	eqeltrid 2848	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
58	57	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝐺 ∈ V)
59		vex 3492	. . . . . . . 8 ⊢ 𝑝 ∈ V
60	59	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝑝 ∈ V)
61	58, 60	coexd 7971	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → (𝐺 ∘ 𝑝) ∈ V)
62	61, 5	fmptd 7148	. . . . 5 ⊢ (𝜑 → 𝐹:(Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))⟶V)
63	62	ffund 6751	. . . 4 ⊢ (𝜑 → Fun 𝐹)
64	62	fdmd 6757	. . . . 5 ⊢ (𝜑 → dom 𝐹 = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
65	54, 64	eleqtrrd 2847	. . . 4 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹)
66		fvco 7020	. . . 4 ⊢ ((Fun 𝐹 ∧ ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹) → ((𝐻 ∘ 𝐹)‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))))
67	63, 65, 66	syl2anc 583	. . 3 ⊢ (𝜑 → ((𝐻 ∘ 𝐹)‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))))
68		eqid 2740	. . . . . . . 8 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
69	9	crngringd 20273	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Ring)
70	4	simp1d 1142	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
71		prmnn 16721	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
72	70, 71	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ ℕ)
73	3, 72	eqeltrrid 2849	. . . . . . . . . 10 ⊢ (𝜑 → (chr‘𝐾) ∈ ℕ)
74	73	nnzd 12666	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∈ ℤ)
75	4	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
76	3, 75	eqbrtrrid 5202	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∥ 𝑁)
77	69, 27, 74, 76, 29, 6	zndvdchrrhm 41927	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾))
78	32, 68, 38, 5, 77	rhmply1 22411	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)))
79		rhmghm 20510	. . . . . . 7 ⊢ (𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)) → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
80	78, 79	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
81		eqid 2740	. . . . . . 7 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
82	38, 52, 81	ghmsub 19264	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∧ (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → (𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = ((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))))
83	80, 48, 51, 82	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = ((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))))
84	83	fveq2d 6924	. . . 4 ⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))))
85		eqid 2740	. . . . . . . 8 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
86		eqid 2740	. . . . . . . 8 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
87	85, 68, 19, 86, 9, 22, 7	evl1maprhm 22404	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾))
88		rhmghm 20510	. . . . . . 7 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
89	87, 88	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
90	38, 86	rhmf 20511	. . . . . . . 8 ⊢ (𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)) → 𝐹:(Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))⟶(Base‘(Poly₁‘𝐾)))
91	78, 90	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹:(Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))⟶(Base‘(Poly₁‘𝐾)))
92	91, 48	ffvelcdmd 7119	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
93	91, 51	ffvelcdmd 7119	. . . . . 6 ⊢ (𝜑 → (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
94		eqid 2740	. . . . . . 7 ⊢ (-_g‘𝐾) = (-_g‘𝐾)
95	86, 81, 94	ghmsub 19264	. . . . . 6 ⊢ ((𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾) ∧ (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾))) → (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))))
96	89, 92, 93, 95	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))))
97		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
98	38, 97, 49, 41, 48	ringlidmd 20295	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))
99	98	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
100	31	elexd 3512	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ V)
101	32	ply1sca 22275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ/nℤ‘𝑁) ∈ V → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
103	102	fveq2d 6924	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
104	103	fveq2d 6924	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))))
105		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))
106		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))
107	32	ply1lmod 22274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
108	44, 107	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
109	105, 106, 108, 41	ascl1 21928	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
110	104, 109	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
111	110	eqcomd 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))))
112	111	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
113	99, 112	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = (((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
114	32	ply1assa 22222	. . . . . . . . . . . . . . . 16 ⊢ ((ℤ/nℤ‘𝑁) ∈ CRing → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
115	31, 114	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
116		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(ℤ/nℤ‘𝑁))
117		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(ℤ/nℤ‘𝑁))
118	116, 117	ringidcl 20289	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
119	44, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
120	102	fveq2d 6924	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
121	119, 120	eleqtrd 2846	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
122		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
123		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))
124	105, 106, 122, 38, 97, 123	asclmul1 21929	. . . . . . . . . . . . . . 15 ⊢ (((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg ∧ (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∧ (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → (((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = ((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
125	115, 121, 48, 124	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = ((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
126	113, 125	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
127	126	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))))
128		eqid 2740	. . . . . . . . . . . . 13 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
129		eqid 2740	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘(Poly₁‘𝐾)) = ( ·_𝑠 ‘(Poly₁‘𝐾))
130		eqid 2740	. . . . . . . . . . . . 13 ⊢ (mulGrp‘(Poly₁‘𝐾)) = (mulGrp‘(Poly₁‘𝐾))
131		eqid 2740	. . . . . . . . . . . . 13 ⊢ (._g‘(mulGrp‘(Poly₁‘𝐾))) = (._g‘(mulGrp‘(Poly₁‘𝐾)))
132	32, 68, 38, 116, 5, 45, 128, 123, 129, 37, 130, 40, 131, 77, 119, 14	rhmply1mon 22414	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
133	127, 132	eqtrd 2780	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
134	133	fveq2d 6924	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
135		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝐾) = (1_r‘𝐾)
136	117, 135	rhm1 20515	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾) → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
137	77, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
138	137	oveq1d 7463	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
139	138	fveq2d 6924	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
140	68	ply1assa 22222	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ AssAlg)
141	9, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ AssAlg)
142	19, 135	ringidcl 20289	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (1_r‘𝐾) ∈ (Base‘𝐾))
143	69, 142	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘𝐾))
144	68	ply1sca 22275	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
145	2, 144	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
146	145	fveq2d 6924	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘(Poly₁‘𝐾))))
147	143, 146	eleqtrd 2846	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘(Scalar‘(Poly₁‘𝐾))))
148	130, 86	mgpbas 20167	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(mulGrp‘(Poly₁‘𝐾)))
149	68	ply1crng 22221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
150	9, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ CRing)
151		crngring 20272	. . . . . . . . . . . . . . . . . 18 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Ring)
153	130	ringmgp 20266	. . . . . . . . . . . . . . . . 17 ⊢ ((Poly₁‘𝐾) ∈ Ring → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
154	152, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
155	128, 68, 86	vr1cl 22240	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
156	69, 155	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
157	148, 131, 154, 14, 156	mulgnn0cld 19135	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾)))
158		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
159		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘(Poly₁‘𝐾)) = (Scalar‘(Poly₁‘𝐾))
160		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘𝐾))) = (Base‘(Scalar‘(Poly₁‘𝐾)))
161		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (._r‘(Poly₁‘𝐾)) = (._r‘(Poly₁‘𝐾))
162	158, 159, 160, 86, 161, 129	asclmul1 21929	. . . . . . . . . . . . . . 15 ⊢ (((Poly₁‘𝐾) ∈ AssAlg ∧ (1_r‘𝐾) ∈ (Base‘(Scalar‘(Poly₁‘𝐾))) ∧ (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾))) → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
163	141, 147, 157, 162	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
164	163	eqcomd 2746	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
165	164	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
166		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘(Poly₁‘𝐾)) = (1_r‘(Poly₁‘𝐾))
167	68, 158, 135, 166, 69	ply1ascl1 22278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾)) = (1_r‘(Poly₁‘𝐾)))
168	167	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
169	168	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
170	86, 161, 166, 152, 157	ringlidmd 20295	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))
171	170	fveq2d 6924	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
172	7	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐻 = (𝑟 ∈ (Base‘(Poly₁‘𝐾)) ↦ (((eval₁‘𝐾)‘𝑟)‘𝑀)))
173		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))
174	173	fveq2d 6924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → ((eval₁‘𝐾)‘𝑟) = ((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
175	174	fveq1d 6922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → (((eval₁‘𝐾)‘𝑟)‘𝑀) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
176		fvexd 6935	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) ∈ V)
177	172, 175, 157, 176	fvmptd 7036	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
178	85, 128, 19, 68, 86, 9, 22	evl1vard 22362	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(var₁‘𝐾))‘𝑀) = 𝑀))
179	85, 68, 19, 86, 9, 22, 178, 131, 15, 14	evl1expd 22370	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (𝑅(._g‘(mulGrp‘𝐾))𝑀)))
180	179	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (𝑅(._g‘(mulGrp‘𝐾))𝑀))
181	17	simp2d 1143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)))
182	10, 135	ringidval 20210	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_r‘𝐾) = (0_g‘(mulGrp‘𝐾))
183	182	eqcomi 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾)
184	183	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾))
185	181, 184	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (1_r‘𝐾))
186	180, 185	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (1_r‘𝐾))
187	177, 186	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (1_r‘𝐾))
188	171, 187	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
189	169, 188	eqtrd 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
190	165, 189	eqtrd 2780	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
191	139, 190	eqtrd 2780	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
192	134, 191	eqtrd 2780	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
193	166, 135	rhm1 20515	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
194	87, 193	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
195	194	eqcomd 2746	. . . . . . . . 9 ⊢ (𝜑 → (1_r‘𝐾) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
196	192, 195	eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
197	196, 194	eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
198	49, 166	rhm1 20515	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)) → (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (1_r‘(Poly₁‘𝐾)))
199	78, 198	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (1_r‘(Poly₁‘𝐾)))
200	199	fveq2d 6924	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
201	200, 194	eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
202	197, 201	oveq12d 7466	. . . . . 6 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)))
203	69	ringgrpd 20269	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Grp)
204	19, 1, 94	grpsubid 19064	. . . . . . 7 ⊢ ((𝐾 ∈ Grp ∧ (1_r‘𝐾) ∈ (Base‘𝐾)) → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
205	203, 143, 204	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
206	202, 205	eqtrd 2780	. . . . 5 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
207	96, 206	eqtrd 2780	. . . 4 ⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
208	84, 207	eqtrd 2780	. . 3 ⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
209	67, 208	eqtrd 2780	. 2 ⊢ (𝜑 → ((𝐻 ∘ 𝐹)‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (0_g‘𝐾))
210	1, 23, 24, 25, 26, 34, 35, 54, 209	rhmqusspan 42142	1 ⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ∀wral 3067 Vcvv 3488 {csn 4648 ∪ cuni 4931 class class class wbr 5166 ↦ cmpt 5249 ^◡ccnv 5699 dom cdm 5700 “ cima 5703 ∘ ccom 5704 Fun wfun 6567 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 [cec 8761 ℕcn 12293 ℕ₀cn0 12553 ∥ cdvds 16302 ℙcprime 16718 Basecbs 17258 ._rcmulr 17312 Scalarcsca 17314 ·_𝑠 cvsca 17315 0_gc0g 17499 /_s cqus 17565 Mndcmnd 18772 Grpcgrp 18973 -_gcsg 18975 ._gcmg 19107 ~_QG cqg 19162 GrpHom cghm 19252 CMndccmn 19822 mulGrpcmgp 20161 1_rcur 20208 Ringcrg 20260 CRingccrg 20261 RingHom crh 20495 Fieldcfield 20752 LModclmod 20880 RSpancrsp 21240 ℤRHomczrh 21533 chrcchr 21535 ℤ/nℤczn 21536 AssAlgcasa 21893 algSccascl 21895 var₁cv1 22198 Poly₁cpl1 22199 eval₁ce1 22339 PrimRoots cprimroots 42048

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-addf 11263 ax-mulf 11264

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-ofr 7715 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-tpos 8267 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-ec 8765 df-qs 8769 df-map 8886 df-pm 8887 df-ixp 8956 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-sup 9511 df-inf 9512 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-z 12640 df-dec 12759 df-uz 12904 df-rp 13058 df-fz 13568 df-fzo 13712 df-fl 13843 df-mod 13921 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-dvds 16303 df-prm 16719 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-0g 17501 df-gsum 17502 df-prds 17507 df-pws 17509 df-imas 17568 df-qus 17569 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-mhm 18818 df-submnd 18819 df-grp 18976 df-minusg 18977 df-sbg 18978 df-mulg 19108 df-subg 19163 df-nsg 19164 df-eqg 19165 df-ghm 19253 df-cntz 19357 df-od 19570 df-cmn 19824 df-abl 19825 df-mgp 20162 df-rng 20180 df-ur 20209 df-srg 20214 df-ring 20262 df-cring 20263 df-oppr 20360 df-dvdsr 20383 df-rhm 20498 df-subrng 20572 df-subrg 20597 df-field 20754 df-lmod 20882 df-lss 20953 df-lsp 20993 df-sra 21195 df-rgmod 21196 df-lidl 21241 df-rsp 21242 df-2idl 21283 df-cnfld 21388 df-zring 21481 df-zrh 21537 df-chr 21539 df-zn 21540 df-assa 21896 df-asp 21897 df-ascl 21898 df-psr 21952 df-mvr 21953 df-mpl 21954 df-opsr 21956 df-evls 22121 df-evl 22122 df-psr1 22202 df-vr1 22203 df-ply1 22204 df-coe1 22205 df-evls1 22340 df-evl1 22341 df-primroots 42049

This theorem is referenced by: aks5lem3a 42146

W3C validator