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 42441

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 2736	. 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 20675	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
10		eqid 2736	. . . . . . . . 9 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
11	10	crngmgp 20176	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
12	9, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
13		aks5lem2.5	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ ℕ)
14	13	nnnn0d 12462	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
15		eqid 2736	. . . . . . 7 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
16	12, 14, 15	isprimroot 42347	. . . . . 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 2736	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
20	10, 19	mgpbas 20080	. . . . 5 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
21	20	eqcomi 2745	. . . 4 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
22	18, 21	eleqtrdi 2846	. . 3 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
23	2, 3, 4, 5, 6, 7, 22	aks5lem1 42440	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom 𝐾))
24		eqid 2736	. 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 12462	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
29		eqid 2736	. . . . 5 ⊢ (ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁)
30	29	zncrng 21499	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (ℤ/nℤ‘𝑁) ∈ CRing)
31	28, 30	syl 17	. . 3 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ CRing)
32		eqid 2736	. . . 4 ⊢ (Poly₁‘(ℤ/nℤ‘𝑁)) = (Poly₁‘(ℤ/nℤ‘𝑁))
33	32	ply1crng 22139	. . 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 20182	. . 3 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Grp)
37		eqid 2736	. . . . 5 ⊢ (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))
38		eqid 2736	. . . . 5 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))
39	37, 38	mgpbas 20080	. . . 4 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
40		eqid 2736	. . . 4 ⊢ (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
41	34	crngringd 20181	. . . . 5 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring)
42	37	ringmgp 20174	. . . . 5 ⊢ ((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
43	41, 42	syl 17	. . . 4 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
44	31	crngringd 20181	. . . . 5 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ Ring)
45		eqid 2736	. . . . . 6 ⊢ (var₁‘(ℤ/nℤ‘𝑁)) = (var₁‘(ℤ/nℤ‘𝑁))
46	45, 32, 38	vr1cl 22158	. . . . 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 19025	. . 3 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
49		eqid 2736	. . . . 5 ⊢ (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
50	38, 49	ringidcl 20200	. . . 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 2736	. . . 4 ⊢ (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))
53	38, 52	grpsubcl 18950	. . 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 6849	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) ∈ V)
56	55	mptexd 7170	. . . . . . . . 9 ⊢ (𝜑 → (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) ∈ V)
57	6, 56	eqeltrid 2840	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
58	57	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝐺 ∈ V)
59		vex 3444	. . . . . . . 8 ⊢ 𝑝 ∈ V
60	59	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝑝 ∈ V)
61	58, 60	coexd 7873	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → (𝐺 ∘ 𝑝) ∈ V)
62	61, 5	fmptd 7059	. . . . 5 ⊢ (𝜑 → 𝐹:(Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))⟶V)
63	62	ffund 6666	. . . 4 ⊢ (𝜑 → Fun 𝐹)
64	62	fdmd 6672	. . . . 5 ⊢ (𝜑 → dom 𝐹 = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
65	54, 64	eleqtrrd 2839	. . . 4 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹)
66		fvco 6932	. . . 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 2736	. . . . . . . 8 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
69	9	crngringd 20181	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Ring)
70	4	simp1d 1142	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
71		prmnn 16601	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
72	70, 71	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ ℕ)
73	3, 72	eqeltrrid 2841	. . . . . . . . . 10 ⊢ (𝜑 → (chr‘𝐾) ∈ ℕ)
74	73	nnzd 12514	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∈ ℤ)
75	4	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
76	3, 75	eqbrtrrid 5134	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∥ 𝑁)
77	69, 27, 74, 76, 29, 6	zndvdchrrhm 42226	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾))
78	32, 68, 38, 5, 77	rhmply1 22330	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)))
79		rhmghm 20419	. . . . . . 7 ⊢ (𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)) → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
80	78, 79	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
81		eqid 2736	. . . . . . 7 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
82	38, 52, 81	ghmsub 19153	. . . . . 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 6838	. . . 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 2736	. . . . . . . 8 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
86		eqid 2736	. . . . . . . 8 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
87	85, 68, 19, 86, 9, 22, 7	evl1maprhm 22323	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾))
88		rhmghm 20419	. . . . . . 7 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
89	87, 88	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
90	38, 86	rhmf 20420	. . . . . . . 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 7030	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
93	91, 51	ffvelcdmd 7030	. . . . . 6 ⊢ (𝜑 → (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
94		eqid 2736	. . . . . . 7 ⊢ (-_g‘𝐾) = (-_g‘𝐾)
95	86, 81, 94	ghmsub 19153	. . . . . 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 2736	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
98	38, 97, 49, 41, 48	ringlidmd 20207	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))
99	98	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
100	31	elexd 3464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ V)
101	32	ply1sca 22193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ/nℤ‘𝑁) ∈ V → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
103	102	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
104	103	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))))
105		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))
106		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))
107	32	ply1lmod 22192	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
108	44, 107	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
109	105, 106, 108, 41	ascl1 21841	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
110	104, 109	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
111	110	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))))
112	111	oveq1d 7373	. . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . 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 22140	. . . . . . . . . . . . . . . 16 ⊢ ((ℤ/nℤ‘𝑁) ∈ CRing → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
115	31, 114	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
116		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(ℤ/nℤ‘𝑁))
117		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(ℤ/nℤ‘𝑁))
118	116, 117	ringidcl 20200	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
119	44, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
120	102	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
121	119, 120	eleqtrd 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
122		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
123		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))
124	105, 106, 122, 38, 97, 123	asclmul1 21842	. . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
127	126	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))))
128		eqid 2736	. . . . . . . . . . . . 13 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
129		eqid 2736	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘(Poly₁‘𝐾)) = ( ·_𝑠 ‘(Poly₁‘𝐾))
130		eqid 2736	. . . . . . . . . . . . 13 ⊢ (mulGrp‘(Poly₁‘𝐾)) = (mulGrp‘(Poly₁‘𝐾))
131		eqid 2736	. . . . . . . . . . . . 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 22333	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
133	127, 132	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
134	133	fveq2d 6838	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
135		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝐾) = (1_r‘𝐾)
136	117, 135	rhm1 20424	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾) → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
137	77, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
138	137	oveq1d 7373	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
139	138	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
140	68	ply1assa 22140	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ AssAlg)
141	9, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ AssAlg)
142	19, 135	ringidcl 20200	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (1_r‘𝐾) ∈ (Base‘𝐾))
143	69, 142	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘𝐾))
144	68	ply1sca 22193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
145	2, 144	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
146	145	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘(Poly₁‘𝐾))))
147	143, 146	eleqtrd 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘(Scalar‘(Poly₁‘𝐾))))
148	130, 86	mgpbas 20080	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(mulGrp‘(Poly₁‘𝐾)))
149	68	ply1crng 22139	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
150	9, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ CRing)
151		crngring 20180	. . . . . . . . . . . . . . . . . 18 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Ring)
153	130	ringmgp 20174	. . . . . . . . . . . . . . . . 17 ⊢ ((Poly₁‘𝐾) ∈ Ring → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
154	152, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
155	128, 68, 86	vr1cl 22158	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
156	69, 155	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
157	148, 131, 154, 14, 156	mulgnn0cld 19025	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾)))
158		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
159		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘(Poly₁‘𝐾)) = (Scalar‘(Poly₁‘𝐾))
160		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘𝐾))) = (Base‘(Scalar‘(Poly₁‘𝐾)))
161		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (._r‘(Poly₁‘𝐾)) = (._r‘(Poly₁‘𝐾))
162	158, 159, 160, 86, 161, 129	asclmul1 21842	. . . . . . . . . . . . . . 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 2742	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
165	164	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
166		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘(Poly₁‘𝐾)) = (1_r‘(Poly₁‘𝐾))
167	68, 158, 135, 166, 69	ply1ascl1 22196	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾)) = (1_r‘(Poly₁‘𝐾)))
168	167	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
169	168	fveq2d 6838	. . . . . . . . . . . . 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 20207	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))
171	170	fveq2d 6838	. . . . . . . . . . . . . 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 6838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → ((eval₁‘𝐾)‘𝑟) = ((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
175	174	fveq1d 6836	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → (((eval₁‘𝐾)‘𝑟)‘𝑀) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
176		fvexd 6849	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) ∈ V)
177	172, 175, 157, 176	fvmptd 6948	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
178	85, 128, 19, 68, 86, 9, 22	evl1vard 22281	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(var₁‘𝐾))‘𝑀) = 𝑀))
179	85, 68, 19, 86, 9, 22, 178, 131, 15, 14	evl1expd 22289	. . . . . . . . . . . . . . . . 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 20118	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_r‘𝐾) = (0_g‘(mulGrp‘𝐾))
183	182	eqcomi 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾)
184	183	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾))
185	181, 184	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (1_r‘𝐾))
186	180, 185	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (1_r‘𝐾))
187	177, 186	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (1_r‘𝐾))
188	171, 187	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
189	169, 188	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
190	165, 189	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
191	139, 190	eqtrd 2771	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
192	134, 191	eqtrd 2771	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
193	166, 135	rhm1 20424	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
194	87, 193	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
195	194	eqcomd 2742	. . . . . . . . 9 ⊢ (𝜑 → (1_r‘𝐾) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
196	192, 195	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
197	196, 194	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
198	49, 166	rhm1 20424	. . . . . . . . . 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 6838	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
201	200, 194	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
202	197, 201	oveq12d 7376	. . . . . 6 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)))
203	69	ringgrpd 20177	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Grp)
204	19, 1, 94	grpsubid 18954	. . . . . . 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 2771	. . . . 5 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
207	96, 206	eqtrd 2771	. . . 4 ⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
208	84, 207	eqtrd 2771	. . 3 ⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
209	67, 208	eqtrd 2771	. 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 42439	1 ⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∀wral 3051 Vcvv 3440 {csn 4580 ∪ cuni 4863 class class class wbr 5098 ↦ cmpt 5179 ^◡ccnv 5623 dom cdm 5624 “ cima 5627 ∘ ccom 5628 Fun wfun 6486 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 [cec 8633 ℕcn 12145 ℕ₀cn0 12401 ∥ cdvds 16179 ℙcprime 16598 Basecbs 17136 ._rcmulr 17178 Scalarcsca 17180 ·_𝑠 cvsca 17181 0_gc0g 17359 /_s cqus 17426 Mndcmnd 18659 Grpcgrp 18863 -_gcsg 18865 ._gcmg 18997 ~_QG cqg 19052 GrpHom cghm 19141 CMndccmn 19709 mulGrpcmgp 20075 1_rcur 20116 Ringcrg 20168 CRingccrg 20169 RingHom crh 20405 Fieldcfield 20663 LModclmod 20811 RSpancrsp 21162 ℤRHomczrh 21454 chrcchr 21456 ℤ/nℤczn 21457 AssAlgcasa 21805 algSccascl 21807 var₁cv1 22116 Poly₁cpl1 22117 eval₁ce1 22258 PrimRoots cprimroots 42345

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-addf 11105 ax-mulf 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-ofr 7623 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-tpos 8168 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-ec 8637 df-qs 8641 df-map 8765 df-pm 8766 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-sup 9345 df-inf 9346 df-oi 9415 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-rp 12906 df-fz 13424 df-fzo 13571 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-dvds 16180 df-prm 16599 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-starv 17192 df-sca 17193 df-vsca 17194 df-ip 17195 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-hom 17201 df-cco 17202 df-0g 17361 df-gsum 17362 df-prds 17367 df-pws 17369 df-imas 17429 df-qus 17430 df-mre 17505 df-mrc 17506 df-acs 17508 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-mhm 18708 df-submnd 18709 df-grp 18866 df-minusg 18867 df-sbg 18868 df-mulg 18998 df-subg 19053 df-nsg 19054 df-eqg 19055 df-ghm 19142 df-cntz 19246 df-od 19457 df-cmn 19711 df-abl 19712 df-mgp 20076 df-rng 20088 df-ur 20117 df-srg 20122 df-ring 20170 df-cring 20171 df-oppr 20273 df-dvdsr 20293 df-rhm 20408 df-subrng 20479 df-subrg 20503 df-field 20665 df-lmod 20813 df-lss 20883 df-lsp 20923 df-sra 21125 df-rgmod 21126 df-lidl 21163 df-rsp 21164 df-2idl 21205 df-cnfld 21310 df-zring 21402 df-zrh 21458 df-chr 21460 df-zn 21461 df-assa 21808 df-asp 21809 df-ascl 21810 df-psr 21865 df-mvr 21866 df-mpl 21867 df-opsr 21869 df-evls 22029 df-evl 22030 df-psr1 22120 df-vr1 22121 df-ply1 22122 df-coe1 22123 df-evls1 22259 df-evl1 22260 df-primroots 42346

This theorem is referenced by: aks5lem3a 42443

W3C validator