Theorem ply1idvr1

Description: The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019) (Proof shortened by SN, 3-Jul-2025)

	Ref	Expression
Hypotheses	ply1idvr1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1idvr1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	ply1idvr1.n	$$⊢N={\mathrm{mulGrp}}_P$$
	ply1idvr1.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
Assertion	ply1idvr1	$$⊢R\in \mathrm{Ring}\to 0\underset{\dot{}}{\times }X=1_P$$

Proof

Step	Hyp	Ref	Expression
1		ply1idvr1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1idvr1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
3		ply1idvr1.n	$$⊢N={\mathrm{mulGrp}}_P$$
4		ply1idvr1.e	$$⊢\underset{\dot{}}{\times }={\cdot }_N$$
5		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
6	2 1 5	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_P$$
7	3 5	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_N$$
8		eqid	$$⊢1_P=1_P$$
9	3 8	ringidval	$$⊢1_P=0_N$$
10	7 9 4	mulg0	$$⊢X\in {\mathrm{Base}}_P\to 0\underset{\dot{}}{\times }X=1_P$$
11	6 10	syl	$$⊢R\in \mathrm{Ring}\to 0\underset{\dot{}}{\times }X=1_P$$