Theorem coe1scl

Description: Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	ply1scl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1scl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	coe1scl.k	$$⊢K={\mathrm{Base}}_R$$
	coe1scl.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	coe1scl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to {\mathrm{coe}}_1\left(A\left(X\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1scl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
3		coe1scl.k	$$⊢K={\mathrm{Base}}_R$$
4		coe1scl.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		eqid	$$⊢{\mathrm{var}}_1\left(R\right)={\mathrm{var}}_1\left(R\right)$$
6		eqid	$$⊢{\cdot }_P={\cdot }_P$$
7		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
8		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
9	3 1 5 6 7 8 2	ply1scltm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to A\left(X\right)=X{\cdot }_P\left(0{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)$$
10	9	fveq2d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to {\mathrm{coe}}_1\left(A\left(X\right)\right)={\mathrm{coe}}_1\left(X{\cdot }_P\left(0{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)$$
11		0nn0	$$⊢0\in {\mathbb{N}}_0$$
12	4 3 1 5 6 7 8	coe1tm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\wedge 0\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(X{\cdot }_P\left(0{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,\underset{\dot{}}{0}\right)\right)$$
13	11 12	mp3an3	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to {\mathrm{coe}}_1\left(X{\cdot }_P\left(0{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,\underset{\dot{}}{0}\right)\right)$$
14	10 13	eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to {\mathrm{coe}}_1\left(A\left(X\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,\underset{\dot{}}{0}\right)\right)$$