coe1tm - Metamath Proof Explorer

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

Theorem coe1tm 20147

Description: Coefficient vector of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)

**Hypotheses**
Ref	Expression
coe1tm.z	⊢ 0 = (0_g‘𝑅)
coe1tm.k	⊢ 𝐾 = (Base‘𝑅)
coe1tm.p	⊢ 𝑃 = (Poly₁‘𝑅)
coe1tm.x	⊢ 𝑋 = (var₁‘𝑅)
coe1tm.m	⊢ · = ( ·_𝑠 ‘𝑃)
coe1tm.n	⊢ 𝑁 = (mulGrp‘𝑃)
coe1tm.e	⊢ ↑ = (._g‘𝑁)

**Assertion**
Ref	Expression
coe1tm	⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (coe₁‘(𝐶 · (𝐷 ↑ 𝑋))) = (𝑥 ∈ ℕ₀ ↦ if(𝑥 = 𝐷, 𝐶, 0 )))

Distinct variable groups: 𝑥, 0 𝑥,𝐶 𝑥,𝐷 𝑥,𝐾 𝑥, ↑ 𝑥,𝑁 𝑥,𝑃 𝑥,𝑋 𝑥,𝑅 𝑥, ·

Proof of Theorem coe1tm Dummy variables 𝑎 𝑏 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		coe1tm.k	. . . 4 ⊢ 𝐾 = (Base‘𝑅)
2		coe1tm.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
3		coe1tm.x	. . . 4 ⊢ 𝑋 = (var₁‘𝑅)
4		coe1tm.m	. . . 4 ⊢ · = ( ·_𝑠 ‘𝑃)
5		coe1tm.n	. . . 4 ⊢ 𝑁 = (mulGrp‘𝑃)
6		coe1tm.e	. . . 4 ⊢ ↑ = (._g‘𝑁)
7		eqid 2778	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
8	1, 2, 3, 4, 5, 6, 7	ply1tmcl 20146	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ (Base‘𝑃))
9		eqid 2778	. . . 4 ⊢ (coe₁‘(𝐶 · (𝐷 ↑ 𝑋))) = (coe₁‘(𝐶 · (𝐷 ↑ 𝑋)))
10		eqid 2778	. . . 4 ⊢ (𝑥 ∈ ℕ₀ ↦ (1_o × {𝑥})) = (𝑥 ∈ ℕ₀ ↦ (1_o × {𝑥}))
11	9, 7, 2, 10	coe1fval2 20084	. . 3 ⊢ ((𝐶 · (𝐷 ↑ 𝑋)) ∈ (Base‘𝑃) → (coe₁‘(𝐶 · (𝐷 ↑ 𝑋))) = ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ₀ ↦ (1_o × {𝑥}))))
12	8, 11	syl 17	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (coe₁‘(𝐶 · (𝐷 ↑ 𝑋))) = ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ₀ ↦ (1_o × {𝑥}))))
13		fconst6g 6399	. . . . 5 ⊢ (𝑥 ∈ ℕ₀ → (1_o × {𝑥}):1_o⟶ℕ₀)
14		nn0ex 11717	. . . . . 6 ⊢ ℕ₀ ∈ V
15		1oex 7915	. . . . . 6 ⊢ 1_o ∈ V
16	14, 15	elmap 8237	. . . . 5 ⊢ ((1_o × {𝑥}) ∈ (ℕ₀ ↑_𝑚 1_o) ↔ (1_o × {𝑥}):1_o⟶ℕ₀)
17	13, 16	sylibr 226	. . . 4 ⊢ (𝑥 ∈ ℕ₀ → (1_o × {𝑥}) ∈ (ℕ₀ ↑_𝑚 1_o))
18	17	adantl 474	. . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → (1_o × {𝑥}) ∈ (ℕ₀ ↑_𝑚 1_o))
19		eqidd 2779	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝑥 ∈ ℕ₀ ↦ (1_o × {𝑥})) = (𝑥 ∈ ℕ₀ ↦ (1_o × {𝑥})))
20		eqid 2778	. . . . . . . 8 ⊢ (._g‘(mulGrp‘(1_o mPoly 𝑅))) = (._g‘(mulGrp‘(1_o mPoly 𝑅)))
21	5, 7	mgpbas 18971	. . . . . . . . 9 ⊢ (Base‘𝑃) = (Base‘𝑁)
22	21	a1i 11	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) = (Base‘𝑁))
23		eqid 2778	. . . . . . . . . 10 ⊢ (mulGrp‘(1_o mPoly 𝑅)) = (mulGrp‘(1_o mPoly 𝑅))
24		eqid 2778	. . . . . . . . . . 11 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
25	2, 24, 7	ply1bas 20069	. . . . . . . . . 10 ⊢ (Base‘𝑃) = (Base‘(1_o mPoly 𝑅))
26	23, 25	mgpbas 18971	. . . . . . . . 9 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘(1_o mPoly 𝑅)))
27	26	a1i 11	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) = (Base‘(mulGrp‘(1_o mPoly 𝑅))))
28		ssv 3883	. . . . . . . . 9 ⊢ (Base‘𝑃) ⊆ V
29	28	a1i 11	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ⊆ V)
30		ovexd 7012	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+_g‘𝑁)𝑦) ∈ V)
31		eqid 2778	. . . . . . . . . . . 12 ⊢ (._r‘𝑃) = (._r‘𝑃)
32	5, 31	mgpplusg 18969	. . . . . . . . . . 11 ⊢ (._r‘𝑃) = (+_g‘𝑁)
33		eqid 2778	. . . . . . . . . . . . 13 ⊢ (1_o mPoly 𝑅) = (1_o mPoly 𝑅)
34	2, 33, 31	ply1mulr 20101	. . . . . . . . . . . 12 ⊢ (._r‘𝑃) = (._r‘(1_o mPoly 𝑅))
35	23, 34	mgpplusg 18969	. . . . . . . . . . 11 ⊢ (._r‘𝑃) = (+_g‘(mulGrp‘(1_o mPoly 𝑅)))
36	32, 35	eqtr3i 2804	. . . . . . . . . 10 ⊢ (+_g‘𝑁) = (+_g‘(mulGrp‘(1_o mPoly 𝑅)))
37	36	a1i 11	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (+_g‘𝑁) = (+_g‘(mulGrp‘(1_o mPoly 𝑅))))
38	37	oveqdr 7006	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+_g‘𝑁)𝑦) = (𝑥(+_g‘(mulGrp‘(1_o mPoly 𝑅)))𝑦))
39	6, 20, 22, 27, 29, 30, 38	mulgpropd 18056	. . . . . . 7 ⊢ (𝑅 ∈ Ring → ↑ = (._g‘(mulGrp‘(1_o mPoly 𝑅))))
40	39	3ad2ant1 1113	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → ↑ = (._g‘(mulGrp‘(1_o mPoly 𝑅))))
41		eqidd 2779	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → 𝐷 = 𝐷)
42	3	vr1val 20066	. . . . . . 7 ⊢ 𝑋 = ((1_o mVar 𝑅)‘∅)
43	42	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → 𝑋 = ((1_o mVar 𝑅)‘∅))
44	40, 41, 43	oveq123d 6999	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝐷 ↑ 𝑋) = (𝐷(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
45	44	oveq2d 6994	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝐶 · (𝐷 ↑ 𝑋)) = (𝐶 · (𝐷(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅))))
46		psr1baslem 20059	. . . . . 6 ⊢ (ℕ₀ ↑_𝑚 1_o) = {𝑎 ∈ (ℕ₀ ↑_𝑚 1_o) ∣ (^◡𝑎 “ ℕ) ∈ Fin}
47		coe1tm.z	. . . . . 6 ⊢ 0 = (0_g‘𝑅)
48		eqid 2778	. . . . . 6 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
49		1on 7914	. . . . . . 7 ⊢ 1_o ∈ On
50	49	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → 1_o ∈ On)
51		eqid 2778	. . . . . 6 ⊢ (1_o mVar 𝑅) = (1_o mVar 𝑅)
52		simp1 1116	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → 𝑅 ∈ Ring)
53		0lt1o 7933	. . . . . . 7 ⊢ ∅ ∈ 1_o
54	53	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → ∅ ∈ 1_o)
55		simp3 1118	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → 𝐷 ∈ ℕ₀)
56	33, 46, 47, 48, 50, 23, 20, 51, 52, 54, 55	mplcoe3 19963	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝑦 ∈ (ℕ₀ ↑_𝑚 1_o) ↦ if(𝑦 = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), (1_r‘𝑅), 0 )) = (𝐷(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
57	56	oveq2d 6994	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝐶 · (𝑦 ∈ (ℕ₀ ↑_𝑚 1_o) ↦ if(𝑦 = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), (1_r‘𝑅), 0 ))) = (𝐶 · (𝐷(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅))))
58	2, 33, 4	ply1vsca 20100	. . . . 5 ⊢ · = ( ·_𝑠 ‘(1_o mPoly 𝑅))
59		elsni 4459	. . . . . . . . . . 11 ⊢ (𝑏 ∈ {∅} → 𝑏 = ∅)
60		df1o2 7920	. . . . . . . . . . 11 ⊢ 1_o = {∅}
61	59, 60	eleq2s 2884	. . . . . . . . . 10 ⊢ (𝑏 ∈ 1_o → 𝑏 = ∅)
62	61	iftrued 4359	. . . . . . . . 9 ⊢ (𝑏 ∈ 1_o → if(𝑏 = ∅, 𝐷, 0) = 𝐷)
63	62	adantl 474	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑏 ∈ 1_o) → if(𝑏 = ∅, 𝐷, 0) = 𝐷)
64	63	mpteq2dva 5023	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)) = (𝑏 ∈ 1_o ↦ 𝐷))
65		fconstmpt 5465	. . . . . . 7 ⊢ (1_o × {𝐷}) = (𝑏 ∈ 1_o ↦ 𝐷)
66	64, 65	syl6eqr 2832	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)) = (1_o × {𝐷}))
67		fconst6g 6399	. . . . . . . 8 ⊢ (𝐷 ∈ ℕ₀ → (1_o × {𝐷}):1_o⟶ℕ₀)
68	14, 15	elmap 8237	. . . . . . . 8 ⊢ ((1_o × {𝐷}) ∈ (ℕ₀ ↑_𝑚 1_o) ↔ (1_o × {𝐷}):1_o⟶ℕ₀)
69	67, 68	sylibr 226	. . . . . . 7 ⊢ (𝐷 ∈ ℕ₀ → (1_o × {𝐷}) ∈ (ℕ₀ ↑_𝑚 1_o))
70	69	3ad2ant3 1115	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (1_o × {𝐷}) ∈ (ℕ₀ ↑_𝑚 1_o))
71	66, 70	eqeltrd 2866	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)) ∈ (ℕ₀ ↑_𝑚 1_o))
72		simp2 1117	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → 𝐶 ∈ 𝐾)
73	33, 58, 46, 48, 47, 1, 50, 52, 71, 72	mplmon2 19989	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝐶 · (𝑦 ∈ (ℕ₀ ↑_𝑚 1_o) ↦ if(𝑦 = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), (1_r‘𝑅), 0 ))) = (𝑦 ∈ (ℕ₀ ↑_𝑚 1_o) ↦ if(𝑦 = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )))
74	45, 57, 73	3eqtr2d 2820	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝐶 · (𝐷 ↑ 𝑋)) = (𝑦 ∈ (ℕ₀ ↑_𝑚 1_o) ↦ if(𝑦 = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )))
75		eqeq1 2782	. . . 4 ⊢ (𝑦 = (1_o × {𝑥}) → (𝑦 = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)) ↔ (1_o × {𝑥}) = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0))))
76	75	ifbid 4373	. . 3 ⊢ (𝑦 = (1_o × {𝑥}) → if(𝑦 = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ) = if((1_o × {𝑥}) = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ))
77	18, 19, 74, 76	fmptco 6716	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ₀ ↦ (1_o × {𝑥}))) = (𝑥 ∈ ℕ₀ ↦ if((1_o × {𝑥}) = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )))
78	66	adantr 473	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)) = (1_o × {𝐷}))
79	78	eqeq2d 2788	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → ((1_o × {𝑥}) = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)) ↔ (1_o × {𝑥}) = (1_o × {𝐷})))
80		fveq1 6500	. . . . . . 7 ⊢ ((1_o × {𝑥}) = (1_o × {𝐷}) → ((1_o × {𝑥})‘∅) = ((1_o × {𝐷})‘∅))
81		vex 3418	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
82	81	fvconst2 6795	. . . . . . . . 9 ⊢ (∅ ∈ 1_o → ((1_o × {𝑥})‘∅) = 𝑥)
83	53, 82	mp1i 13	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → ((1_o × {𝑥})‘∅) = 𝑥)
84		simpl3 1173	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → 𝐷 ∈ ℕ₀)
85		fvconst2g 6793	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℕ₀ ∧ ∅ ∈ 1_o) → ((1_o × {𝐷})‘∅) = 𝐷)
86	84, 53, 85	sylancl 577	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → ((1_o × {𝐷})‘∅) = 𝐷)
87	83, 86	eqeq12d 2793	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → (((1_o × {𝑥})‘∅) = ((1_o × {𝐷})‘∅) ↔ 𝑥 = 𝐷))
88	80, 87	syl5ib 236	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → ((1_o × {𝑥}) = (1_o × {𝐷}) → 𝑥 = 𝐷))
89		sneq 4452	. . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝑥} = {𝐷})
90	89	xpeq2d 5438	. . . . . 6 ⊢ (𝑥 = 𝐷 → (1_o × {𝑥}) = (1_o × {𝐷}))
91	88, 90	impbid1 217	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → ((1_o × {𝑥}) = (1_o × {𝐷}) ↔ 𝑥 = 𝐷))
92	79, 91	bitrd 271	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → ((1_o × {𝑥}) = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)) ↔ 𝑥 = 𝐷))
93	92	ifbid 4373	. . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) ∧ 𝑥 ∈ ℕ₀) → if((1_o × {𝑥}) = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ) = if(𝑥 = 𝐷, 𝐶, 0 ))
94	93	mpteq2dva 5023	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (𝑥 ∈ ℕ₀ ↦ if((1_o × {𝑥}) = (𝑏 ∈ 1_o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )) = (𝑥 ∈ ℕ₀ ↦ if(𝑥 = 𝐷, 𝐶, 0 )))
95	12, 77, 94	3eqtrd 2818	1 ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀) → (coe₁‘(𝐶 · (𝐷 ↑ 𝑋))) = (𝑥 ∈ ℕ₀ ↦ if(𝑥 = 𝐷, 𝐶, 0 )))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 Vcvv 3415 ⊆ wss 3831 ∅c0 4180 ifcif 4351 {csn 4442 ↦ cmpt 5009 × cxp 5406 ∘ ccom 5412 Oncon0 6031 ⟶wf 6186 ‘cfv 6190 (class class class)co 6978 1_oc1o 7900 ↑_𝑚 cmap 8208 0cc0 10337 ℕ₀cn0 11710 Basecbs 16342 +_gcplusg 16424 ._rcmulr 16425 ·_𝑠 cvsca 16428 0_gc0g 16572 ._gcmg 18014 mulGrpcmgp 18965 1_rcur 18977 Ringcrg 19023 mVar cmvr 19849 mPoly cmpl 19850 PwSer₁cps1 20049 var₁cv1 20050 Poly₁cpl1 20051 coe₁cco1 20052

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413 ax-pre-mulgt0 10414

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-uni 4714 df-int 4751 df-iun 4795 df-iin 4796 df-br 4931 df-opab 4993 df-mpt 5010 df-tr 5032 df-id 5313 df-eprel 5318 df-po 5327 df-so 5328 df-fr 5367 df-se 5368 df-we 5369 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-pred 5988 df-ord 6034 df-on 6035 df-lim 6036 df-suc 6037 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-isom 6199 df-riota 6939 df-ov 6981 df-oprab 6982 df-mpo 6983 df-of 7229 df-ofr 7230 df-om 7399 df-1st 7503 df-2nd 7504 df-supp 7636 df-wrecs 7752 df-recs 7814 df-rdg 7852 df-1o 7907 df-2o 7908 df-oadd 7911 df-er 8091 df-map 8210 df-pm 8211 df-ixp 8262 df-en 8309 df-dom 8310 df-sdom 8311 df-fin 8312 df-fsupp 8631 df-oi 8771 df-card 9164 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-sub 10674 df-neg 10675 df-nn 11442 df-2 11506 df-3 11507 df-4 11508 df-5 11509 df-6 11510 df-7 11511 df-8 11512 df-9 11513 df-n0 11711 df-z 11797 df-dec 11915 df-uz 12062 df-fz 12712 df-fzo 12853 df-seq 13188 df-hash 13509 df-struct 16344 df-ndx 16345 df-slot 16346 df-base 16348 df-sets 16349 df-ress 16350 df-plusg 16437 df-mulr 16438 df-sca 16440 df-vsca 16441 df-tset 16443 df-ple 16444 df-0g 16574 df-gsum 16575 df-mre 16718 df-mrc 16719 df-acs 16721 df-mgm 17713 df-sgrp 17755 df-mnd 17766 df-mhm 17806 df-submnd 17807 df-grp 17897 df-minusg 17898 df-sbg 17899 df-mulg 18015 df-subg 18063 df-ghm 18130 df-cntz 18221 df-cmn 18671 df-abl 18672 df-mgp 18966 df-ur 18978 df-ring 19025 df-subrg 19259 df-lmod 19361 df-lss 19429 df-psr 19853 df-mvr 19854 df-mpl 19855 df-opsr 19857 df-psr1 20054 df-vr1 20055 df-ply1 20056 df-coe1 20057

This theorem is referenced by: coe1tmfv1 20148 coe1tmfv2 20149 coe1scl 20161 gsummoncoe1 20178 decpmatid 21085 monmatcollpw 21094 mp2pm2mplem4 21124

W3C validator