Theorem subrgvr1cl

Description: The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 5-Jul-2015)

	Ref	Expression
Hypotheses	subrgvr1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	subrgvr1.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	subrgvr1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	subrgvr1cl.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	subrgvr1cl.b	$$⊢B={\mathrm{Base}}_U$$
Assertion	subrgvr1cl	$$⊢\phi \to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		subrgvr1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
2		subrgvr1.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
3		subrgvr1.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
4		subrgvr1cl.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
5		subrgvr1cl.b	$$⊢B={\mathrm{Base}}_U$$
6	1	vr1val	$$⊢X=\left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)$$
7		eqid	$$⊢1_{𝑜}\mathrm{mVar}R=1_{𝑜}\mathrm{mVar}R$$
8		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
9	8	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
10		eqid	$$⊢1_{𝑜}\mathrm{mPoly}H=1_{𝑜}\mathrm{mPoly}H$$
11		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
12	4 11 5	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
13	7 9 2 3 10 12	subrgmvrf	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}R\right):1_{𝑜}⟶B$$
14		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
15		ffvelcdm	$$⊢\left(\left(1_{𝑜}\mathrm{mVar}R\right):1_{𝑜}⟶B\wedge \varnothing \in 1_{𝑜}\right)\to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)\in B$$
16	13 14 15	sylancl	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)\in B$$
17	6 16	eqeltrid	$$⊢\phi \to X\in B$$