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 42801

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 2762	. 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 20788	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
10		eqid 2762	. . . . . . . . 9 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
11	10	crngmgp 20287	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
12	9, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
13		aks5lem2.5	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ ℕ)
14	13	nnnn0d 12542	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
15		eqid 2762	. . . . . . 7 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
16	12, 14, 15	isprimroot 42707	. . . . . 6 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑙))))
17	8, 16	mpbid 234	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑙)))
18	17	simp1d 1155	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
19		eqid 2762	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
20	10, 19	mgpbas 20191	. . . . 5 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
21	20	eqcomi 2771	. . . 4 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
22	18, 21	eleqtrdi 2872	. . 3 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
23	2, 3, 4, 5, 6, 7, 22	aks5lem1 42800	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom 𝐾))
24		eqid 2762	. 2 ⊢ (^◡(𝐻 ∘ 𝐹) “ {(0_g‘𝐾)}) = (^◡(𝐻 ∘ 𝐹) “ {(0_g‘𝐾)})
25		aks5lem2.3	. 2 ⊢ 𝐴 = ((Poly₁‘(ℤ/nℤ‘𝑁)) /_s ((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿))
26		aks5lem2.2	. 2 ⊢ 𝐼 = (𝑠 ∈ (Base‘𝐴) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠))
27	4	simp2d 1156	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
28	27	nnnn0d 12542	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
29		eqid 2762	. . . . 5 ⊢ (ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁)
30	29	zncrng 21593	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (ℤ/nℤ‘𝑁) ∈ CRing)
31	28, 30	syl 17	. . 3 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ CRing)
32		eqid 2762	. . . 4 ⊢ (Poly₁‘(ℤ/nℤ‘𝑁)) = (Poly₁‘(ℤ/nℤ‘𝑁))
33	32	ply1crng 22257	. . 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 20293	. . 3 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Grp)
37		eqid 2762	. . . . 5 ⊢ (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))
38		eqid 2762	. . . . 5 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))
39	37, 38	mgpbas 20191	. . . 4 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
40		eqid 2762	. . . 4 ⊢ (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
41	34	crngringd 20292	. . . . 5 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring)
42	37	ringmgp 20285	. . . . 5 ⊢ ((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
43	41, 42	syl 17	. . . 4 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
44	31	crngringd 20292	. . . . 5 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ Ring)
45		eqid 2762	. . . . . 6 ⊢ (var₁‘(ℤ/nℤ‘𝑁)) = (var₁‘(ℤ/nℤ‘𝑁))
46	45, 32, 38	vr1cl 22276	. . . . 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 19137	. . 3 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
49		eqid 2762	. . . . 5 ⊢ (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
50	38, 49	ringidcl 20311	. . . 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 2762	. . . 4 ⊢ (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))
53	38, 52	grpsubcl 19062	. . 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 1390	. 2 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
55		fvexd 6882	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) ∈ V)
56	55	mptexd 7208	. . . . . . . . 9 ⊢ (𝜑 → (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) ∈ V)
57	6, 56	eqeltrid 2866	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
58	57	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝐺 ∈ V)
59		vex 3458	. . . . . . . 8 ⊢ 𝑝 ∈ V
60	59	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝑝 ∈ V)
61	58, 60	coexd 7912	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → (𝐺 ∘ 𝑝) ∈ V)
62	61, 5	fmptd 7095	. . . . 5 ⊢ (𝜑 → 𝐹:(Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))⟶V)
63	62	ffund 6696	. . . 4 ⊢ (𝜑 → Fun 𝐹)
64	62	fdmd 6702	. . . . 5 ⊢ (𝜑 → dom 𝐹 = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
65	54, 64	eleqtrrd 2865	. . . 4 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹)
66		fvco 6965	. . . 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 593	. . 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 2762	. . . . . . . 8 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
69	9	crngringd 20292	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Ring)
70	4	simp1d 1155	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
71		prmnn 16708	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
72	70, 71	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ ℕ)
73	3, 72	eqeltrrid 2867	. . . . . . . . . 10 ⊢ (𝜑 → (chr‘𝐾) ∈ ℕ)
74	73	nnzd 12594	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∈ ℤ)
75	4	simp3d 1157	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
76	3, 75	eqbrtrrid 5136	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∥ 𝑁)
77	69, 27, 74, 76, 29, 6	zndvdchrrhm 42587	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾))
78	32, 68, 38, 5, 77	rhmply1 22443	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)))
79		rhmghm 20528	. . . . . . 7 ⊢ (𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)) → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
80	78, 79	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
81		eqid 2762	. . . . . . 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 1390	. . . . 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 6871	. . . 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 2762	. . . . . . . 8 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
86		eqid 2762	. . . . . . . 8 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
87	85, 68, 19, 86, 9, 22, 7	evl1maprhm 22439	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾))
88		rhmghm 20528	. . . . . . 7 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
89	87, 88	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
90	38, 86	rhmf 20529	. . . . . . . 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 7066	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
93	91, 51	ffvelcdmd 7066	. . . . . 6 ⊢ (𝜑 → (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
94		eqid 2762	. . . . . . 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 1390	. . . . 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 2762	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
98	38, 97, 49, 41, 48	ringlidmd 20318	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))
99	98	eqcomd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
100	31	elexd 3477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ V)
101	32	ply1sca 22311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ/nℤ‘𝑁) ∈ V → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
103	102	fveq2d 6871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
104	103	fveq2d 6871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))))
105		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))
106		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))
107	32	ply1lmod 22310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
108	44, 107	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
109	105, 106, 108, 41	ascl1 21934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
110	104, 109	eqtrd 2797	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
111	110	eqcomd 2768	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))))
112	111	oveq1d 7411	. . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . 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 22258	. . . . . . . . . . . . . . . 16 ⊢ ((ℤ/nℤ‘𝑁) ∈ CRing → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
115	31, 114	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
116		eqid 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(ℤ/nℤ‘𝑁))
117		eqid 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(ℤ/nℤ‘𝑁))
118	116, 117	ringidcl 20311	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
119	44, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
120	102	fveq2d 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
121	119, 120	eleqtrd 2864	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
122		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
123		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))
124	105, 106, 122, 38, 97, 123	asclmul1 21935	. . . . . . . . . . . . . . 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 1390	. . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
127	126	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))))
128		eqid 2762	. . . . . . . . . . . . 13 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
129		eqid 2762	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘(Poly₁‘𝐾)) = ( ·_𝑠 ‘(Poly₁‘𝐾))
130		eqid 2762	. . . . . . . . . . . . 13 ⊢ (mulGrp‘(Poly₁‘𝐾)) = (mulGrp‘(Poly₁‘𝐾))
131		eqid 2762	. . . . . . . . . . . . 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 22446	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
133	127, 132	eqtrd 2797	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
134	133	fveq2d 6871	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
135		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝐾) = (1_r‘𝐾)
136	117, 135	rhm1 20534	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾) → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
137	77, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
138	137	oveq1d 7411	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
139	138	fveq2d 6871	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
140	68	ply1assa 22258	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ AssAlg)
141	9, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ AssAlg)
142	19, 135	ringidcl 20311	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (1_r‘𝐾) ∈ (Base‘𝐾))
143	69, 142	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘𝐾))
144	68	ply1sca 22311	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
145	2, 144	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
146	145	fveq2d 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘(Poly₁‘𝐾))))
147	143, 146	eleqtrd 2864	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘(Scalar‘(Poly₁‘𝐾))))
148	130, 86	mgpbas 20191	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(mulGrp‘(Poly₁‘𝐾)))
149	68	ply1crng 22257	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
150	9, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ CRing)
151		crngring 20291	. . . . . . . . . . . . . . . . . 18 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Ring)
153	130	ringmgp 20285	. . . . . . . . . . . . . . . . 17 ⊢ ((Poly₁‘𝐾) ∈ Ring → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
154	152, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
155	128, 68, 86	vr1cl 22276	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
156	69, 155	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
157	148, 131, 154, 14, 156	mulgnn0cld 19137	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾)))
158		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
159		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘(Poly₁‘𝐾)) = (Scalar‘(Poly₁‘𝐾))
160		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘𝐾))) = (Base‘(Scalar‘(Poly₁‘𝐾)))
161		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (._r‘(Poly₁‘𝐾)) = (._r‘(Poly₁‘𝐾))
162	158, 159, 160, 86, 161, 129	asclmul1 21935	. . . . . . . . . . . . . . 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 1390	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
164	163	eqcomd 2768	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
165	164	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
166		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘(Poly₁‘𝐾)) = (1_r‘(Poly₁‘𝐾))
167	68, 158, 135, 166, 69	ply1ascl1 22314	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾)) = (1_r‘(Poly₁‘𝐾)))
168	167	oveq1d 7411	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
169	168	fveq2d 6871	. . . . . . . . . . . . 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 20318	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))
171	170	fveq2d 6871	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
172	7	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐻 = (𝑟 ∈ (Base‘(Poly₁‘𝐾)) ↦ (((eval₁‘𝐾)‘𝑟)‘𝑀)))
173		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))
174	173	fveq2d 6871	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → ((eval₁‘𝐾)‘𝑟) = ((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
175	174	fveq1d 6869	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → (((eval₁‘𝐾)‘𝑟)‘𝑀) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
176		fvexd 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) ∈ V)
177	172, 175, 157, 176	fvmptd 6983	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
178	85, 128, 19, 68, 86, 9, 22	evl1vard 22397	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(var₁‘𝐾))‘𝑀) = 𝑀))
179	85, 68, 19, 86, 9, 22, 178, 131, 15, 14	evl1expd 22405	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (𝑅(._g‘(mulGrp‘𝐾))𝑀)))
180	179	simprd 499	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (𝑅(._g‘(mulGrp‘𝐾))𝑀))
181	17	simp2d 1156	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)))
182	10, 135	ringidval 20229	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_r‘𝐾) = (0_g‘(mulGrp‘𝐾))
183	182	eqcomi 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾)
184	183	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾))
185	181, 184	eqtrd 2797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (1_r‘𝐾))
186	180, 185	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (1_r‘𝐾))
187	177, 186	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (1_r‘𝐾))
188	171, 187	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
189	169, 188	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
190	165, 189	eqtrd 2797	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
191	139, 190	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
192	134, 191	eqtrd 2797	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
193	166, 135	rhm1 20534	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
194	87, 193	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
195	194	eqcomd 2768	. . . . . . . . 9 ⊢ (𝜑 → (1_r‘𝐾) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
196	192, 195	eqtrd 2797	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
197	196, 194	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
198	49, 166	rhm1 20534	. . . . . . . . . 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 6871	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
201	200, 194	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
202	197, 201	oveq12d 7414	. . . . . 6 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)))
203	69	ringgrpd 20288	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Grp)
204	19, 1, 94	grpsubid 19066	. . . . . . 7 ⊢ ((𝐾 ∈ Grp ∧ (1_r‘𝐾) ∈ (Base‘𝐾)) → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
205	203, 143, 204	syl2anc 593	. . . . . 6 ⊢ (𝜑 → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
206	202, 205	eqtrd 2797	. . . . 5 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
207	96, 206	eqtrd 2797	. . . 4 ⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
208	84, 207	eqtrd 2797	. . 3 ⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
209	67, 208	eqtrd 2797	. 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 42799	1 ⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 ∀wral 3076 Vcvv 3454 {csn 4582 ∪ cuni 4865 class class class wbr 5100 ↦ cmpt 5181 ^◡ccnv 5646 dom cdm 5647 “ cima 5650 ∘ ccom 5651 Fun wfun 6515 ⟶wf 6517 ‘cfv 6521 (class class class)co 7396 [cec 8676 ℕcn 12210 ℕ₀cn0 12481 ∥ cdvds 16286 ℙcprime 16705 Basecbs 17245 ._rcmulr 17287 Scalarcsca 17289 ·_𝑠 cvsca 17290 0_gc0g 17468 /_s cqus 17535 Mndcmnd 18768 Grpcgrp 18975 -_gcsg 18977 ._gcmg 19109 ~_QG cqg 19164 GrpHom cghm 19253 CMndccmn 19820 mulGrpcmgp 20186 1_rcur 20227 Ringcrg 20279 CRingccrg 20280 RingHom crh 20514 Fieldcfield 20776 LModclmod 20924 RSpancrsp 21274 ℤRHomczrh 21548 chrcchr 21550 ℤ/nℤczn 21551 AssAlgcasa 21899 algSccascl 21901 var₁cv1 22235 Poly₁cpl1 22236 eval₁ce1 22374 PrimRoots cprimroots 42705

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151 ax-addf 11152 ax-mulf 11153

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-ofr 7661 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-tpos 8206 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8678 df-ec 8680 df-qs 8684 df-map 8810 df-pm 8811 df-ixp 8880 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-sup 9388 df-inf 9389 df-oi 9458 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-rp 12994 df-fz 13513 df-fzo 13660 df-fl 13802 df-mod 13880 df-seq 14015 df-exp 14075 df-hash 14344 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-dvds 16287 df-prm 16706 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-starv 17301 df-sca 17302 df-vsca 17303 df-ip 17304 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-hom 17310 df-cco 17311 df-0g 17470 df-gsum 17471 df-prds 17476 df-pws 17478 df-imas 17538 df-qus 17539 df-mre 17614 df-mrc 17615 df-acs 17617 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-mhm 18817 df-submnd 18818 df-grp 18978 df-minusg 18979 df-sbg 18980 df-mulg 19110 df-subg 19165 df-nsg 19166 df-eqg 19167 df-ghm 19254 df-cntz 19357 df-od 19568 df-cmn 19822 df-abl 19823 df-mgp 20187 df-rng 20199 df-ur 20228 df-srg 20233 df-ring 20281 df-cring 20282 df-oppr 20382 df-dvdsr 20402 df-rhm 20517 df-subrng 20592 df-subrg 20616 df-field 20778 df-lmod 20926 df-lss 20996 df-lsp 21036 df-sra 21237 df-rgmod 21238 df-lidl 21275 df-rsp 21276 df-2idl 21317 df-cnfld 21422 df-zring 21496 df-zrh 21552 df-chr 21554 df-zn 21555 df-assa 21902 df-asp 21903 df-ascl 21904 df-psr 21958 df-mvr 21959 df-mpl 21960 df-opsr 21962 df-evls 22124 df-evl 22125 df-psr1 22239 df-vr1 22240 df-ply1 22241 df-coe1 22242 df-evls1 22375 df-evl1 22376 df-primroots 42706

This theorem is referenced by: aks5lem3a 42803

W3C validator