Metamath Proof Explorer

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)

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}×{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}×{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 df-sca ${⊢}\mathrm{Scalar}=\mathrm{Slot}5$
8 5nn ${⊢}5\in ℕ$
9 5lt10 ${⊢}5<10$
10 1 2 3 7 8 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)$