Theorem linevalexample

Description: The polynomial x - 3 over ZZ evaluated for x = 5 results in 2. (Contributed by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	linevalexample.p	⊢ 𝑃 = ( Poly1 ‘ ℤring )
	linevalexample.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	linevalexample.x	⊢ 𝑋 = ( var1 ‘ ℤring )
	linevalexample.m	⊢ − = ( -g ‘ 𝑃 )
	linevalexample.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	linevalexample.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 3 ) )
	linevalexample.o	⊢ 𝑂 = ( eval1 ‘ ℤring )
Assertion	linevalexample	⊢ ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 3 ) ) ) ‘ 5 ) = 2

Proof

Step	Hyp	Ref	Expression
1		linevalexample.p	⊢ 𝑃 = ( Poly1 ‘ ℤring )
2		linevalexample.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		linevalexample.x	⊢ 𝑋 = ( var1 ‘ ℤring )
4		linevalexample.m	⊢ − = ( -g ‘ 𝑃 )
5		linevalexample.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
6		linevalexample.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 3 ) )
7		linevalexample.o	⊢ 𝑂 = ( eval1 ‘ ℤring )
8		zringcrng	⊢ ℤring ∈ CRing
9		zringbas	⊢ ℤ = ( Base ‘ ℤring )
10		eqid	⊢ ( 𝑋 − ( 𝐴 ‘ 3 ) ) = ( 𝑋 − ( 𝐴 ‘ 3 ) )
11		3z	⊢ 3 ∈ ℤ
12	11	a1i	⊢ ( ℤring ∈ CRing → 3 ∈ ℤ )
13		id	⊢ ( ℤring ∈ CRing → ℤring ∈ CRing )
14		5nn0	⊢ 5 ∈ ℕ0
15	14	nn0zi	⊢ 5 ∈ ℤ
16	15	a1i	⊢ ( ℤring ∈ CRing → 5 ∈ ℤ )
17	1 2 9 3 4 5 10 12 7 13 16	lineval	⊢ ( ℤring ∈ CRing → ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 3 ) ) ) ‘ 5 ) = ( 5 ( -g ‘ ℤring ) 3 ) )
18	8 17	ax-mp	⊢ ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 3 ) ) ) ‘ 5 ) = ( 5 ( -g ‘ ℤring ) 3 )
19		eqid	⊢ ( -g ‘ ℤring ) = ( -g ‘ ℤring )
20	19	zringsubgval	⊢ ( ( 5 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 5 − 3 ) = ( 5 ( -g ‘ ℤring ) 3 ) )
21	15 11 20	mp2an	⊢ ( 5 − 3 ) = ( 5 ( -g ‘ ℤring ) 3 )
22		5cn	⊢ 5 ∈ ℂ
23		3cn	⊢ 3 ∈ ℂ
24		2cn	⊢ 2 ∈ ℂ
25		3p2e5	⊢ ( 3 + 2 ) = 5
26	22 23 24 25	subaddrii	⊢ ( 5 − 3 ) = 2
27	18 21 26	3eqtr2i	⊢ ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 3 ) ) ) ‘ 5 ) = 2