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

Metamath Proof Explorer

Theorem psr1sca

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

		Ref	Expression
	Hypothesis	psr1lmod.p	$⊢ P = {PwSer}_{1} (R)$
	Assertion	psr1sca	$⊢ R \in V \to R = Scalar (P)$

Step	Hyp	Ref	Expression
1		psr1lmod.p	$⊢ P = {PwSer}_{1} (R)$
2		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
3	1	psr1val	$⊢ P = (1_{𝑜} ordPwSer R) (\emptyset)$
4		0ss	$⊢ \emptyset \subseteq 1_{𝑜} \times 1_{𝑜}$
5	4	a1i	$⊢ R \in V \to \emptyset \subseteq 1_{𝑜} \times 1_{𝑜}$
6		1on	$⊢ 1_{𝑜} \in On$
7	6	a1i	$⊢ R \in V \to 1_{𝑜} \in On$
8		id	$⊢ R \in V \to R \in V$
9	2 3 5 7 8	opsrsca	$⊢ R \in V \to R = Scalar (P)$