ply1coe - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ply1coe		Structured version Visualization version GIF version

Theorem ply1coe 22167

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	⊢ 𝑃 = (Poly₁‘𝑅)
ply1coe.x	⊢ 𝑋 = (var₁‘𝑅)
ply1coe.b	⊢ 𝐵 = (Base‘𝑃)
ply1coe.n	⊢ · = ( ·_𝑠 ‘𝑃)
ply1coe.m	⊢ 𝑀 = (mulGrp‘𝑃)
ply1coe.e	⊢ ↑ = (._g‘𝑀)
ply1coe.a	⊢ 𝐴 = (coe₁‘𝐾)

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

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 2726	. . 3 ⊢ (1_o mPoly 𝑅) = (1_o mPoly 𝑅)
2		psr1baslem 22054	. . 3 ⊢ (ℕ₀ ↑_m 1_o) = {𝑑 ∈ (ℕ₀ ↑_m 1_o) ∣ (^◡𝑑 “ ℕ) ∈ Fin}
3		eqid 2726	. . 3 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
4		eqid 2726	. . 3 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
5		1onn 8638	. . . 4 ⊢ 1_o ∈ ω
6	5	a1i 11	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 1_o ∈ ω)
7		ply1coe.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
8		eqid 2726	. . . 4 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
9		ply1coe.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
10	7, 8, 9	ply1bas 22064	. . 3 ⊢ 𝐵 = (Base‘(1_o mPoly 𝑅))
11		ply1coe.n	. . . 4 ⊢ · = ( ·_𝑠 ‘𝑃)
12	7, 1, 11	ply1vsca 22093	. . 3 ⊢ · = ( ·_𝑠 ‘(1_o mPoly 𝑅))
13		simpl 482	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑅 ∈ Ring)
14		simpr 484	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 ∈ 𝐵)
15	1, 2, 3, 4, 6, 10, 12, 13, 14	mplcoe1 21929	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅)))))))
16		ply1coe.a	. . . . . . 7 ⊢ 𝐴 = (coe₁‘𝐾)
17	16	fvcoe1 22076	. . . . . 6 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅)))
18	17	adantll 711	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅)))
19	5	a1i 11	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 1_o ∈ ω)
20		eqid 2726	. . . . . . 7 ⊢ (mulGrp‘(1_o mPoly 𝑅)) = (mulGrp‘(1_o mPoly 𝑅))
21		eqid 2726	. . . . . . 7 ⊢ (._g‘(mulGrp‘(1_o mPoly 𝑅))) = (._g‘(mulGrp‘(1_o mPoly 𝑅)))
22		eqid 2726	. . . . . . 7 ⊢ (1_o mVar 𝑅) = (1_o mVar 𝑅)
23		simpll 764	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑅 ∈ Ring)
24		simpr 484	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑎 ∈ (ℕ₀ ↑_m 1_o))
25		eqidd 2727	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
26		0ex 5300	. . . . . . . . . . 11 ⊢ ∅ ∈ V
27		fveq2 6884	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → ((1_o mVar 𝑅)‘𝑏) = ((1_o mVar 𝑅)‘∅))
28	27	oveq1d 7419	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
29	27	oveq2d 7420	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
30	28, 29	eqeq12d 2742	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → ((((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅))))
31	26, 30	ralsn 4680	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
32	25, 31	sylibr 233	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
33		fveq2 6884	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((1_o mVar 𝑅)‘𝑥) = ((1_o mVar 𝑅)‘∅))
34	33	oveq2d 7420	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
35	33	oveq1d 7419	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
36	34, 35	eqeq12d 2742	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏))))
37	36	ralbidv 3171	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏))))
38	26, 37	ralsn 4680	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
39	32, 38	sylibr 233	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
40		df1o2 8471	. . . . . . . . 9 ⊢ 1_o = {∅}
41	40	raleqi 3317	. . . . . . . . 9 ⊢ (∀𝑏 ∈ 1_o (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
42	40, 41	raleqbii 3332	. . . . . . . 8 ⊢ (∀𝑥 ∈ 1_o ∀𝑏 ∈ 1_o (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
43	39, 42	sylibr 233	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∀𝑥 ∈ 1_o ∀𝑏 ∈ 1_o (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
44	1, 2, 3, 4, 19, 20, 21, 22, 23, 24, 43	mplcoe5 21932	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅))) = ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))))
45	40	mpteq1i 5237	. . . . . . . 8 ⊢ (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐))) = (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))
46	45	oveq2i 7415	. . . . . . 7 ⊢ ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐))))
47	1	mplring 21915	. . . . . . . . . . 11 ⊢ ((1_o ∈ ω ∧ 𝑅 ∈ Ring) → (1_o mPoly 𝑅) ∈ Ring)
48	5, 47	mpan 687	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (1_o mPoly 𝑅) ∈ Ring)
49	20	ringmgp 20141	. . . . . . . . . 10 ⊢ ((1_o mPoly 𝑅) ∈ Ring → (mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd)
50	48, 49	syl 17	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd)
51	50	ad2antrr 723	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd)
52	26	a1i 11	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∅ ∈ V)
53		ply1coe.e	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘𝑀)
54	20, 10	mgpbas 20042	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘(mulGrp‘(1_o mPoly 𝑅)))
55	54	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘(mulGrp‘(1_o mPoly 𝑅))))
56		ply1coe.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (mulGrp‘𝑃)
57	56, 9	mgpbas 20042	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑀)
58	57	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘𝑀))
59		ssv 4001	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ V
60	59	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 ⊆ V)
61		ovexd 7439	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+_g‘(mulGrp‘(1_o mPoly 𝑅)))𝑏) ∈ V)
62		eqid 2726	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝑃) = (._r‘𝑃)
63	7, 1, 62	ply1mulr 22094	. . . . . . . . . . . . . . . 16 ⊢ (._r‘𝑃) = (._r‘(1_o mPoly 𝑅))
64	20, 63	mgpplusg 20040	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝑃) = (+_g‘(mulGrp‘(1_o mPoly 𝑅)))
65	56, 62	mgpplusg 20040	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝑃) = (+_g‘𝑀)
66	64, 65	eqtr3i 2756	. . . . . . . . . . . . . 14 ⊢ (+_g‘(mulGrp‘(1_o mPoly 𝑅))) = (+_g‘𝑀)
67	66	oveqi 7417	. . . . . . . . . . . . 13 ⊢ (𝑎(+_g‘(mulGrp‘(1_o mPoly 𝑅)))𝑏) = (𝑎(+_g‘𝑀)𝑏)
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+_g‘(mulGrp‘(1_o mPoly 𝑅)))𝑏) = (𝑎(+_g‘𝑀)𝑏))
69	21, 53, 55, 58, 60, 61, 68	mulgpropd 19040	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (._g‘(mulGrp‘(1_o mPoly 𝑅))) = ↑ )
70	69	oveqd 7421	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
71	70	adantr 480	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
72	7	ply1ring 22116	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
73	56	ringmgp 20141	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd)
74	72, 73	syl 17	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
75	74	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑀 ∈ Mnd)
76		elmapi 8842	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) → 𝑎:1_o⟶ℕ₀)
77		0lt1o 8502	. . . . . . . . . . . 12 ⊢ ∅ ∈ 1_o
78		ffvelcdm 7076	. . . . . . . . . . . 12 ⊢ ((𝑎:1_o⟶ℕ₀ ∧ ∅ ∈ 1_o) → (𝑎‘∅) ∈ ℕ₀)
79	76, 77, 78	sylancl 585	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) → (𝑎‘∅) ∈ ℕ₀)
80	79	adantl 481	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝑎‘∅) ∈ ℕ₀)
81		ply1coe.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (var₁‘𝑅)
82	81, 7, 9	vr1cl 22086	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
83	82	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑋 ∈ 𝐵)
84	57, 53, 75, 80, 83	mulgnn0cld 19019	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵)
85	71, 84	eqeltrd 2827	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) ∈ 𝐵)
86		fveq2 6884	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (𝑎‘𝑐) = (𝑎‘∅))
87		fveq2 6884	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((1_o mVar 𝑅)‘𝑐) = ((1_o mVar 𝑅)‘∅))
88	81	vr1val 22061	. . . . . . . . . . 11 ⊢ 𝑋 = ((1_o mVar 𝑅)‘∅)
89	87, 88	eqtr4di 2784	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → ((1_o mVar 𝑅)‘𝑐) = 𝑋)
90	86, 89	oveq12d 7422	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
91	54, 90	gsumsn 19871	. . . . . . . 8 ⊢ (((mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd ∧ ∅ ∈ V ∧ ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) ∈ 𝐵) → ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
92	51, 52, 85, 91	syl3anc 1368	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
93	46, 92	eqtrid 2778	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
94	44, 93, 71	3eqtrd 2770	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅))) = ((𝑎‘∅) ↑ 𝑋))
95	18, 94	oveq12d 7422	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅)))) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
96	95	mpteq2dva 5241	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅))))) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
97	96	oveq2d 7420	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅)))))) = ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
98		nn0ex 12479	. . . . . 6 ⊢ ℕ₀ ∈ V
99	98	mptex 7219	. . . . 5 ⊢ (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V
100	99	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V)
101	7	fvexi 6898	. . . . 5 ⊢ 𝑃 ∈ V
102	101	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑃 ∈ V)
103		ovexd 7439	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1_o mPoly 𝑅) ∈ V)
104	9, 10	eqtr3i 2756	. . . . 5 ⊢ (Base‘𝑃) = (Base‘(1_o mPoly 𝑅))
105	104	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (Base‘𝑃) = (Base‘(1_o mPoly 𝑅)))
106		eqid 2726	. . . . . 6 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
107	7, 1, 106	ply1plusg 22092	. . . . 5 ⊢ (+_g‘𝑃) = (+_g‘(1_o mPoly 𝑅))
108	107	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (+_g‘𝑃) = (+_g‘(1_o mPoly 𝑅)))
109	100, 102, 103, 105, 108	gsumpropd 18608	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1_o mPoly 𝑅) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
110		eqid 2726	. . . . 5 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
111	1, 7, 110	ply1mpl0 22124	. . . 4 ⊢ (0_g‘𝑃) = (0_g‘(1_o mPoly 𝑅))
112	1	mpllmod 21914	. . . . . 6 ⊢ ((1_o ∈ ω ∧ 𝑅 ∈ Ring) → (1_o mPoly 𝑅) ∈ LMod)
113	5, 13, 112	sylancr 586	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1_o mPoly 𝑅) ∈ LMod)
114		lmodcmn 20753	. . . . 5 ⊢ ((1_o mPoly 𝑅) ∈ LMod → (1_o mPoly 𝑅) ∈ CMnd)
115	113, 114	syl 17	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1_o mPoly 𝑅) ∈ CMnd)
116	98	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ℕ₀ ∈ V)
117	7	ply1lmod 22120	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
118	117	ad2antrr 723	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑃 ∈ LMod)
119		eqid 2726	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
120	16, 9, 7, 119	coe1f 22080	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝐵 → 𝐴:ℕ₀⟶(Base‘𝑅))
121	120	adantl 481	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴:ℕ₀⟶(Base‘𝑅))
122	121	ffvelcdmda 7079	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ (Base‘𝑅))
123	7	ply1sca 22121	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
124	123	eqcomd 2732	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅)
125	124	ad2antrr 723	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (Scalar‘𝑃) = 𝑅)
126	125	fveq2d 6888	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
127	122, 126	eleqtrrd 2830	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
128	74	ad2antrr 723	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑀 ∈ Mnd)
129		simpr 484	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
130	82	ad2antrr 723	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑋 ∈ 𝐵)
131	57, 53, 128, 129, 130	mulgnn0cld 19019	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝑘 ↑ 𝑋) ∈ 𝐵)
132		eqid 2726	. . . . . . 7 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
133		eqid 2726	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
134	9, 132, 11, 133	lmodvscl 20721	. . . . . 6 ⊢ ((𝑃 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
135	118, 127, 131, 134	syl3anc 1368	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
136	135	fmpttd 7109	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))):ℕ₀⟶𝐵)
137	7, 81, 9, 11, 56, 53, 16	ply1coefsupp 22166	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0_g‘𝑃))
138		eqid 2726	. . . . . 6 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅))
139	40, 98, 26, 138	mapsnf1o2 8887	. . . . 5 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)):(ℕ₀ ↑_m 1_o)–1-1-onto→ℕ₀
140	139	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)):(ℕ₀ ↑_m 1_o)–1-1-onto→ℕ₀)
141	10, 111, 115, 116, 136, 137, 140	gsumf1o 19833	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1_o mPoly 𝑅) Σ_g ((𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)))))
142		eqidd 2727	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)))
143		eqidd 2727	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))
144		fveq2 6884	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝐴‘𝑘) = (𝐴‘(𝑎‘∅)))
145		oveq1 7411	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝑘 ↑ 𝑋) = ((𝑎‘∅) ↑ 𝑋))
146	144, 145	oveq12d 7422	. . . . 5 ⊢ (𝑘 = (𝑎‘∅) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
147	80, 142, 143, 146	fmptco 7122	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅))) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
148	147	oveq2d 7420	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g ((𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)))) = ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
149	109, 141, 148	3eqtrrd 2771	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) = (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
150	15, 97, 149	3eqtrd 2770	1 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ∀wral 3055 Vcvv 3468 ⊆ wss 3943 ∅c0 4317 ifcif 4523 {csn 4623 ↦ cmpt 5224 ∘ ccom 5673 ⟶wf 6532 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7404 ωcom 7851 1_oc1o 8457 ↑_m cmap 8819 ℕ₀cn0 12473 Basecbs 17150 +_gcplusg 17203 ._rcmulr 17204 Scalarcsca 17206 ·_𝑠 cvsca 17207 0_gc0g 17391 Σ_g cgsu 17392 Mndcmnd 18664 ._gcmg 18992 CMndccmn 19697 mulGrpcmgp 20036 1_rcur 20083 Ringcrg 20135 LModclmod 20703 mVar cmvr 21794 mPoly cmpl 21795 PwSer₁cps1 22044 var₁cv1 22045 Poly₁cpl1 22046 coe₁cco1 22047

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7721 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-iin 4993 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6293 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6488 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-of 7666 df-ofr 7667 df-om 7852 df-1st 7971 df-2nd 7972 df-supp 8144 df-frecs 8264 df-wrecs 8295 df-recs 8369 df-rdg 8408 df-1o 8464 df-er 8702 df-map 8821 df-pm 8822 df-ixp 8891 df-en 8939 df-dom 8940 df-sdom 8941 df-fin 8942 df-fsupp 9361 df-sup 9436 df-oi 9504 df-card 9933 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11447 df-neg 11448 df-nn 12214 df-2 12276 df-3 12277 df-4 12278 df-5 12279 df-6 12280 df-7 12281 df-8 12282 df-9 12283 df-n0 12474 df-z 12560 df-dec 12679 df-uz 12824 df-fz 13488 df-fzo 13631 df-seq 13970 df-hash 14293 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17151 df-ress 17180 df-plusg 17216 df-mulr 17217 df-sca 17219 df-vsca 17220 df-ip 17221 df-tset 17222 df-ple 17223 df-ds 17225 df-hom 17227 df-cco 17228 df-0g 17393 df-gsum 17394 df-prds 17399 df-pws 17401 df-mre 17536 df-mrc 17537 df-acs 17539 df-mgm 18570 df-sgrp 18649 df-mnd 18665 df-mhm 18710 df-submnd 18711 df-grp 18863 df-minusg 18864 df-sbg 18865 df-mulg 18993 df-subg 19047 df-ghm 19136 df-cntz 19230 df-cmn 19699 df-abl 19700 df-mgp 20037 df-rng 20055 df-ur 20084 df-srg 20089 df-ring 20137 df-subrng 20443 df-subrg 20468 df-lmod 20705 df-lss 20776 df-psr 21798 df-mvr 21799 df-mpl 21800 df-opsr 21802 df-psr1 22049 df-vr1 22050 df-ply1 22051 df-coe1 22052

This theorem is referenced by: eqcoe1ply1eq 22168 pmatcollpw1lem2 22627 mp2pm2mp 22663 plypf1 26096 evls1fpws 33154 ply1degltdimlem 33224

W3C validator