Theorem coe1vr1

Description: Polynomial coefficient of the variable. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	coe1vr1.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1vr1.2	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	coe1vr1.3	$$⊢\phi \to R\in \mathrm{Ring}$$
	coe1vr1.4	$$⊢\underset{\dot{}}{0}=0_R$$
	coe1vr1.5	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	coe1vr1	$$⊢\phi \to {\mathrm{coe}}_1\left(X\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=1,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1vr1.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		coe1vr1.2	$$⊢X={\mathrm{var}}_1\left(R\right)$$
3		coe1vr1.3	$$⊢\phi \to R\in \mathrm{Ring}$$
4		coe1vr1.4	$$⊢\underset{\dot{}}{0}=0_R$$
5		coe1vr1.5	$$⊢\underset{\dot{}}{1}=1_R$$
6		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
7	2 1 6	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_P$$
8		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
9	8 6	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
10		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
11	9 10	mulg1	$$⊢X\in {\mathrm{Base}}_P\to 1{\cdot }_{{\mathrm{mulGrp}}_P}X=X$$
12	3 7 11	3syl	$$⊢\phi \to 1{\cdot }_{{\mathrm{mulGrp}}_P}X=X$$
13	12	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)={\mathrm{coe}}_1\left(X\right)$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15	14	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
16	1 2 10 3 15 4 5	coe1mon	$$⊢\phi \to {\mathrm{coe}}_1\left(1{\cdot }_{{\mathrm{mulGrp}}_P}X\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=1,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
17	13 16	eqtr3d	$$⊢\phi \to {\mathrm{coe}}_1\left(X\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=1,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$