Theorem subrgvr1

Description: The variables in a subring polynomial algebra are the same as the original ring. (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$$
Assertion	subrgvr1	$$⊢\phi \to X={\mathrm{var}}_1\left(H\right)$$

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		eqid	$$⊢1_{𝑜}\mathrm{mVar}R=1_{𝑜}\mathrm{mVar}R$$
5		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
6	5	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
7	4 6 2 3	subrgmvr	$$⊢\phi \to 1_{𝑜}\mathrm{mVar}R=1_{𝑜}\mathrm{mVar}H$$
8	7	fveq1d	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)=\left(1_{𝑜}\mathrm{mVar}H\right)\left(\varnothing \right)$$
9	1	vr1val	$$⊢X=\left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)$$
10		eqid	$$⊢{\mathrm{var}}_1\left(H\right)={\mathrm{var}}_1\left(H\right)$$
11	10	vr1val	$$⊢{\mathrm{var}}_1\left(H\right)=\left(1_{𝑜}\mathrm{mVar}H\right)\left(\varnothing \right)$$
12	8 9 11	3eqtr4g	$$⊢\phi \to X={\mathrm{var}}_1\left(H\right)$$