Theorem ply1vr1smo

Description: The variable in a polynomial expressed as scaled monomial. (Contributed by AV, 12-Aug-2019)

	Ref	Expression
Hypotheses	ply1vr1smo.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1vr1smo.i	$$⊢\underset{\dot{}}{1}=1_R$$
	ply1vr1smo.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	ply1vr1smo.m	$$⊢G={\mathrm{mulGrp}}_P$$
	ply1vr1smo.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	ply1vr1smo.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
Assertion	ply1vr1smo	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(1\underset{\dot{}}{\times }X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		ply1vr1smo.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1vr1smo.i	$$⊢\underset{\dot{}}{1}=1_R$$
3		ply1vr1smo.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
4		ply1vr1smo.m	$$⊢G={\mathrm{mulGrp}}_P$$
5		ply1vr1smo.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
6		ply1vr1smo.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
7	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
8	7	fveq2d	$$⊢R\in \mathrm{Ring}\to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
9	2 8	syl5eq	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(P\right)}$$
10	9	oveq1d	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(1\underset{\dot{}}{\times }X\right)=1_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{·}\left(1\underset{\dot{}}{\times }X\right)$$
11	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
12		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
13	6 1 12	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in {\mathrm{Base}}_P$$
14	4 12	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_G$$
15	14 5	mulg1	$$⊢X\in {\mathrm{Base}}_P\to 1\underset{\dot{}}{\times }X=X$$
16	13 15	syl	$$⊢R\in \mathrm{Ring}\to 1\underset{\dot{}}{\times }X=X$$
17	16 13	eqeltrd	$$⊢R\in \mathrm{Ring}\to 1\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
18		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
19		eqid	$$⊢1_{\mathrm{Scalar}\left(P\right)}=1_{\mathrm{Scalar}\left(P\right)}$$
20	12 18 3 19	lmodvs1	$$⊢\left(P\in \mathrm{LMod}\wedge 1\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\right)\to 1_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{·}\left(1\underset{\dot{}}{\times }X\right)=1\underset{\dot{}}{\times }X$$
21	11 17 20	syl2anc	$$⊢R\in \mathrm{Ring}\to 1_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{·}\left(1\underset{\dot{}}{\times }X\right)=1\underset{\dot{}}{\times }X$$
22	10 21 16	3eqtrd	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(1\underset{\dot{}}{\times }X\right)=X$$