ply1sca2

Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015)

		Ref	Expression
	Hypothesis	ply1lmod.p	$⊢ P = {Poly}_{1} (R)$
	Assertion	ply1sca2	$⊢ I (R) = Scalar (P)$

Step	Hyp	Ref	Expression
1		ply1lmod.p	$⊢ P = {Poly}_{1} (R)$
2		fvi	$⊢ R \in V \to I (R) = R$
3	1	ply1sca	$⊢ R \in V \to R = Scalar (P)$
4	2 3	eqtrd	$⊢ R \in V \to I (R) = Scalar (P)$
5		fvprc	$⊢ \neg R \in V \to I (R) = \emptyset$
6		fvprc	$⊢ \neg R \in V \to {Poly}_{1} (R) = \emptyset$
7	6	fveq2d	$⊢ \neg R \in V \to Scalar ({Poly}_{1} (R)) = Scalar (\emptyset)$
8	1	fveq2i	$⊢ Scalar (P) = Scalar ({Poly}_{1} (R))$
9		scaid	$⊢ Scalar = Slot Scalar (ndx)$
10	9	str0	$⊢ \emptyset = Scalar (\emptyset)$
11	7 8 10	3eqtr4g	$⊢ \neg R \in V \to Scalar (P) = \emptyset$
12	5 11	eqtr4d	$⊢ \neg R \in V \to I (R) = Scalar (P)$
13	4 12	pm2.61i	$⊢ I (R) = Scalar (P)$

Metamath Proof Explorer