coe1tm

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

	Ref	Expression
Hypotheses	coe1tm.z	⊢ 0 = ( 0_g ‘ 𝑅 )
	coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1tm.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	coe1tm.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	coe1tm.m	⊢ · = ( ·_𝑠 ‘ 𝑃 )
	coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	coe1tm.e	⊢ ↑ = ( ._g ‘ 𝑁 )
Assertion	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	⊢ 0 = ( 0_g ‘ 𝑅 )
2		coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		coe1tm.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
4		coe1tm.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
5		coe1tm.m	⊢ · = ( ·_𝑠 ‘ 𝑃 )
6		coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
7		coe1tm.e	⊢ ↑ = ( ._g ‘ 𝑁 )
8		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9	2 3 4 5 6 7 8	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
10		eqid	⊢ ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) )
11		eqid	⊢ ( 𝑥 ∈ ℕ₀ ↦ ( 1_o × { 𝑥 } ) ) = ( 𝑥 ∈ ℕ₀ ↦ ( 1_o × { 𝑥 } ) )
12	10 8 3 11	coe1fval2	⊢ ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) → ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∘ ( 𝑥 ∈ ℕ₀ ↦ ( 1_o × { 𝑥 } ) ) ) )
13	9 12	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∘ ( 𝑥 ∈ ℕ₀ ↦ ( 1_o × { 𝑥 } ) ) ) )
14		fconst6g	⊢ ( 𝑥 ∈ ℕ₀ → ( 1_o × { 𝑥 } ) : 1_o ⟶ ℕ₀ )
15		nn0ex	⊢ ℕ₀ ∈ V
16		1oex	⊢ 1_o ∈ V
17	15 16	elmap	⊢ ( ( 1_o × { 𝑥 } ) ∈ ( ℕ₀ ↑_m 1_o ) ↔ ( 1_o × { 𝑥 } ) : 1_o ⟶ ℕ₀ )
18	14 17	sylibr	⊢ ( 𝑥 ∈ ℕ₀ → ( 1_o × { 𝑥 } ) ∈ ( ℕ₀ ↑_m 1_o ) )
19	18	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( 1_o × { 𝑥 } ) ∈ ( ℕ₀ ↑_m 1_o ) )
20		eqidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝑥 ∈ ℕ₀ ↦ ( 1_o × { 𝑥 } ) ) = ( 𝑥 ∈ ℕ₀ ↦ ( 1_o × { 𝑥 } ) ) )
21		eqid	⊢ ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) = ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) )
22	6 8	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 )
23	22	a1i	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 ) )
24		eqid	⊢ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) = ( mulGrp ‘ ( 1_o mPoly 𝑅 ) )
25	3 8	ply1bas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1_o mPoly 𝑅 ) )
26	24 25	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) )
27	26	a1i	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) )
28		ssv	⊢ ( Base ‘ 𝑃 ) ⊆ V
29	28	a1i	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) ⊆ V )
30		ovexd	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +_g ‘ 𝑁 ) 𝑦 ) ∈ V )
31		eqid	⊢ ( ._r ‘ 𝑃 ) = ( ._r ‘ 𝑃 )
32	6 31	mgpplusg	⊢ ( ._r ‘ 𝑃 ) = ( +_g ‘ 𝑁 )
33		eqid	⊢ ( 1_o mPoly 𝑅 ) = ( 1_o mPoly 𝑅 )
34	3 33 31	ply1mulr	⊢ ( ._r ‘ 𝑃 ) = ( ._r ‘ ( 1_o mPoly 𝑅 ) )
35	24 34	mgpplusg	⊢ ( ._r ‘ 𝑃 ) = ( +_g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) )
36	32 35	eqtr3i	⊢ ( +_g ‘ 𝑁 ) = ( +_g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) )
37	36	a1i	⊢ ( 𝑅 ∈ Ring → ( +_g ‘ 𝑁 ) = ( +_g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) )
38	37	oveqdr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +_g ‘ 𝑁 ) 𝑦 ) = ( 𝑥 ( +_g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) 𝑦 ) )
39	7 21 23 27 29 30 38	mulgpropd	⊢ ( 𝑅 ∈ Ring → ↑ = ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) )
40	39	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ↑ = ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) )
41		eqidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → 𝐷 = 𝐷 )
42	4	vr1val	⊢ 𝑋 = ( ( 1_o mVar 𝑅 ) ‘ ∅ )
43	42	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → 𝑋 = ( ( 1_o mVar 𝑅 ) ‘ ∅ ) )
44	40 41 43	oveq123d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝐷 ↑ 𝑋 ) = ( 𝐷 ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) ( ( 1_o mVar 𝑅 ) ‘ ∅ ) ) )
45	44	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) = ( 𝐶 · ( 𝐷 ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) ( ( 1_o mVar 𝑅 ) ‘ ∅ ) ) ) )
46		psr1baslem	⊢ ( ℕ₀ ↑_m 1_o ) = { 𝑎 ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin }
47		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
48		1on	⊢ 1_o ∈ On
49	48	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → 1_o ∈ On )
50		eqid	⊢ ( 1_o mVar 𝑅 ) = ( 1_o mVar 𝑅 )
51		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → 𝑅 ∈ Ring )
52		0lt1o	⊢ ∅ ∈ 1_o
53	52	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ∅ ∈ 1_o )
54		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → 𝐷 ∈ ℕ₀ )
55	33 46 1 47 49 24 21 50 51 53 54	mplcoe3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝑦 ∈ ( ℕ₀ ↑_m 1_o ) ↦ if ( 𝑦 = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , ( 1_r ‘ 𝑅 ) , 0 ) ) = ( 𝐷 ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) ( ( 1_o mVar 𝑅 ) ‘ ∅ ) ) )
56	55	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝐶 · ( 𝑦 ∈ ( ℕ₀ ↑_m 1_o ) ↦ if ( 𝑦 = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , ( 1_r ‘ 𝑅 ) , 0 ) ) ) = ( 𝐶 · ( 𝐷 ( ._g ‘ ( mulGrp ‘ ( 1_o mPoly 𝑅 ) ) ) ( ( 1_o mVar 𝑅 ) ‘ ∅ ) ) ) )
57	3 33 5	ply1vsca	⊢ · = ( ·_𝑠 ‘ ( 1_o mPoly 𝑅 ) )
58		elsni	⊢ ( 𝑏 ∈ { ∅ } → 𝑏 = ∅ )
59		df1o2	⊢ 1_o = { ∅ }
60	58 59	eleq2s	⊢ ( 𝑏 ∈ 1_o → 𝑏 = ∅ )
61	60	iftrued	⊢ ( 𝑏 ∈ 1_o → if ( 𝑏 = ∅ , 𝐷 , 0 ) = 𝐷 )
62	61	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑏 ∈ 1_o ) → if ( 𝑏 = ∅ , 𝐷 , 0 ) = 𝐷 )
63	62	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) = ( 𝑏 ∈ 1_o ↦ 𝐷 ) )
64		fconstmpt	⊢ ( 1_o × { 𝐷 } ) = ( 𝑏 ∈ 1_o ↦ 𝐷 )
65	63 64	eqtr4di	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) = ( 1_o × { 𝐷 } ) )
66		fconst6g	⊢ ( 𝐷 ∈ ℕ₀ → ( 1_o × { 𝐷 } ) : 1_o ⟶ ℕ₀ )
67	15 16	elmap	⊢ ( ( 1_o × { 𝐷 } ) ∈ ( ℕ₀ ↑_m 1_o ) ↔ ( 1_o × { 𝐷 } ) : 1_o ⟶ ℕ₀ )
68	66 67	sylibr	⊢ ( 𝐷 ∈ ℕ₀ → ( 1_o × { 𝐷 } ) ∈ ( ℕ₀ ↑_m 1_o ) )
69	68	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 1_o × { 𝐷 } ) ∈ ( ℕ₀ ↑_m 1_o ) )
70	65 69	eqeltrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) ∈ ( ℕ₀ ↑_m 1_o ) )
71		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → 𝐶 ∈ 𝐾 )
72	33 57 46 47 1 2 49 51 70 71	mplmon2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝐶 · ( 𝑦 ∈ ( ℕ₀ ↑_m 1_o ) ↦ if ( 𝑦 = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , ( 1_r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ ( ℕ₀ ↑_m 1_o ) ↦ if ( 𝑦 = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , 𝐶 , 0 ) ) )
73	45 56 72	3eqtr2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) = ( 𝑦 ∈ ( ℕ₀ ↑_m 1_o ) ↦ if ( 𝑦 = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , 𝐶 , 0 ) ) )
74		eqeq1	⊢ ( 𝑦 = ( 1_o × { 𝑥 } ) → ( 𝑦 = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) ↔ ( 1_o × { 𝑥 } ) = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) ) )
75	74	ifbid	⊢ ( 𝑦 = ( 1_o × { 𝑥 } ) → if ( 𝑦 = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , 𝐶 , 0 ) = if ( ( 1_o × { 𝑥 } ) = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , 𝐶 , 0 ) )
76	19 20 73 75	fmptco	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ∘ ( 𝑥 ∈ ℕ₀ ↦ ( 1_o × { 𝑥 } ) ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( ( 1_o × { 𝑥 } ) = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , 𝐶 , 0 ) ) )
77	65	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) = ( 1_o × { 𝐷 } ) )
78	77	eqeq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 1_o × { 𝑥 } ) = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) ↔ ( 1_o × { 𝑥 } ) = ( 1_o × { 𝐷 } ) ) )
79		fveq1	⊢ ( ( 1_o × { 𝑥 } ) = ( 1_o × { 𝐷 } ) → ( ( 1_o × { 𝑥 } ) ‘ ∅ ) = ( ( 1_o × { 𝐷 } ) ‘ ∅ ) )
80		vex	⊢ 𝑥 ∈ V
81	80	fvconst2	⊢ ( ∅ ∈ 1_o → ( ( 1_o × { 𝑥 } ) ‘ ∅ ) = 𝑥 )
82	52 81	mp1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 1_o × { 𝑥 } ) ‘ ∅ ) = 𝑥 )
83		simpl3	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → 𝐷 ∈ ℕ₀ )
84		fvconst2g	⊢ ( ( 𝐷 ∈ ℕ₀ ∧ ∅ ∈ 1_o ) → ( ( 1_o × { 𝐷 } ) ‘ ∅ ) = 𝐷 )
85	83 52 84	sylancl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 1_o × { 𝐷 } ) ‘ ∅ ) = 𝐷 )
86	82 85	eqeq12d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( ( 1_o × { 𝑥 } ) ‘ ∅ ) = ( ( 1_o × { 𝐷 } ) ‘ ∅ ) ↔ 𝑥 = 𝐷 ) )
87	79 86	imbitrid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 1_o × { 𝑥 } ) = ( 1_o × { 𝐷 } ) → 𝑥 = 𝐷 ) )
88		sneq	⊢ ( 𝑥 = 𝐷 → { 𝑥 } = { 𝐷 } )
89	88	xpeq2d	⊢ ( 𝑥 = 𝐷 → ( 1_o × { 𝑥 } ) = ( 1_o × { 𝐷 } ) )
90	87 89	impbid1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 1_o × { 𝑥 } ) = ( 1_o × { 𝐷 } ) ↔ 𝑥 = 𝐷 ) )
91	78 90	bitrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 1_o × { 𝑥 } ) = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) ↔ 𝑥 = 𝐷 ) )
92	91	ifbid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → if ( ( 1_o × { 𝑥 } ) = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , 𝐶 , 0 ) = if ( 𝑥 = 𝐷 , 𝐶 , 0 ) )
93	92	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( 𝑥 ∈ ℕ₀ ↦ if ( ( 1_o × { 𝑥 } ) = ( 𝑏 ∈ 1_o ↦ if ( 𝑏 = ∅ , 𝐷 , 0 ) ) , 𝐶 , 0 ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )
94	13 76 93	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ₀ ) → ( coe₁ ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )

Metamath Proof Explorer

Theorem coe1tm

Proof