Theorem ply1sclid

Description: Recover the base scalar from a scalar polynomial. (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)$$
	ply1sclid.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	ply1sclid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to X={\mathrm{coe}}_1\left(A\left(X\right)\right)\left(0\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		ply1sclid.k	$$⊢K={\mathrm{Base}}_R$$
4		eqid	$$⊢0_R=0_R$$
5	1 2 3 4	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,0_R\right)\right)$$
6	5	fveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to {\mathrm{coe}}_1\left(A\left(X\right)\right)\left(0\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,0_R\right)\right)\left(0\right)$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8		iftrue	$$⊢x=0\to if\left(x=0,X,0_R\right)=X$$
9		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,0_R\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,0_R\right)\right)$$
10	8 9	fvmptg	$$⊢\left(0\in {\mathbb{N}}_0\wedge X\in K\right)\to \left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,0_R\right)\right)\left(0\right)=X$$
11	7 10	mpan	$$⊢X\in K\to \left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,0_R\right)\right)\left(0\right)=X$$
12	11	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to \left(x\in {\mathbb{N}}_0⟼if\left(x=0,X,0_R\right)\right)\left(0\right)=X$$
13	6 12	eqtr2d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to X={\mathrm{coe}}_1\left(A\left(X\right)\right)\left(0\right)$$