Theorem coe1id

Description: Coefficient vector of the unit polynomial. (Contributed by AV, 9-Aug-2019)

	Ref	Expression
Hypotheses	coe1id.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1id.i	$$⊢I=1_P$$
	coe1id.0	$$⊢\underset{\dot{}}{0}=0_R$$
	coe1id.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	coe1id	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(I\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1id.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		coe1id.i	$$⊢I=1_P$$
3		coe1id.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		coe1id.1	$$⊢\underset{\dot{}}{1}=1_R$$
5		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
6	1 5 4 2	ply1scl1	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)=I$$
7	6	eqcomd	$$⊢R\in \mathrm{Ring}\to I=\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)$$
8	7	fveq2d	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(I\right)={\mathrm{coe}}_1\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\right)$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10	9 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
11	1 5 9 3	coe1scl	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\to {\mathrm{coe}}_1\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
12	10 11	mpdan	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
13	8 12	eqtrd	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(I\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$