Theorem psr1sca2

Description: Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 26-Mar-2015) (Revised by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypothesis	psr1lmod.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
Assertion	psr1sca2	$$⊢\mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		psr1lmod.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
2		fvi	$$⊢R\in \mathrm{V}\to \mathrm{I}\left(R\right)=R$$
3	1	psr1sca	$$⊢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		df-sca	$$⊢\mathrm{Scalar}=\mathrm{Slot}5$$
6	5	str0	$$⊢\varnothing =\mathrm{Scalar}\left(\varnothing \right)$$
7		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\varnothing$$
8		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{PwSer}}_1\left(R\right)=\varnothing$$
9	1 8	syl5eq	$$⊢\neg R\in \mathrm{V}\to P=\varnothing$$
10	9	fveq2d	$$⊢\neg R\in \mathrm{V}\to \mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(\varnothing \right)$$
11	6 7 10	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$
12	4 11	pm2.61i	$$⊢\mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$