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 42643

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 2737	. 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 20713	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
10		eqid 2737	. . . . . . . . 9 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
11	10	crngmgp 20216	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
12	9, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
13		aks5lem2.5	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ ℕ)
14	13	nnnn0d 12492	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
15		eqid 2737	. . . . . . 7 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
16	12, 14, 15	isprimroot 42549	. . . . . 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 1143	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
19		eqid 2737	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
20	10, 19	mgpbas 20120	. . . . 5 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
21	20	eqcomi 2746	. . . 4 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
22	18, 21	eleqtrdi 2847	. . 3 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
23	2, 3, 4, 5, 6, 7, 22	aks5lem1 42642	. 2 ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom 𝐾))
24		eqid 2737	. 2 ⊢ (^◡(𝐻 ∘ 𝐹) “ {(0_g‘𝐾)}) = (^◡(𝐻 ∘ 𝐹) “ {(0_g‘𝐾)})
25		aks5lem2.3	. 2 ⊢ 𝐴 = ((Poly₁‘(ℤ/nℤ‘𝑁)) /_s ((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿))
26		aks5lem2.2	. 2 ⊢ 𝐼 = (𝑠 ∈ (Base‘𝐴) ↦ ∪ ((𝐻 ∘ 𝐹) “ 𝑠))
27	4	simp2d 1144	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
28	27	nnnn0d 12492	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
29		eqid 2737	. . . . 5 ⊢ (ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁)
30	29	zncrng 21537	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (ℤ/nℤ‘𝑁) ∈ CRing)
31	28, 30	syl 17	. . 3 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ CRing)
32		eqid 2737	. . . 4 ⊢ (Poly₁‘(ℤ/nℤ‘𝑁)) = (Poly₁‘(ℤ/nℤ‘𝑁))
33	32	ply1crng 22175	. . 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 20222	. . 3 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Grp)
37		eqid 2737	. . . . 5 ⊢ (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))
38		eqid 2737	. . . . 5 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))
39	37, 38	mgpbas 20120	. . . 4 ⊢ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Base‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
40		eqid 2737	. . . 4 ⊢ (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))
41	34	crngringd 20221	. . . . 5 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring)
42	37	ringmgp 20214	. . . . 5 ⊢ ((Poly₁‘(ℤ/nℤ‘𝑁)) ∈ Ring → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
43	41, 42	syl 17	. . . 4 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))) ∈ Mnd)
44	31	crngringd 20221	. . . . 5 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ Ring)
45		eqid 2737	. . . . . 6 ⊢ (var₁‘(ℤ/nℤ‘𝑁)) = (var₁‘(ℤ/nℤ‘𝑁))
46	45, 32, 38	vr1cl 22194	. . . . 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 19065	. . 3 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
49		eqid 2737	. . . . 5 ⊢ (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
50	38, 49	ringidcl 20240	. . . 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 2737	. . . 4 ⊢ (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))
53	38, 52	grpsubcl 18990	. . 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 1374	. 2 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
55		fvexd 6850	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) ∈ V)
56	55	mptexd 7173	. . . . . . . . 9 ⊢ (𝜑 → (𝑞 ∈ (Base‘(ℤ/nℤ‘𝑁)) ↦ ∪ ((ℤRHom‘𝐾) “ 𝑞)) ∈ V)
57	6, 56	eqeltrid 2841	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ V)
58	57	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝐺 ∈ V)
59		vex 3434	. . . . . . . 8 ⊢ 𝑝 ∈ V
60	59	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → 𝑝 ∈ V)
61	58, 60	coexd 7876	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))) → (𝐺 ∘ 𝑝) ∈ V)
62	61, 5	fmptd 7061	. . . . 5 ⊢ (𝜑 → 𝐹:(Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))⟶V)
63	62	ffund 6667	. . . 4 ⊢ (𝜑 → Fun 𝐹)
64	62	fdmd 6673	. . . . 5 ⊢ (𝜑 → dom 𝐹 = (Base‘(Poly₁‘(ℤ/nℤ‘𝑁))))
65	54, 64	eleqtrrd 2840	. . . 4 ⊢ (𝜑 → ((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹)
66		fvco 6933	. . . 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 585	. . 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 2737	. . . . . . . 8 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
69	9	crngringd 20221	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Ring)
70	4	simp1d 1143	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
71		prmnn 16637	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
72	70, 71	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ ℕ)
73	3, 72	eqeltrrid 2842	. . . . . . . . . 10 ⊢ (𝜑 → (chr‘𝐾) ∈ ℕ)
74	73	nnzd 12544	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∈ ℤ)
75	4	simp3d 1145	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
76	3, 75	eqbrtrrid 5122	. . . . . . . . 9 ⊢ (𝜑 → (chr‘𝐾) ∥ 𝑁)
77	69, 27, 74, 76, 29, 6	zndvdchrrhm 42429	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾))
78	32, 68, 38, 5, 77	rhmply1 22364	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)))
79		rhmghm 20457	. . . . . . 7 ⊢ (𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) RingHom (Poly₁‘𝐾)) → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
80	78, 79	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ ((Poly₁‘(ℤ/nℤ‘𝑁)) GrpHom (Poly₁‘𝐾)))
81		eqid 2737	. . . . . . 7 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
82	38, 52, 81	ghmsub 19193	. . . . . 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 1374	. . . . 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 6839	. . . 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 2737	. . . . . . . 8 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
86		eqid 2737	. . . . . . . 8 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
87	85, 68, 19, 86, 9, 22, 7	evl1maprhm 22357	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾))
88		rhmghm 20457	. . . . . . 7 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
89	87, 88	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ ((Poly₁‘𝐾) GrpHom 𝐾))
90	38, 86	rhmf 20458	. . . . . . . 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 7032	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
93	91, 51	ffvelcdmd 7032	. . . . . 6 ⊢ (𝜑 → (𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly₁‘𝐾)))
94		eqid 2737	. . . . . . 7 ⊢ (-_g‘𝐾) = (-_g‘𝐾)
95	86, 81, 94	ghmsub 19193	. . . . . 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 1374	. . . . 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 2737	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))
98	38, 97, 49, 41, 48	ringlidmd 20247	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))
99	98	eqcomd 2743	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(._r‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
100	31	elexd 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) ∈ V)
101	32	ply1sca 22229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ/nℤ‘𝑁) ∈ V → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ/nℤ‘𝑁) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
103	102	fveq2d 6839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
104	103	fveq2d 6839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))))
105		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))
106		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))) = (Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))
107	32	ply1lmod 22228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
108	44, 107	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ LMod)
109	105, 106, 108, 41	ascl1 21878	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
110	104, 109	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))
111	110	eqcomd 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ((algSc‘(Poly₁‘(ℤ/nℤ‘𝑁)))‘(1_r‘(ℤ/nℤ‘𝑁))))
112	111	oveq1d 7376	. . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . 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 22176	. . . . . . . . . . . . . . . 16 ⊢ ((ℤ/nℤ‘𝑁) ∈ CRing → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
115	31, 114	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘(ℤ/nℤ‘𝑁)) ∈ AssAlg)
116		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(ℤ/nℤ‘𝑁))
117		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘(ℤ/nℤ‘𝑁)) = (1_r‘(ℤ/nℤ‘𝑁))
118	116, 117	ringidcl 20240	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
119	44, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)))
120	102	fveq2d 6839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
121	119, 120	eleqtrd 2839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))))
122		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁)))) = (Base‘(Scalar‘(Poly₁‘(ℤ/nℤ‘𝑁))))
123		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁))) = ( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))
124	105, 106, 122, 38, 97, 123	asclmul1 21879	. . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))) = ((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))
127	126	fveq2d 6839	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))))
128		eqid 2737	. . . . . . . . . . . . 13 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
129		eqid 2737	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠 ‘(Poly₁‘𝐾)) = ( ·_𝑠 ‘(Poly₁‘𝐾))
130		eqid 2737	. . . . . . . . . . . . 13 ⊢ (mulGrp‘(Poly₁‘𝐾)) = (mulGrp‘(Poly₁‘𝐾))
131		eqid 2737	. . . . . . . . . . . . 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 22367	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘((1_r‘(ℤ/nℤ‘𝑁))( ·_𝑠 ‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
133	127, 132	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))) = ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
134	133	fveq2d 6839	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
135		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (1_r‘𝐾) = (1_r‘𝐾)
136	117, 135	rhm1 20462	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ ((ℤ/nℤ‘𝑁) RingHom 𝐾) → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
137	77, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(1_r‘(ℤ/nℤ‘𝑁))) = (1_r‘𝐾))
138	137	oveq1d 7376	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
139	138	fveq2d 6839	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
140	68	ply1assa 22176	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ AssAlg)
141	9, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ AssAlg)
142	19, 135	ringidcl 20240	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (1_r‘𝐾) ∈ (Base‘𝐾))
143	69, 142	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘𝐾))
144	68	ply1sca 22229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
145	2, 144	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 = (Scalar‘(Poly₁‘𝐾)))
146	145	fveq2d 6839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘(Poly₁‘𝐾))))
147	143, 146	eleqtrd 2839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1_r‘𝐾) ∈ (Base‘(Scalar‘(Poly₁‘𝐾))))
148	130, 86	mgpbas 20120	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(mulGrp‘(Poly₁‘𝐾)))
149	68	ply1crng 22175	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
150	9, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ CRing)
151		crngring 20220	. . . . . . . . . . . . . . . . . 18 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Ring)
153	130	ringmgp 20214	. . . . . . . . . . . . . . . . 17 ⊢ ((Poly₁‘𝐾) ∈ Ring → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
154	152, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘(Poly₁‘𝐾)) ∈ Mnd)
155	128, 68, 86	vr1cl 22194	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
156	69, 155	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)))
157	148, 131, 154, 14, 156	mulgnn0cld 19065	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)) ∈ (Base‘(Poly₁‘𝐾)))
158		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
159		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘(Poly₁‘𝐾)) = (Scalar‘(Poly₁‘𝐾))
160		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Scalar‘(Poly₁‘𝐾))) = (Base‘(Scalar‘(Poly₁‘𝐾)))
161		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (._r‘(Poly₁‘𝐾)) = (._r‘(Poly₁‘𝐾))
162	158, 159, 160, 86, 161, 129	asclmul1 21879	. . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
164	163	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
165	164	fveq2d 6839	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))))
166		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘(Poly₁‘𝐾)) = (1_r‘(Poly₁‘𝐾))
167	68, 158, 135, 166, 69	ply1ascl1 22232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾)) = (1_r‘(Poly₁‘𝐾)))
168	167	oveq1d 7376	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
169	168	fveq2d 6839	. . . . . . . . . . . . 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 20247	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))
171	170	fveq2d 6839	. . . . . . . . . . . . . 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 6839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → ((eval₁‘𝐾)‘𝑟) = ((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))))
175	174	fveq1d 6837	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 = (𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) → (((eval₁‘𝐾)‘𝑟)‘𝑀) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
176		fvexd 6850	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) ∈ V)
177	172, 175, 157, 176	fvmptd 6950	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀))
178	85, 128, 19, 68, 86, 9, 22	evl1vard 22315	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((var₁‘𝐾) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(var₁‘𝐾))‘𝑀) = 𝑀))
179	85, 68, 19, 86, 9, 22, 178, 131, 15, 14	evl1expd 22323	. . . . . . . . . . . . . . . . 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 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)))
182	10, 135	ringidval 20158	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_r‘𝐾) = (0_g‘(mulGrp‘𝐾))
183	182	eqcomi 2746	. . . . . . . . . . . . . . . . . 18 ⊢ (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾)
184	183	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0_g‘(mulGrp‘𝐾)) = (1_r‘𝐾))
185	181, 184	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (1_r‘𝐾))
186	180, 185	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))‘𝑀) = (1_r‘𝐾))
187	177, 186	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾))) = (1_r‘𝐾))
188	171, 187	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘((1_r‘(Poly₁‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
189	169, 188	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻‘(((algSc‘(Poly₁‘𝐾))‘(1_r‘𝐾))(._r‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
190	165, 189	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘((1_r‘𝐾)( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
191	139, 190	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘((𝐺‘(1_r‘(ℤ/nℤ‘𝑁)))( ·_𝑠 ‘(Poly₁‘𝐾))(𝑅(._g‘(mulGrp‘(Poly₁‘𝐾)))(var₁‘𝐾)))) = (1_r‘𝐾))
192	134, 191	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
193	166, 135	rhm1 20462	. . . . . . . . . . 11 ⊢ (𝐻 ∈ ((Poly₁‘𝐾) RingHom 𝐾) → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
194	87, 193	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(1_r‘(Poly₁‘𝐾))) = (1_r‘𝐾))
195	194	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → (1_r‘𝐾) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
196	192, 195	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
197	196, 194	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
198	49, 166	rhm1 20462	. . . . . . . . . 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 6839	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1_r‘(Poly₁‘𝐾))))
201	200, 194	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁))))) = (1_r‘𝐾))
202	197, 201	oveq12d 7379	. . . . . 6 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)))
203	69	ringgrpd 20217	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Grp)
204	19, 1, 94	grpsubid 18994	. . . . . . 7 ⊢ ((𝐾 ∈ Grp ∧ (1_r‘𝐾) ∈ (Base‘𝐾)) → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
205	203, 143, 204	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ((1_r‘𝐾)(-_g‘𝐾)(1_r‘𝐾)) = (0_g‘𝐾))
206	202, 205	eqtrd 2772	. . . . 5 ⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))))(-_g‘𝐾)(𝐻‘(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
207	96, 206	eqtrd 2772	. . . 4 ⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁))))(-_g‘(Poly₁‘𝐾))(𝐹‘(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
208	84, 207	eqtrd 2772	. . 3 ⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(._g‘(mulGrp‘(Poly₁‘(ℤ/nℤ‘𝑁))))(var₁‘(ℤ/nℤ‘𝑁)))(-_g‘(Poly₁‘(ℤ/nℤ‘𝑁)))(1_r‘(Poly₁‘(ℤ/nℤ‘𝑁)))))) = (0_g‘𝐾))
209	67, 208	eqtrd 2772	. 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 42641	1 ⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈ (Base‘(Poly₁‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly₁‘(ℤ/nℤ‘𝑁)) ~_QG 𝐿)) = ((𝐻 ∘ 𝐹)‘𝑔)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 Vcvv 3430 {csn 4568 ∪ cuni 4851 class class class wbr 5086 ↦ cmpt 5167 ^◡ccnv 5624 dom cdm 5625 “ cima 5628 ∘ ccom 5629 Fun wfun 6487 ⟶wf 6489 ‘cfv 6493 (class class class)co 7361 [cec 8635 ℕcn 12168 ℕ₀cn0 12431 ∥ cdvds 16215 ℙcprime 16634 Basecbs 17173 ._rcmulr 17215 Scalarcsca 17217 ·_𝑠 cvsca 17218 0_gc0g 17396 /_s cqus 17463 Mndcmnd 18696 Grpcgrp 18903 -_gcsg 18905 ._gcmg 19037 ~_QG cqg 19092 GrpHom cghm 19181 CMndccmn 19749 mulGrpcmgp 20115 1_rcur 20156 Ringcrg 20208 CRingccrg 20209 RingHom crh 20443 Fieldcfield 20701 LModclmod 20849 RSpancrsp 21200 ℤRHomczrh 21492 chrcchr 21494 ℤ/nℤczn 21495 AssAlgcasa 21843 algSccascl 21845 var₁cv1 22152 Poly₁cpl1 22153 eval₁ce1 22292 PrimRoots cprimroots 42547

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110 ax-addf 11111 ax-mulf 11112

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-ofr 7626 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8105 df-tpos 8170 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-er 8637 df-ec 8639 df-qs 8643 df-map 8769 df-pm 8770 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-sup 9349 df-inf 9350 df-oi 9419 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-z 12519 df-dec 12639 df-uz 12783 df-rp 12937 df-fz 13456 df-fzo 13603 df-fl 13745 df-mod 13823 df-seq 13958 df-exp 14018 df-hash 14287 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-dvds 16216 df-prm 16635 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-starv 17229 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-unif 17237 df-hom 17238 df-cco 17239 df-0g 17398 df-gsum 17399 df-prds 17404 df-pws 17406 df-imas 17466 df-qus 17467 df-mre 17542 df-mrc 17543 df-acs 17545 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-mhm 18745 df-submnd 18746 df-grp 18906 df-minusg 18907 df-sbg 18908 df-mulg 19038 df-subg 19093 df-nsg 19094 df-eqg 19095 df-ghm 19182 df-cntz 19286 df-od 19497 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-srg 20162 df-ring 20210 df-cring 20211 df-oppr 20311 df-dvdsr 20331 df-rhm 20446 df-subrng 20517 df-subrg 20541 df-field 20703 df-lmod 20851 df-lss 20921 df-lsp 20961 df-sra 21163 df-rgmod 21164 df-lidl 21201 df-rsp 21202 df-2idl 21243 df-cnfld 21348 df-zring 21440 df-zrh 21496 df-chr 21498 df-zn 21499 df-assa 21846 df-asp 21847 df-ascl 21848 df-psr 21902 df-mvr 21903 df-mpl 21904 df-opsr 21906 df-evls 22065 df-evl 22066 df-psr1 22156 df-vr1 22157 df-ply1 22158 df-coe1 22159 df-evls1 22293 df-evl1 22294 df-primroots 42548

This theorem is referenced by: aks5lem3a 42645

W3C validator