Theorem opsrsca

Description: The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (Revised by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	opsrbas.s	$$⊢S=I\mathrm{mPwSer}R$$
	opsrbas.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
	opsrbas.t	$$⊢\phi \to T\subseteq I\times I$$
	opsrsca.i	$$⊢\phi \to I\in V$$
	opsrsca.r	$$⊢\phi \to R\in W$$
Assertion	opsrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		opsrbas.s	$$⊢S=I\mathrm{mPwSer}R$$
2		opsrbas.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
3		opsrbas.t	$$⊢\phi \to T\subseteq I\times I$$
4		opsrsca.i	$$⊢\phi \to I\in V$$
5		opsrsca.r	$$⊢\phi \to R\in W$$
6	1 4 5	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(S\right)$$
7		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
8		plendxnscandx	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
9	8	necomi	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}$$
10	1 2 3 7 9	opsrbaslem	$$⊢\phi \to \mathrm{Scalar}\left(S\right)=\mathrm{Scalar}\left(O\right)$$
11	6 10	eqtrd	$$⊢\phi \to R=\mathrm{Scalar}\left(O\right)$$