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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	linply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	linply1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	linply1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	linply1.m	⊢ − = ( -g ‘ 𝑃 )
	linply1.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	linply1.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝐶 ) )
	linply1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	lineval.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	lineval.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	lineval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐾 )
Assertion	lineval	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑉 ) = ( 𝑉 ( -g ‘ 𝑅 ) 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		linply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		linply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		linply1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		linply1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		linply1.m	⊢ − = ( -g ‘ 𝑃 )
6		linply1.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
7		linply1.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝐶 ) )
8		linply1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
9		lineval.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
10		lineval.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
11		lineval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐾 )
12	7	fveq2i	⊢ ( 𝑂 ‘ 𝐺 ) = ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝐶 ) ) )
13	12	fveq1i	⊢ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑉 ) = ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝐶 ) ) ) ‘ 𝑉 )
14	9 4 3 1 2 10 11	evl1vard	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑉 ) = 𝑉 ) )
15	9 1 3 6 2 10 8 11	evl1scad	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐶 ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐴 ‘ 𝐶 ) ) ‘ 𝑉 ) = 𝐶 ) )
16		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
17	9 1 3 2 10 11 14 15 5 16	evl1subd	⊢ ( 𝜑 → ( ( 𝑋 − ( 𝐴 ‘ 𝐶 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝐶 ) ) ) ‘ 𝑉 ) = ( 𝑉 ( -g ‘ 𝑅 ) 𝐶 ) ) )
18	17	simprd	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝐶 ) ) ) ‘ 𝑉 ) = ( 𝑉 ( -g ‘ 𝑅 ) 𝐶 ) )
19	13 18	syl5eq	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑉 ) = ( 𝑉 ( -g ‘ 𝑅 ) 𝐶 ) )