Theorem ply1coe 22609

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 2761	. . 3 ⊢ (1o mPoly 𝑅) = (1o mPoly 𝑅)
2		psr1baslem 22496	. . 3 ⊢ (ℕ0 ↑m 1o) = {𝑑 ∈ (ℕ0 ↑m 1o) ∣ (◡𝑑 “ ℕ) ∈ Fin}
3		eqid 2761	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
4		eqid 2761	. . 3 ⊢ (1r‘𝑅) = (1r‘𝑅)
5		1onn 8642	. . . 4 ⊢ 1o ∈ ω
6	5	a1i 11	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 1o ∈ ω)
7		ply1coe.p	. . . 4 ⊢ 𝑃 = (Poly1‘𝑅)
8		ply1coe.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
9	7, 8	ply1bas 22506	. . 3 ⊢ 𝐵 = (Base‘(1o mPoly 𝑅))
10		ply1coe.n	. . . 4 ⊢ · = ( ·𝑠 ‘𝑃)
11	7, 1, 10	ply1vsca 22535	. . 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 22339	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))))))
15		ply1coe.a	. . . . . . 7 ⊢ 𝐴 = (coe1‘𝐾)
16	15	fvcoe1 22518	. . . . . 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 2761	. . . . . . 7 ⊢ (mulGrp‘(1o mPoly 𝑅)) = (mulGrp‘(1o mPoly 𝑅))
20		eqid 2761	. . . . . . 7 ⊢ (.g‘(mulGrp‘(1o mPoly 𝑅))) = (.g‘(mulGrp‘(1o mPoly 𝑅)))
21		eqid 2761	. . . . . . 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 2762	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
25		0ex 5261	. . . . . . . . . . 11 ⊢ ∅ ∈ V
26		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → ((1o mVar 𝑅)‘𝑏) = ((1o mVar 𝑅)‘∅))
27	26	oveq1d 7433	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
28	26	oveq2d 7434	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
29	27, 28	eqeq12d 2777	. . . . . . . . . . 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 4642	. . . . . . . . . 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 6883	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((1o mVar 𝑅)‘𝑥) = ((1o mVar 𝑅)‘∅))
33	32	oveq2d 7434	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑥)) = (((1o mVar 𝑅)‘𝑏)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘∅)))
34	32	oveq1d 7433	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1o mVar 𝑅)‘𝑥)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)) = (((1o mVar 𝑅)‘∅)(+g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑏)))
35	33, 34	eqeq12d 2777	. . . . . . . . . . 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 3186	. . . . . . . . . 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 4642	. . . . . . . . 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 8476	. . . . . . . . 9 ⊢ 1o = {∅}
40	39	raleqi 3318	. . . . . . . . 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 3333	. . . . . . . 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 22342	. . . . . 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 5196	. . . . . . . 8 ⊢ (𝑐 ∈ 1o ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐))) = (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)))
45	44	oveq2i 7429	. . . . . . 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 22319	. . . . . . . . . . 11 ⊢ ((1o ∈ ω ∧ 𝑅 ∈ Ring) → (1o mPoly 𝑅) ∈ Ring)
47	5, 46	mpan 703	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (1o mPoly 𝑅) ∈ Ring)
48	19	ringmgp 20458	. . . . . . . . . 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 20358	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘(mulGrp‘(1o mPoly 𝑅)))
54	53	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘(mulGrp‘(1o mPoly 𝑅))))
55		ply1coe.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (mulGrp‘𝑃)
56	55, 8	mgpbas 20358	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑀)
57	56	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘𝑀))
58		ssv 3955	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ V
59	58	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 ⊆ V)
60		ovexd 7453	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+g‘(mulGrp‘(1o mPoly 𝑅)))𝑏) ∈ V)
61		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (.r‘𝑃) = (.r‘𝑃)
62	7, 1, 61	ply1mulr 22536	. . . . . . . . . . . . . . . 16 ⊢ (.r‘𝑃) = (.r‘(1o mPoly 𝑅))
63	19, 62	mgpplusg 20357	. . . . . . . . . . . . . . 15 ⊢ (.r‘𝑃) = (+g‘(mulGrp‘(1o mPoly 𝑅)))
64	55, 61	mgpplusg 20357	. . . . . . . . . . . . . . 15 ⊢ (.r‘𝑃) = (+g‘𝑀)
65	63, 64	eqtr3i 2786	. . . . . . . . . . . . . 14 ⊢ (+g‘(mulGrp‘(1o mPoly 𝑅))) = (+g‘𝑀)
66	65	oveqi 7431	. . . . . . . . . . . . 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 19319	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (.g‘(mulGrp‘(1o mPoly 𝑅))) = ↑ )
69	68	oveqd 7435	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
70	69	adantr 486	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
71	7	ply1ring 22558	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
72	55	ringmgp 20458	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd)
73	71, 72	syl 18	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
74	73	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → 𝑀 ∈ Mnd)
75		elmapi 8862	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (ℕ0 ↑m 1o) → 𝑎:1o⟶ℕ0)
76		0lt1o 8505	. . . . . . . . . . . 12 ⊢ ∅ ∈ 1o
77		ffvelcdm 7079	. . . . . . . . . . . 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 22528	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
82	81	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → 𝑋 ∈ 𝐵)
83	56, 52, 74, 79, 82	mulgnn0cld 19298	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵)
84	70, 83	eqeltrd 2861	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋) ∈ 𝐵)
85		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (𝑎‘𝑐) = (𝑎‘∅))
86		fveq2 6883	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((1o mVar 𝑅)‘𝑐) = ((1o mVar 𝑅)‘∅))
87	80	vr1val 22503	. . . . . . . . . . 11 ⊢ 𝑋 = ((1o mVar 𝑅)‘∅)
88	86, 87	eqtr4di 2814	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → ((1o mVar 𝑅)‘𝑐) = 𝑋)
89	85, 88	oveq12d 7436	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑎‘𝑐)(.g‘(mulGrp‘(1o mPoly 𝑅)))((1o mVar 𝑅)‘𝑐)) = ((𝑎‘∅)(.g‘(mulGrp‘(1o mPoly 𝑅)))𝑋))
90	53, 89	gsumsn 20161	. . . . . . . 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 2808	. . . . . 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 2800	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))) = ((𝑎‘∅) ↑ 𝑋))
94	17, 93	oveq12d 7436	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ↑m 1o)) → ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
95	94	mpteq2dva 5198	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅))))) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
96	95	oveq2d 7434	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ0 ↑m 1o) ↦ if(𝑏 = 𝑎, (1r‘𝑅), (0g‘𝑅)))))) = ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
97		nn0ex 12605	. . . . . 6 ⊢ ℕ0 ∈ V
98	97	mptex 7227	. . . . 5 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V
99	98	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V)
100	7	fvexi 6897	. . . . 5 ⊢ 𝑃 ∈ V
101	100	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑃 ∈ V)
102		ovexd 7453	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1o mPoly 𝑅) ∈ V)
103	8, 9	eqtr3i 2786	. . . . 5 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
104	103	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (Base‘𝑃) = (Base‘(1o mPoly 𝑅)))
105		eqid 2761	. . . . . 6 ⊢ (+g‘𝑃) = (+g‘𝑃)
106	7, 1, 105	ply1plusg 22534	. . . . 5 ⊢ (+g‘𝑃) = (+g‘(1o mPoly 𝑅))
107	106	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (+g‘𝑃) = (+g‘(1o mPoly 𝑅)))
108	99, 101, 102, 104, 107	gsumpropd 18860	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1o mPoly 𝑅) Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
109		eqid 2761	. . . . 5 ⊢ (0g‘𝑃) = (0g‘𝑃)
110	1, 7, 109	ply1mpl0 22567	. . . 4 ⊢ (0g‘𝑃) = (0g‘(1o mPoly 𝑅))
111	1	mpllmod 22318	. . . . . 6 ⊢ ((1o ∈ ω ∧ 𝑅 ∈ Ring) → (1o mPoly 𝑅) ∈ LMod)
112	5, 12, 111	sylancr 599	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1o mPoly 𝑅) ∈ LMod)
113		lmodcmn 21178	. . . . 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 22562	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
117	116	ad2antrr 739	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod)
118		eqid 2761	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
119	15, 8, 7, 118	coe1f 22522	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝐵 → 𝐴:ℕ0⟶(Base‘𝑅))
120	119	adantl 487	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴:ℕ0⟶(Base‘𝑅))
121	120	ffvelcdmda 7082	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑅))
122	7	ply1sca 22563	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
123	122	eqcomd 2767	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅)
124	123	ad2antrr 739	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (Scalar‘𝑃) = 𝑅)
125	124	fveq2d 6887	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
126	121, 125	eleqtrrd 2864	. . . . . 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 19298	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐵)
131		eqid 2761	. . . . . . 7 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
132		eqid 2761	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
133	8, 131, 10, 132	lmodvscl 21146	. . . . . 6 ⊢ ((𝑃 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
134	117, 126, 130, 133	syl3anc 1398	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
135	134	fmpttd 7113	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))):ℕ0⟶𝐵)
136	7, 80, 8, 10, 55, 52, 15	ply1coefsupp 22608	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0g‘𝑃))
137		eqid 2761	. . . . . 6 ⊢ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅))
138	39, 97, 25, 137	mapsnf1o2 8915	. . . . 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 20123	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1o mPoly 𝑅) Σg ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)))))
141		eqidd 2762	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)))
142		eqidd 2762	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))
143		fveq2 6883	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝐴‘𝑘) = (𝐴‘(𝑎‘∅)))
144		oveq1 7425	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝑘 ↑ 𝑋) = ((𝑎‘∅) ↑ 𝑋))
145	143, 144	oveq12d 7436	. . . . 5 ⊢ (𝑘 = (𝑎‘∅) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
146	79, 141, 142, 145	fmptco 7128	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅))) = (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
147	146	oveq2d 7434	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ0 ↑m 1o) ↦ (𝑎‘∅)))) = ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
148	108, 140, 147	3eqtrrd 2801	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1o mPoly 𝑅) Σg (𝑎 ∈ (ℕ0 ↑m 1o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
149	14, 96, 148	3eqtrd 2800	1 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  Vcvv 3451   ⊆ wss 3899  ∅c0 4279  ifcif 4482  {csn 4584   ↦ cmpt 5186   ∘ ccom 5655  ⟶wf 6533  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7418  ωcom 7875  1_oc1o 8462   ↑_m cmap 8840  ℕ₀cn0 12599  Basecbs 17380  +_gcplusg 17421  ._rcmulr 17422  Scalarcsca 17424   ·_𝑠 cvsca 17425  0_gc0g 17603   Σ_g cgsu 17604  Mndcmnd 18916  ._gcmg 19270  CMndccmn 19987  mulGrpcmgp 20353  1_rcur 20400  Ringcrg 20452  LModclmod 21128   mVar cmvr 22206   mPoly cmpl 22207  var₁cv1 22487  Poly₁cpl1 22488  coe₁cco1 22489

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-ofr 7692  df-om 7876  df-1st 7999  df-2nd 8000  df-supp 8171  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-er 8710  df-map 8842  df-pm 8843  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9347  df-sup 9427  df-oi 9497  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404  df-9 12405  df-n0 12600  df-z 12687  df-dec 12808  df-uz 12959  df-fz 13633  df-fzo 13782  df-seq 14138  df-hash 14468  df-struct 17318  df-sets 17335  df-slot 17353  df-ndx 17365  df-base 17381  df-ress 17402  df-plusg 17434  df-mulr 17435  df-sca 17437  df-vsca 17438  df-ip 17439  df-tset 17440  df-ple 17441  df-ds 17443  df-hom 17445  df-cco 17446  df-0g 17605  df-gsum 17606  df-prds 17611  df-pws 17613  df-mre 17749  df-mrc 17750  df-acs 17752  df-mgm 18809  df-sgrp 18901  df-mnd 18917  df-mhm 18971  df-submnd 18972  df-grp 19140  df-minusg 19141  df-sbg 19142  df-mulg 19271  df-subg 19326  df-ghm 19421  df-cntz 19524  df-cmn 19989  df-abl 19990  df-mgp 20354  df-rng 20368  df-ur 20401  df-srg 20406  df-ring 20454  df-subrng 20791  df-subrg 20815  df-lmod 21130  df-lss 21200  df-psr 22210  df-mvr 22211  df-mpl 22212  df-opsr 22214  df-psr1 22491  df-vr1 22492  df-ply1 22493  df-coe1 22494

This theorem is used by:  eqcoe1ply1eq  22610  evls1fpws  22680  pmatcollpw1lem2  23086  mp2pm2mp  23122  plypf1  26524  ply1coedeg  34114  ply1degltdimlem  34247