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 = ( Poly1 ` R )
	linply1.b	|- B = ( Base ` P )
	linply1.k	|- K = ( Base ` R )
	linply1.x	|- X = ( var1 ` R )
	linply1.m	|- .- = ( -g ` P )
	linply1.a	|- A = ( algSc ` P )
	linply1.g	|- G = ( X .- ( A ` C ) )
	linply1.c	|- ( ph -> C e. K )
	lineval.o	|- O = ( eval1 ` R )
	lineval.r	|- ( ph -> R e. CRing )
	lineval.v	|- ( ph -> V e. K )
Assertion	lineval	|- ( ph -> ( ( O ` G ) ` V ) = ( V ( -g ` R ) C ) )

Proof

Step	Hyp	Ref	Expression
1		linply1.p	|- P = ( Poly1 ` R )
2		linply1.b	|- B = ( Base ` P )
3		linply1.k	|- K = ( Base ` R )
4		linply1.x	|- X = ( var1 ` R )
5		linply1.m	|- .- = ( -g ` P )
6		linply1.a	|- A = ( algSc ` P )
7		linply1.g	|- G = ( X .- ( A ` C ) )
8		linply1.c	|- ( ph -> C e. K )
9		lineval.o	|- O = ( eval1 ` R )
10		lineval.r	|- ( ph -> R e. CRing )
11		lineval.v	|- ( ph -> V e. K )
12	7	fveq2i	|- ( O ` G ) = ( O ` ( X .- ( A ` C ) ) )
13	12	fveq1i	|- ( ( O ` G ) ` V ) = ( ( O ` ( X .- ( A ` C ) ) ) ` V )
14	9 4 3 1 2 10 11	evl1vard	|- ( ph -> ( X e. B /\ ( ( O ` X ) ` V ) = V ) )
15	9 1 3 6 2 10 8 11	evl1scad	|- ( ph -> ( ( A ` C ) e. B /\ ( ( O ` ( A ` C ) ) ` V ) = C ) )
16		eqid	|- ( -g ` R ) = ( -g ` R )
17	9 1 3 2 10 11 14 15 5 16	evl1subd	|- ( ph -> ( ( X .- ( A ` C ) ) e. B /\ ( ( O ` ( X .- ( A ` C ) ) ) ` V ) = ( V ( -g ` R ) C ) ) )
18	17	simprd	|- ( ph -> ( ( O ` ( X .- ( A ` C ) ) ) ` V ) = ( V ( -g ` R ) C ) )
19	13 18	syl5eq	|- ( ph -> ( ( O ` G ) ` V ) = ( V ( -g ` R ) C ) )