Theorem evl1scad

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

	Ref	Expression
Hypotheses	evl1sca.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	evl1sca.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	evl1sca.b	$$⊢B={\mathrm{Base}}_R$$
	evl1sca.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	evl1scad.u	$$⊢U={\mathrm{Base}}_P$$
	evl1scad.1	$$⊢\phi \to R\in \mathrm{CRing}$$
	evl1scad.2	$$⊢\phi \to X\in B$$
	evl1scad.3	$$⊢\phi \to Y\in B$$
Assertion	evl1scad	$$⊢\phi \to \left(A\left(X\right)\in U\wedge O\left(A\left(X\right)\right)\left(Y\right)=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		evl1sca.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
2		evl1sca.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		evl1sca.b	$$⊢B={\mathrm{Base}}_R$$
4		evl1sca.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
5		evl1scad.u	$$⊢U={\mathrm{Base}}_P$$
6		evl1scad.1	$$⊢\phi \to R\in \mathrm{CRing}$$
7		evl1scad.2	$$⊢\phi \to X\in B$$
8		evl1scad.3	$$⊢\phi \to Y\in B$$
9		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
10	2 4 3 5	ply1sclf	$$⊢R\in \mathrm{Ring}\to A:B⟶U$$
11	6 9 10	3syl	$$⊢\phi \to A:B⟶U$$
12	11 7	ffvelrnd	$$⊢\phi \to A\left(X\right)\in U$$
13	1 2 3 4	evl1sca	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\right)\to O\left(A\left(X\right)\right)=B\times \left\{X\right\}$$
14	6 7 13	syl2anc	$$⊢\phi \to O\left(A\left(X\right)\right)=B\times \left\{X\right\}$$
15	14	fveq1d	$$⊢\phi \to O\left(A\left(X\right)\right)\left(Y\right)=\left(B\times \left\{X\right\}\right)\left(Y\right)$$
16		fvconst2g	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(B\times \left\{X\right\}\right)\left(Y\right)=X$$
17	7 8 16	syl2anc	$$⊢\phi \to \left(B\times \left\{X\right\}\right)\left(Y\right)=X$$
18	15 17	eqtrd	$$⊢\phi \to O\left(A\left(X\right)\right)\left(Y\right)=X$$
19	12 18	jca	$$⊢\phi \to \left(A\left(X\right)\in U\wedge O\left(A\left(X\right)\right)\left(Y\right)=X\right)$$