ply1lss

Description: Univariate polynomials form a linear subspace of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	ply1val.1	$⊢ P = {Poly}_{1} (R)$
	ply1val.2	$⊢ S = {PwSer}_{1} (R)$
	ply1bas.u	$⊢ U = {Base}_{P}$
Assertion	ply1lss	$⊢ R \in Ring \to U \in LSubSp (S)$

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	$⊢ P = {Poly}_{1} (R)$
2		ply1val.2	$⊢ S = {PwSer}_{1} (R)$
3		ply1bas.u	$⊢ U = {Base}_{P}$
4		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
5		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
6	1 2 3	ply1bas	$⊢ U = {Base}_{(1_{𝑜} mPoly R)}$
7		1on	$⊢ 1_{𝑜} \in On$
8	7	a1i	$⊢ R \in Ring \to 1_{𝑜} \in On$
9		id	$⊢ R \in Ring \to R \in Ring$
10	4 5 6 8 9	mpllss	$⊢ R \in Ring \to U \in LSubSp (1_{𝑜} mPwSer R)$
11		eqidd	$⊢ R \in Ring \to {Base}_{(1_{𝑜} mPwSer R)} = {Base}_{(1_{𝑜} mPwSer R)}$
12	2	psr1val	$⊢ S = (1_{𝑜} ordPwSer R) (\emptyset)$
13		0ss	$⊢ \emptyset \subseteq 1_{𝑜} \times 1_{𝑜}$
14	13	a1i	$⊢ R \in Ring \to \emptyset \subseteq 1_{𝑜} \times 1_{𝑜}$
15	4 12 14	opsrbas	$⊢ R \in Ring \to {Base}_{(1_{𝑜} mPwSer R)} = {Base}_{S}$
16		ssv	$⊢ {Base}_{(1_{𝑜} mPwSer R)} \subseteq V$
17	16	a1i	$⊢ R \in Ring \to {Base}_{(1_{𝑜} mPwSer R)} \subseteq V$
18	4 12 14	opsrplusg	$⊢ R \in Ring \to +_{(1_{𝑜} mPwSer R)} = +_{S}$
19	18	oveqdr	$⊢ (R \in Ring \land (x \in V \land y \in V)) \to x +_{(1_{𝑜} mPwSer R)} y = x +_{S} y$
20		ovexd	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{(1_{𝑜} mPwSer R)})) \to x \cdot_{(1_{𝑜} mPwSer R)} y \in V$
21	4 12 14	opsrvsca	$⊢ R \in Ring \to \cdot_{(1_{𝑜} mPwSer R)} = \cdot_{S}$
22	21	oveqdr	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{(1_{𝑜} mPwSer R)})) \to x \cdot_{(1_{𝑜} mPwSer R)} y = x \cdot_{S} y$
23	4 8 9	psrsca	$⊢ R \in Ring \to R = Scalar (1_{𝑜} mPwSer R)$
24	23	fveq2d	$⊢ R \in Ring \to {Base}_{R} = {Base}_{Scalar (1_{𝑜} mPwSer R)}$
25	4 12 14 8 9	opsrsca	$⊢ R \in Ring \to R = Scalar (S)$
26	25	fveq2d	$⊢ R \in Ring \to {Base}_{R} = {Base}_{Scalar (S)}$
27	11 15 17 19 20 22 24 26	lsspropd	$⊢ R \in Ring \to LSubSp (1_{𝑜} mPwSer R) = LSubSp (S)$
28	10 27	eleqtrd	$⊢ R \in Ring \to U \in LSubSp (S)$

Metamath Proof Explorer

Theorem ply1lss

Proof