This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) (Revised by AV, 1-Nov-2024)

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

Proof

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