Theorem evl1vard

Description: Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	evl1var.q	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	evl1var.v	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	evl1var.b	$$⊢B={\mathrm{Base}}_R$$
	evl1vard.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	evl1vard.u	$$⊢U={\mathrm{Base}}_P$$
	evl1vard.1	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1vard.2	$$⊢\phi \to Y\in B$$
Assertion	evl1vard	$$⊢\phi \to \left(X\in U\wedge O\left(X\right)\left(Y\right)=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		evl1var.q	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
2		evl1var.v	$$⊢X={\mathrm{var}}_1\left(R\right)$$
3		evl1var.b	$$⊢B={\mathrm{Base}}_R$$
4		evl1vard.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
5		evl1vard.u	$$⊢U={\mathrm{Base}}_P$$
6		evl1vard.1	$$⊢\phi \to R\in \mathrm{CRing}$$
7		evl1vard.2	$$⊢\phi \to Y\in B$$
8		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
9	2 4 5	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in U$$
10	6 8 9	3syl	$$⊢\phi \to X\in U$$
11	1 2 3	evl1var	$$⊢R\in \mathrm{CRing}\to O\left(X\right)={\mathrm{I}\upharpoonright }_B$$
12	6 11	syl	$$⊢\phi \to O\left(X\right)={\mathrm{I}\upharpoonright }_B$$
13	12	fveq1d	$$⊢\phi \to O\left(X\right)\left(Y\right)=\left({\mathrm{I}\upharpoonright }_B\right)\left(Y\right)$$
14		fvresi	$$⊢Y\in B\to \left({\mathrm{I}\upharpoonright }_B\right)\left(Y\right)=Y$$
15	7 14	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_B\right)\left(Y\right)=Y$$
16	13 15	eqtrd	$$⊢\phi \to O\left(X\right)\left(Y\right)=Y$$
17	10 16	jca	$$⊢\phi \to \left(X\in U\wedge O\left(X\right)\left(Y\right)=Y\right)$$