Theorem vr1cl2

Description: The variable X is a member of the power series algebra R [ [ X ] ] . (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	vr1val.1	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	vr1cl2.2	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
	vr1cl2.3	$$⊢B={\mathrm{Base}}_S$$
Assertion	vr1cl2	$$⊢R\in \mathrm{Ring}\to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		vr1val.1	$$⊢X={\mathrm{var}}_1\left(R\right)$$
2		vr1cl2.2	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
3		vr1cl2.3	$$⊢B={\mathrm{Base}}_S$$
4	1	vr1val	$$⊢X=\left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
6		eqid	$$⊢1_{𝑜}\mathrm{mVar}R=1_{𝑜}\mathrm{mVar}R$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
8		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
9	8	a1i	$$⊢R\in \mathrm{Ring}\to 1_{𝑜}\in \mathrm{On}$$
10		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
11		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
12	11	a1i	$$⊢R\in \mathrm{Ring}\to \varnothing \in 1_{𝑜}$$
13	5 6 7 9 10 12	mvrcl2	$$⊢R\in \mathrm{Ring}\to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
14	2	psr1val	$$⊢S=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
15		0ss	$$⊢\varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
16	15	a1i	$$⊢R\in \mathrm{Ring}\to \varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
17	5 14 16	opsrbas	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\mathrm{Base}}_S$$
18	17 3	eqtr4di	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}=B$$
19	13 18	eleqtrd	$$⊢R\in \mathrm{Ring}\to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)\in B$$
20	4 19	eqeltrid	$$⊢R\in \mathrm{Ring}\to X\in B$$