Theorem coe1tm

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

	Ref	Expression
Hypotheses	coe1tm.z	⊢ 0 = ( 0g ‘ 𝑅 )
	coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1tm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1tm.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	coe1tm.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	coe1tm.e	⊢ ↑ = ( .g ‘ 𝑁 )
Assertion	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 𝐷 , 𝐶 , 0 ) ) )

Proof

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