Theorem ply1idvr1

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

	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}}_R={\mathrm{Base}}_R$$
6		eqid	$$⊢1_R=1_R$$
7	5 6	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
8		eqid	$$⊢{\cdot }_P={\cdot }_P$$
9		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
10	5 1 2 8 3 4 9	ply1scltm	$$⊢\left(R\in \mathrm{Ring}\wedge 1_R\in {\mathrm{Base}}_R\right)\to \mathrm{algSc}\left(P\right)\left(1_R\right)=1_R{\cdot }_P\left(0\underset{\dot{}}{\times }X\right)$$
11	7 10	mpdan	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right)\left(1_R\right)=1_R{\cdot }_P\left(0\underset{\dot{}}{\times }X\right)$$
12	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
13	12	fveq2d	$$⊢R\in \mathrm{Ring}\to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
14	13	oveq1d	$$⊢R\in \mathrm{Ring}\to 1_R{\cdot }_P\left(0\underset{\dot{}}{\times }X\right)=1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(0\underset{\dot{}}{\times }X\right)$$
15	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
16		0nn0	$$⊢0\in {\mathbb{N}}_0$$
17		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
18	1 2 3 4 17	ply1moncl	$$⊢\left(R\in \mathrm{Ring}\wedge 0\in {\mathbb{N}}_0\right)\to 0\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
19	16 18	mpan2	$$⊢R\in \mathrm{Ring}\to 0\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
20		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
21		eqid	$$⊢1_{\mathrm{Scalar}\left(P\right)}=1_{\mathrm{Scalar}\left(P\right)}$$
22	17 20 8 21	lmodvs1	$$⊢\left(P\in \mathrm{LMod}\wedge 0\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\right)\to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(0\underset{\dot{}}{\times }X\right)=0\underset{\dot{}}{\times }X$$
23	15 19 22	syl2anc	$$⊢R\in \mathrm{Ring}\to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(0\underset{\dot{}}{\times }X\right)=0\underset{\dot{}}{\times }X$$
24	11 14 23	3eqtrrd	$$⊢R\in \mathrm{Ring}\to 0\underset{\dot{}}{\times }X=\mathrm{algSc}\left(P\right)\left(1_R\right)$$
25		eqid	$$⊢1_P=1_P$$
26	1 9 6 25	ply1scl1	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right)\left(1_R\right)=1_P$$
27	24 26	eqtrd	$$⊢R\in \mathrm{Ring}\to 0\underset{\dot{}}{\times }X=1_P$$