vr1cl2

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

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

Metamath Proof Explorer