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 42160

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 2729	. 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 20627	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
10		eqid 2729	. . . . . . . . 9 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
11	10	crngmgp 20126	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
12	9, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
13		aks5lem2.5	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ ℕ)
14	13	nnnn0d 12445	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
15		eqid 2729	. . . . . . 7 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
16	12, 14, 15	isprimroot 42066	. . . . . 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 2729	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
20	10, 19	mgpbas 20030	. . . . 5 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
21	20	eqcomi 2738	. . . 4 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
22	18, 21	eleqtrdi 2838	. . 3 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
23	2, 3, 4, 5, 6, 7, 22	aks5lem1 42159	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom 𝐾))
24		eqid 2729	. 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 12445	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
29		eqid 2729	. . . . 5 ⊢ (ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁)
30	29	zncrng 21451	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (ℤ/nℤ‘𝑁) ∈ CRing)
31	28, 30	syl 17	. . 3 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ CRing)
32		eqid 2729	. . . 4 ⊢ (Poly₁‘(ℤ/nℤ‘𝑁)) = (Poly₁‘(ℤ/nℤ‘𝑁))
33	32	ply1crng 22081	. . 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 20132	. . 3 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Grp)
37		eqid 2729	. . . . 5 ⊢ (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))
38		eqid 2729	. . . . 5 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))
39	37, 38	mgpbas 20030	. . . 4 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
40		eqid 2729	. . . 4 ⊢ (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
41	34	crngringd 20131	. . . . 5 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring)
42	37	ringmgp 20124	. . . . 5 ⊢ ((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
43	41, 42	syl 17	. . . 4 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
44	31	crngringd 20131	. . . . 5 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ Ring)
45		eqid 2729	. . . . . 6 ⊢ (var₁‘(ℤ/nℤ‘𝑁)) = (var₁‘(ℤ/nℤ‘𝑁))
46	45, 32, 38	vr1cl 22100	. . . . 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 18974	. . 3 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
49		eqid 2729	. . . . 5 ⊢ (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
50	38, 49	ringidcl 20150	. . . 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 2729	. . . 4 ⊢ (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))
53	38, 52	grpsubcl 18899	. . 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 1373	. 2 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
55		fvexd 6837	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) ∈ V)
56	55	mptexd 7160	. . . . . . . . 9 ⊢ (𝜑 → (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) ∈ V)
57	6, 56	eqeltrid 2832	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
58	57	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝐺 ∈ V)
59		vex 3440	. . . . . . . 8 ⊢ 𝑝 ∈ V
60	59	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝑝 ∈ V)
61	58, 60	coexd 7864	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → (𝐺 ∘ 𝑝) ∈ V)
62	61, 5	fmptd 7048	. . . . 5 ⊢ (𝜑 → 𝐹:(Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))⟶V)
63	62	ffund 6656	. . . 4 ⊢ (𝜑 → Fun 𝐹)
64	62	fdmd 6662	. . . . 5 ⊢ (𝜑 → dom 𝐹 = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
65	54, 64	eleqtrrd 2831	. . . 4 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹)
66		fvco 6921	. . . 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 584	. . 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 2729	. . . . . . . 8 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
69	9	crngringd 20131	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Ring)
70	4	simp1d 1142	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
71		prmnn 16585	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
72	70, 71	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ ℕ)
73	3, 72	eqeltrrid 2833	. . . . . . . . . 10 ⊢ (𝜑 → (chr‘𝐾) ∈ ℕ)
74	73	nnzd 12498	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∈ ℤ)
75	4	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
76	3, 75	eqbrtrrid 5128	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∥ 𝑁)
77	69, 27, 74, 76, 29, 6	zndvdchrrhm 41945	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾))
78	32, 68, 38, 5, 77	rhmply1 22271	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)))
79		rhmghm 20369	. . . . . . 7 ⊢ (𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)) → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
80	78, 79	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
81		eqid 2729	. . . . . . 7 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
82	38, 52, 81	ghmsub 19103	. . . . . 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 1373	. . . . 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 6826	. . . 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 2729	. . . . . . . 8 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
86		eqid 2729	. . . . . . . 8 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
87	85, 68, 19, 86, 9, 22, 7	evl1maprhm 22264	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾))
88		rhmghm 20369	. . . . . . 7 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
89	87, 88	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
90	38, 86	rhmf 20370	. . . . . . . 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 7019	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
93	91, 51	ffvelcdmd 7019	. . . . . 6 ⊢ (𝜑 → (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
94		eqid 2729	. . . . . . 7 ⊢ (-_g‘𝐾) = (-_g‘𝐾)
95	86, 81, 94	ghmsub 19103	. . . . . 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 1373	. . . . 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 2729	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
98	38, 97, 49, 41, 48	ringlidmd 20157	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))
99	98	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
100	31	elexd 3460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ V)
101	32	ply1sca 22135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ/nℤ‘𝑁) ∈ V → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
103	102	fveq2d 6826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
104	103	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))))
105		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))
106		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))
107	32	ply1lmod 22134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
108	44, 107	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
109	105, 106, 108, 41	ascl1 21792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
110	104, 109	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
111	110	eqcomd 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))))
112	111	oveq1d 7364	. . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . 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 22082	. . . . . . . . . . . . . . . 16 ⊢ ((ℤ/nℤ‘𝑁) ∈ CRing → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
115	31, 114	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
116		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(ℤ/nℤ‘𝑁))
117		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(ℤ/nℤ‘𝑁))
118	116, 117	ringidcl 20150	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
119	44, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
120	102	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
121	119, 120	eleqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
122		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
123		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))
124	105, 106, 122, 38, 97, 123	asclmul1 21793	. . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
127	126	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))))
128		eqid 2729	. . . . . . . . . . . . 13 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
129		eqid 2729	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘(Poly₁‘𝐾)) = ( ·_𝑠 ‘(Poly₁‘𝐾))
130		eqid 2729	. . . . . . . . . . . . 13 ⊢ (mulGrp‘(Poly₁‘𝐾)) = (mulGrp‘(Poly₁‘𝐾))
131		eqid 2729	. . . . . . . . . . . . 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 22274	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
133	127, 132	eqtrd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
134	133	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
135		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝐾) = (1_r‘𝐾)
136	117, 135	rhm1 20374	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾) → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
137	77, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
138	137	oveq1d 7364	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
139	138	fveq2d 6826	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
140	68	ply1assa 22082	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ AssAlg)
141	9, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ AssAlg)
142	19, 135	ringidcl 20150	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (1_r‘𝐾) ∈ (Base‘𝐾))
143	69, 142	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘𝐾))
144	68	ply1sca 22135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
145	2, 144	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
146	145	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘(Poly₁‘𝐾))))
147	143, 146	eleqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘(Scalar‘(Poly₁‘𝐾))))
148	130, 86	mgpbas 20030	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(mulGrp‘(Poly₁‘𝐾)))
149	68	ply1crng 22081	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
150	9, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ CRing)
151		crngring 20130	. . . . . . . . . . . . . . . . . 18 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Ring)
153	130	ringmgp 20124	. . . . . . . . . . . . . . . . 17 ⊢ ((Poly₁‘𝐾) ∈ Ring → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
154	152, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
155	128, 68, 86	vr1cl 22100	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
156	69, 155	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
157	148, 131, 154, 14, 156	mulgnn0cld 18974	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾)))
158		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
159		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘(Poly₁‘𝐾)) = (Scalar‘(Poly₁‘𝐾))
160		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘𝐾))) = (Base‘(Scalar‘(Poly₁‘𝐾)))
161		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (._r‘(Poly₁‘𝐾)) = (._r‘(Poly₁‘𝐾))
162	158, 159, 160, 86, 161, 129	asclmul1 21793	. . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
164	163	eqcomd 2735	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
165	164	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
166		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘(Poly₁‘𝐾)) = (1_r‘(Poly₁‘𝐾))
167	68, 158, 135, 166, 69	ply1ascl1 22138	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾)) = (1_r‘(Poly₁‘𝐾)))
168	167	oveq1d 7364	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
169	168	fveq2d 6826	. . . . . . . . . . . . 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 20157	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))
171	170	fveq2d 6826	. . . . . . . . . . . . . 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 6826	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → ((eval₁‘𝐾)‘𝑟) = ((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
175	174	fveq1d 6824	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → (((eval₁‘𝐾)‘𝑟)‘𝑀) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
176		fvexd 6837	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) ∈ V)
177	172, 175, 157, 176	fvmptd 6937	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
178	85, 128, 19, 68, 86, 9, 22	evl1vard 22222	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(var₁‘𝐾))‘𝑀) = 𝑀))
179	85, 68, 19, 86, 9, 22, 178, 131, 15, 14	evl1expd 22230	. . . . . . . . . . . . . . . . 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 20068	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_r‘𝐾) = (0_g‘(mulGrp‘𝐾))
183	182	eqcomi 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾)
184	183	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾))
185	181, 184	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (1_r‘𝐾))
186	180, 185	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (1_r‘𝐾))
187	177, 186	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (1_r‘𝐾))
188	171, 187	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
189	169, 188	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
190	165, 189	eqtrd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
191	139, 190	eqtrd 2764	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
192	134, 191	eqtrd 2764	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
193	166, 135	rhm1 20374	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
194	87, 193	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
195	194	eqcomd 2735	. . . . . . . . 9 ⊢ (𝜑 → (1_r‘𝐾) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
196	192, 195	eqtrd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
197	196, 194	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
198	49, 166	rhm1 20374	. . . . . . . . . 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 6826	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
201	200, 194	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
202	197, 201	oveq12d 7367	. . . . . 6 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)))
203	69	ringgrpd 20127	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Grp)
204	19, 1, 94	grpsubid 18903	. . . . . . 7 ⊢ ((𝐾 ∈ Grp ∧ (1_r‘𝐾) ∈ (Base‘𝐾)) → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
205	203, 143, 204	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
206	202, 205	eqtrd 2764	. . . . 5 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
207	96, 206	eqtrd 2764	. . . 4 ⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
208	84, 207	eqtrd 2764	. . 3 ⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
209	67, 208	eqtrd 2764	. 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 42158	1 ⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 Vcvv 3436 {csn 4577 ∪ cuni 4858 class class class wbr 5092 ↦ cmpt 5173 ^◡ccnv 5618 dom cdm 5619 “ cima 5622 ∘ ccom 5623 Fun wfun 6476 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 [cec 8623 ℕcn 12128 ℕ₀cn0 12384 ∥ cdvds 16163 ℙcprime 16582 Basecbs 17120 ._rcmulr 17162 Scalarcsca 17164 ·_𝑠 cvsca 17165 0_gc0g 17343 /_s cqus 17409 Mndcmnd 18608 Grpcgrp 18812 -_gcsg 18814 ._gcmg 18946 ~_QG cqg 19001 GrpHom cghm 19091 CMndccmn 19659 mulGrpcmgp 20025 1_rcur 20066 Ringcrg 20118 CRingccrg 20119 RingHom crh 20354 Fieldcfield 20615 LModclmod 20763 RSpancrsp 21114 ℤRHomczrh 21406 chrcchr 21408 ℤ/nℤczn 21409 AssAlgcasa 21757 algSccascl 21759 var₁cv1 22058 Poly₁cpl1 22059 eval₁ce1 22199 PrimRoots cprimroots 42064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088 ax-mulf 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-ofr 7614 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-tpos 8159 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-ec 8627 df-qs 8631 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-sup 9332 df-inf 9333 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-rp 12894 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-prm 16583 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-0g 17345 df-gsum 17346 df-prds 17351 df-pws 17353 df-imas 17412 df-qus 17413 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-mhm 18657 df-submnd 18658 df-grp 18815 df-minusg 18816 df-sbg 18817 df-mulg 18947 df-subg 19002 df-nsg 19003 df-eqg 19004 df-ghm 19092 df-cntz 19196 df-od 19407 df-cmn 19661 df-abl 19662 df-mgp 20026 df-rng 20038 df-ur 20067 df-srg 20072 df-ring 20120 df-cring 20121 df-oppr 20222 df-dvdsr 20242 df-rhm 20357 df-subrng 20431 df-subrg 20455 df-field 20617 df-lmod 20765 df-lss 20835 df-lsp 20875 df-sra 21077 df-rgmod 21078 df-lidl 21115 df-rsp 21116 df-2idl 21157 df-cnfld 21262 df-zring 21354 df-zrh 21410 df-chr 21412 df-zn 21413 df-assa 21760 df-asp 21761 df-ascl 21762 df-psr 21816 df-mvr 21817 df-mpl 21818 df-opsr 21820 df-evls 21979 df-evl 21980 df-psr1 22062 df-vr1 22063 df-ply1 22064 df-coe1 22065 df-evls1 22200 df-evl1 22201 df-primroots 42065

This theorem is referenced by: aks5lem3a 42162

W3C validator