Metamath Proof Explorer

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