Theorem lineval

Description: A term of the form x - C evaluated for x = V results in V - C (part of ply1remlem ). (Contributed by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	linply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	linply1.b	$$⊢B={\mathrm{Base}}_P$$
	linply1.k	$$⊢K={\mathrm{Base}}_R$$
	linply1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	linply1.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	linply1.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	linply1.g	$$⊢G=X\underset{\dot{}}{-}A\left(C\right)$$
	linply1.c	$$⊢\phi \to C\in K$$
	lineval.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	lineval.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	lineval.v	$$⊢\phi \to V\in K$$
Assertion	lineval	$$⊢\phi \to O\left(G\right)\left(V\right)=V{-}_{R}C$$

Proof

Step	Hyp	Ref	Expression
1		linply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		linply1.b	$$⊢B={\mathrm{Base}}_P$$
3		linply1.k	$$⊢K={\mathrm{Base}}_R$$
4		linply1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
5		linply1.m	$$⊢\underset{\dot{}}{-}={-}_P$$
6		linply1.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
7		linply1.g	$$⊢G=X\underset{\dot{}}{-}A\left(C\right)$$
8		linply1.c	$$⊢\phi \to C\in K$$
9		lineval.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
10		lineval.r	$$⊢\phi \to R\in \mathrm{CRing}$$
11		lineval.v	$$⊢\phi \to V\in K$$
12	7	fveq2i	$$⊢O\left(G\right)=O\left(X\underset{\dot{}}{-}A\left(C\right)\right)$$
13	12	fveq1i	$$⊢O\left(G\right)\left(V\right)=O\left(X\underset{\dot{}}{-}A\left(C\right)\right)\left(V\right)$$
14	9 4 3 1 2 10 11	evl1vard	$$⊢\phi \to \left(X\in B\wedge O\left(X\right)\left(V\right)=V\right)$$
15	9 1 3 6 2 10 8 11	evl1scad	$$⊢\phi \to \left(A\left(C\right)\in B\wedge O\left(A\left(C\right)\right)\left(V\right)=C\right)$$
16		eqid	$$⊢{-}_R={-}_R$$
17	9 1 3 2 10 11 14 15 5 16	evl1subd	$$⊢\phi \to \left(X\underset{\dot{}}{-}A\left(C\right)\in B\wedge O\left(X\underset{\dot{}}{-}A\left(C\right)\right)\left(V\right)=V{-}_{R}C\right)$$
18	17	simprd	$$⊢\phi \to O\left(X\underset{\dot{}}{-}A\left(C\right)\right)\left(V\right)=V{-}_{R}C$$
19	13 18	syl5eq	$$⊢\phi \to O\left(G\right)\left(V\right)=V{-}_{R}C$$