Theorem ply1coe 22508

Description: Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 7-Oct-2019.)

Hypotheses

Ref	Expression
ply1coe.p	⊢ 𝑃 = (Poly1‘𝑅)
ply1coe.x	⊢ 𝑋 = (var1‘𝑅)
ply1coe.b	⊢ 𝐵 = (Base‘𝑃)
ply1coe.n	⊢ · = ( ·𝑠 ‘𝑃)
ply1coe.m	⊢ 𝑀 = (mulGrp‘𝑃)
ply1coe.e	⊢ ↑ = (.g‘𝑀)
ply1coe.a	⊢ 𝐴 = (coe1‘𝐾)

Assertion

Ref	Expression
ply1coe	⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘   𝑘,𝐾   𝑘,𝑋   ↑ ,𝑘   𝑅,𝑘   · ,𝑘   𝑃,𝑘

Allowed substitution hint:   𝑀(𝑘)

Proof of Theorem ply1coe

Dummy variables 𝑎 𝑏 𝑐 𝑥 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2765	. . 3 ⊢ (1o mPoly 𝑅) = (1o mPoly 𝑅)
2		psr1baslem 22395	. . 3 ⊢ (ℕ0 ↑m 1o) = {𝑑 ∈ (ℕ0 ↑m 1o) ∣ (◡𝑑 “ ℕ) ∈ Fin}
3		eqid 2765	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
4		eqid 2765	. . 3 ⊢ (1r‘𝑅) = (1r‘𝑅)
5		1onn 8632	. . . 4 ⊢ 1o ∈ ω
6	5	a1i 11	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 1o ∈ ω)
7		ply1coe.p	. . . 4 ⊢ 𝑃 = (Poly1‘𝑅)
8		ply1coe.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
9	7, 8	ply1bas 22405	. . 3 ⊢ 𝐵 = (Base‘(1o mPoly 𝑅))
10		ply1coe.n	. . . 4 ⊢ · = ( ·𝑠 ‘𝑃)
11	7, 1, 10	ply1vsca 22434	. . 3 ⊢ · = ( ·𝑠 ‘(1o mPoly 𝑅))
12		simpl 488	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑅 ∈ Ring)
13		simpr 490	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 ∈ 𝐵)
14	1, 2, 3, 4, 6, 9, 11, 12, 13	mplcoe1 22238	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))))))
15		ply1coe.a	. . . . . . 7 ⊢ 𝐴 = (coe1‘𝐾)
16	15	fvcoe1 22417	. . . . . 6 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅)))
17	16	adantll 727	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅)))
18	5	a1i 11	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → 1o ∈ ω)
19		eqid 2765	. . . . . . 7 ⊢ (mulGrp‘(1o mPoly 𝑅)) = (mulGrp‘(1o mPoly 𝑅))
20		eqid 2765	. . . . . . 7 ⊢ (.g‘(mulGrp‘(1o mPoly 𝑅))) = (.g‘(mulGrp‘(1o mPoly 𝑅)))
21		eqid 2765	. . . . . . 7 ⊢ (1o mVar 𝑅) = (1o mVar 𝑅)
22		simpll 779	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → 𝑅 ∈ Ring)
23		simpr 490	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → 𝑎 ∈ (ℕ0 ↑m 1o))
24		eqidd 2766	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
25		0ex 5272	. . . . . . . . . . 11 ⊢ ∅ ∈ V
26		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → ((1o mVar 𝑅)‘𝑏) = ((1o mVar 𝑅)‘∅))
27	26	oveq1d 7434	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
28	26	oveq2d 7435	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
29	27, 28	eqeq12d 2781	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → ((((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) ↔ (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅))))
30	25, 29	ralsn 4649	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) ↔ (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
31	24, 30	sylibr 237	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
32		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((1o mVar 𝑅)‘𝑥) = ((1o mVar 𝑅)‘∅))
33	32	oveq2d 7435	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
34	32	oveq1d 7434	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
35	33, 34	eqeq12d 2781	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) ↔ (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏))))
36	35	ralbidv 3190	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏))))
37	25, 36	ralsn 4649	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
38	31, 37	sylibr 237	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
39		df1o2 8466	. . . . . . . . 9 ⊢ 1o = {∅}
40	39	raleqi 3323	. . . . . . . . 9 ⊢ (∀𝑏 ∈ 1o (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
41	39, 40	raleqbii 3338	. . . . . . . 8 ⊢ (∀𝑥 ∈ 1o ∀𝑏 ∈ 1o (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) ↔ ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
42	38, 41	sylibr 237	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ∀𝑥 ∈ 1o ∀𝑏 ∈ 1o (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
43	1, 2, 3, 4, 18, 19, 20, 21, 22, 23, 42	mplcoe5 22241	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘(1o mPoly 𝑅)) Σg (𝑐 ∈ 1o ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)))))
44	39	mpteq1i 5204	. . . . . . . 8 ⊢ (𝑐 ∈ 1o ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐))) = (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)))
45	44	oveq2i 7430	. . . . . . 7 ⊢ ((mulGrp‘(1o mPoly 𝑅)) Σg (𝑐 ∈ 1o ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)))) = ((mulGrp‘(1o mPoly 𝑅)) Σg (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐))))
46	1	mplring 22218	. . . . . . . . . . 11 ⊢ ((1o ∈ ω ∧ 𝑅 ∈ Ring) → (1o mPoly 𝑅) ∈ Ring)
47	5, 46	mpan 703	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (1o mPoly 𝑅) ∈ Ring)
48	19	ringmgp 20365	. . . . . . . . . 10 ⊢ ((1o mPoly 𝑅) ∈ Ring → (mulGrp‘(1o mPoly 𝑅)) ∈ Mnd)
49	47, 48	syl 18	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (mulGrp‘(1o mPoly 𝑅)) ∈ Mnd)
50	49	ad2antrr 739	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (mulGrp‘(1o mPoly 𝑅)) ∈ Mnd)
51	25	a1i 11	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ∅ ∈ V)
52		ply1coe.e	. . . . . . . . . . . 12 ⊢ ↑ = (.g‘𝑀)
53	19, 9	mgpbas 20265	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘(mulGrp‘(1o mPoly 𝑅)))
54	53	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘(mulGrp‘(1o mPoly 𝑅))))
55		ply1coe.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (mulGrp‘𝑃)
56	55, 8	mgpbas 20265	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑀)
57	56	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘𝑀))
58		ssv 3962	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ V
59	58	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 ⊆ V)
60		ovexd 7454	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+g‘(mulGrp‘(1o mPoly 𝑅)))𝑏) ∈ V)
61		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘𝑃) = (.r‘𝑃)
62	7, 1, 61	ply1mulr 22435	. . . . . . . . . . . . . . . 16 ⊢ (.r‘𝑃) = (.r‘(1o mPoly 𝑅))
63	19, 62	mgpplusg 20264	. . . . . . . . . . . . . . 15 ⊢ (.r‘𝑃) = (+g‘(mulGrp‘(1o mPoly 𝑅)))
64	55, 61	mgpplusg 20264	. . . . . . . . . . . . . . 15 ⊢ (.r‘𝑃) = (+g‘𝑀)
65	63, 64	eqtr3i 2790	. . . . . . . . . . . . . 14 ⊢ (+g‘(mulGrp‘(1o mPoly 𝑅))) = (+g‘𝑀)
66	65	oveqi 7432	. . . . . . . . . . . . 13 ⊢ (𝑎(+g‘(mulGrp‘(1o mPoly 𝑅)))𝑏) = (𝑎(+g‘𝑀)𝑏)
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+g‘(mulGrp‘(1o mPoly 𝑅)))𝑏) = (𝑎(+g‘𝑀)𝑏))
68	20, 52, 54, 57, 59, 60, 67	mulgpropd 19226	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (.g‘(mulGrp‘(1o mPoly 𝑅))) = ↑ )
69	68	oveqd 7436	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
70	69	adantr 486	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
71	7	ply1ring 22457	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
72	55	ringmgp 20365	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd)
73	71, 72	syl 18	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
74	73	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → 𝑀 ∈ Mnd)
75		elmapi 8852	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (ℕ0 ↑m 1o) → 𝑎:1o⟶ℕ0)
76		0lt1o 8495	. . . . . . . . . . . 12 ⊢ ∅ ∈ 1o
77		ffvelcdm 7080	. . . . . . . . . . . 12 ⊢ ((𝑎:1o⟶ℕ0 ∧ ∅ ∈ 1o) → (𝑎‘∅) ∈ ℕ0)
78	75, 76, 77	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (ℕ0 ↑m 1o) → (𝑎‘∅) ∈ ℕ0)
79	78	adantl 487	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (𝑎‘∅) ∈ ℕ0)
80		ply1coe.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (var1‘𝑅)
81	80, 7, 8	vr1cl 22427	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
82	81	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → 𝑋 ∈ 𝐵)
83	56, 52, 74, 79, 82	mulgnn0cld 19205	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵)
84	70, 83	eqeltrd 2865	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋) ∈ 𝐵)
85		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (𝑎‘𝑐) = (𝑎‘∅))
86		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((1o mVar 𝑅)‘𝑐) = ((1o mVar 𝑅)‘∅))
87	80	vr1val 22402	. . . . . . . . . . 11 ⊢ 𝑋 = ((1o mVar 𝑅)‘∅)
88	86, 87	eqtr4di 2818	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → ((1o mVar 𝑅)‘𝑐) = 𝑋)
89	85, 88	oveq12d 7437	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)) = ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋))
90	53, 89	gsumsn 20068	. . . . . . . 8 ⊢ (((mulGrp‘(1o mPoly 𝑅)) ∈ Mnd ∧ ∅ ∈ V ∧ ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋) ∈ 𝐵) → ((mulGrp‘(1o mPoly 𝑅)) Σg (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋))
91	50, 51, 84, 90	syl3anc 1398	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((mulGrp‘(1o mPoly 𝑅)) Σg (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋))
92	45, 91	eqtrid 2812	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((mulGrp‘(1o mPoly 𝑅)) Σg (𝑐 ∈ 1o ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋))
93	43, 92, 70	3eqtrd 2804	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))) = ((𝑎‘∅) ↑ 𝑋))
94	17, 93	oveq12d 7437	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
95	94	mpteq2dva 5206	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))))) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
96	95	oveq2d 7435	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))))) = ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
97		nn0ex 12525	. . . . . 6 ⊢ ℕ0 ∈ V
98	97	mptex 7228	. . . . 5 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V
99	98	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V)
100	7	fvexi 6899	. . . . 5 ⊢ 𝑃 ∈ V
101	100	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑃 ∈ V)
102		ovexd 7454	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1o mPoly 𝑅) ∈ V)
103	8, 9	eqtr3i 2790	. . . . 5 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
104	103	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (Base‘𝑃) = (Base‘(1o mPoly 𝑅)))
105		eqid 2765	. . . . . 6 ⊢ (+g‘𝑃) = (+g‘𝑃)
106	7, 1, 105	ply1plusg 22433	. . . . 5 ⊢ (+g‘𝑃) = (+g‘(1o mPoly 𝑅))
107	106	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (+g‘𝑃) = (+g‘(1o mPoly 𝑅)))
108	99, 101, 102, 104, 107	gsumpropd 18768	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1o mPoly 𝑅) Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
109		eqid 2765	. . . . 5 ⊢ (0g‘𝑃) = (0g‘𝑃)
110	1, 7, 109	ply1mpl0 22466	. . . 4 ⊢ (0g‘𝑃) = (0g‘(1o mPoly 𝑅))
111	1	mpllmod 22217	. . . . . 6 ⊢ ((1o ∈ ω ∧ 𝑅 ∈ Ring) → (1o mPoly 𝑅) ∈ LMod)
112	5, 12, 111	sylancr 599	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1o mPoly 𝑅) ∈ LMod)
113		lmodcmn 21081	. . . . 5 ⊢ ((1o mPoly 𝑅) ∈ LMod → (1o mPoly 𝑅) ∈ CMnd)
114	112, 113	syl 18	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1o mPoly 𝑅) ∈ CMnd)
115	97	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ℕ0 ∈ V)
116	7	ply1lmod 22461	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
117	116	ad2antrr 739	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod)
118		eqid 2765	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
119	15, 8, 7, 118	coe1f 22421	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝐵 → 𝐴:ℕ0⟶(Base‘𝑅))
120	119	adantl 487	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴:ℕ0⟶(Base‘𝑅))
121	120	ffvelcdmda 7083	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑅))
122	7	ply1sca 22462	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
123	122	eqcomd 2771	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅)
124	123	ad2antrr 739	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (Scalar‘𝑃) = 𝑅)
125	124	fveq2d 6889	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
126	121, 125	eleqtrrd 2868	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
127	73	ad2antrr 739	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑀 ∈ Mnd)
128		simpr 490	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
129	81	ad2antrr 739	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ 𝐵)
130	56, 52, 127, 128, 129	mulgnn0cld 19205	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵)
131		eqid 2765	. . . . . . 7 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
132		eqid 2765	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
133	8, 131, 10, 132	lmodvscl 21049	. . . . . 6 ⊢ ((𝑃 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
134	117, 126, 130, 133	syl3anc 1398	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
135	134	fmpttd 7114	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))):ℕ0⟶𝐵)
136	7, 80, 8, 10, 55, 52, 15	ply1coefsupp 22507	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃))
137		eqid 2765	. . . . . 6 ⊢ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅))
138	39, 97, 25, 137	mapsnf1o2 8898	. . . . 5 ⊢ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)):(ℕ0 ↑m 1o)–1-1-onto→ℕ0
139	138	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)):(ℕ0 ↑m 1o)–1-1-onto→ℕ0)
140	9, 110, 114, 115, 135, 136, 139	gsumf1o 20030	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1o mPoly 𝑅) Σg ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)))))
141		eqidd 2766	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)))
142		eqidd 2766	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))
143		fveq2 6885	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝐴‘𝑘) = (𝐴‘(𝑎‘∅)))
144		oveq1 7426	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝑘 ↑ 𝑋) = ((𝑎‘∅) ↑ 𝑋))
145	143, 144	oveq12d 7437	. . . . 5 ⊢ (𝑘 = (𝑎‘∅) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
146	79, 141, 142, 145	fmptco 7129	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅))) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
147	146	oveq2d 7435	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)))) = ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
148	108, 140, 147	3eqtrrd 2805	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
149	14, 96, 148	3eqtrd 2804	1 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  Vcvv 3457   ⊆ wss 3906  ∅c0 4286  ifcif 4489  {csn 4591   ↦ cmpt 5194   ∘ ccom 5667  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7419  ωcom 7868  1_oc1o 8452   ↑_m cmap 8830  ℕ₀cn0 12519  Basecbs 17291  +_gcplusg 17332  ._rcmulr 17333  Scalarcsca 17335   ·_𝑠 cvsca 17336  0_gc0g 17514   Σ_g cgsu 17515  Mndcmnd 18824  ._gcmg 19177  CMndccmn 19894  mulGrpcmgp 20260  1_rcur 20307  Ringcrg 20359  LModclmod 21031   mVar cmvr 22105   mPoly cmpl 22106  var₁cv1 22386  Poly₁cpl1 22387  coe₁cco1 22388

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7684  df-ofr 7685  df-om 7869  df-1st 7992  df-2nd 7993  df-supp 8163  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-pm 8833  df-ixp 8902  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-fsupp 9329  df-sup 9409  df-oi 9479  df-card 9941  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-nn 12249  df-2 12318  df-3 12319  df-4 12320  df-5 12321  df-6 12322  df-7 12323  df-8 12324  df-9 12325  df-n0 12520  df-z 12607  df-dec 12728  df-uz 12879  df-fz 13552  df-fzo 13700  df-seq 14056  df-hash 14385  df-struct 17229  df-sets 17246  df-slot 17264  df-ndx 17276  df-base 17292  df-ress 17313  df-plusg 17345  df-mulr 17346  df-sca 17348  df-vsca 17349  df-ip 17350  df-tset 17351  df-ple 17352  df-ds 17354  df-hom 17356  df-cco 17357  df-0g 17516  df-gsum 17517  df-prds 17522  df-pws 17524  df-mre 17660  df-mrc 17661  df-acs 17663  df-mgm 18720  df-sgrp 18809  df-mnd 18825  df-mhm 18878  df-submnd 18879  df-grp 19047  df-minusg 19048  df-sbg 19049  df-mulg 19178  df-subg 19233  df-ghm 19328  df-cntz 19431  df-cmn 19896  df-abl 19897  df-mgp 20261  df-rng 20275  df-ur 20308  df-srg 20313  df-ring 20361  df-subrng 20695  df-subrg 20719  df-lmod 21033  df-lss 21103  df-psr 22109  df-mvr 22110  df-mpl 22111  df-opsr 22113  df-psr1 22390  df-vr1 22391  df-ply1 22392  df-coe1 22393

This theorem is used by:  eqcoe1ply1eq  22509  evls1fpws  22579  pmatcollpw1lem2  22982  mp2pm2mp  23018  plypf1  26420  ply1coedeg  33943  ply1degltdimlem  34076