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 = {PwSer}_{1} (R)$
	Assertion	psr1sca2	$⊢ I (R) = Scalar (P)$

Step	Hyp	Ref	Expression
1		psr1lmod.p	$⊢ P = {PwSer}_{1} (R)$
2		fvi	$⊢ R \in V \to I (R) = R$
3	1	psr1sca	$⊢ R \in V \to R = Scalar (P)$
4	2 3	eqtrd	$⊢ R \in V \to I (R) = Scalar (P)$
5		scaid	$⊢ Scalar = Slot Scalar (ndx)$
6	5	str0	$⊢ \emptyset = Scalar (\emptyset)$
7		fvprc	$⊢ \neg R \in V \to I (R) = \emptyset$
8		fvprc	$⊢ \neg R \in V \to {PwSer}_{1} (R) = \emptyset$
9	1 8	eqtrid	$⊢ \neg R \in V \to P = \emptyset$
10	9	fveq2d	$⊢ \neg R \in V \to Scalar (P) = Scalar (\emptyset)$
11	6 7 10	3eqtr4a	$⊢ \neg R \in V \to I (R) = Scalar (P)$
12	4 11	pm2.61i	$⊢ I (R) = Scalar (P)$

Metamath Proof Explorer