Theorem ply1sca2

Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypothesis	ply1lmod.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
Assertion	ply1sca2	$$⊢\mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1lmod.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		fvi	$$⊢R\in \mathrm{V}\to \mathrm{I}\left(R\right)=R$$
3	1	ply1sca	$$⊢R\in \mathrm{V}\to R=\mathrm{Scalar}\left(P\right)$$
4	2 3	eqtrd	$$⊢R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$
5		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\varnothing$$
6		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=\varnothing$$
7	6	fveq2d	$$⊢\neg R\in \mathrm{V}\to \mathrm{Scalar}\left({\mathrm{Poly}}_1\left(R\right)\right)=\mathrm{Scalar}\left(\varnothing \right)$$
8	1	fveq2i	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
9		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
10	9	str0	$$⊢\varnothing =\mathrm{Scalar}\left(\varnothing \right)$$
11	7 8 10	3eqtr4g	$$⊢\neg R\in \mathrm{V}\to \mathrm{Scalar}\left(P\right)=\varnothing$$
12	5 11	eqtr4d	$$⊢\neg R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$
13	4 12	pm2.61i	$$⊢\mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$