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	4 5	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
12	7 9 2 3 10 11	subrgmvrf	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}R\right):1_{𝑜}⟶B$$
13		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
14		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$$
15	12 13 14	sylancl	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)\in B$$
16	6 15	eqeltrid	$$⊢\phi \to X\in B$$