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	$$⊢P={\mathrm{Poly}}_1\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	linevalexample.b	$$⊢B={\mathrm{Base}}_P$$
	linevalexample.x	$$⊢X={\mathrm{var}}_1\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	linevalexample.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	linevalexample.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	linevalexample.g	$$⊢G=X\underset{\dot{}}{-}A\left(3\right)$$
	linevalexample.o	$$⊢O={\mathrm{eval}}_1\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
Assertion	linevalexample	$$⊢O\left(X\underset{\dot{}}{-}A\left(3\right)\right)\left(5\right)=2$$

Proof

Step	Hyp	Ref	Expression
1		linevalexample.p	$$⊢P={\mathrm{Poly}}_1\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		linevalexample.b	$$⊢B={\mathrm{Base}}_P$$
3		linevalexample.x	$$⊢X={\mathrm{var}}_1\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
4		linevalexample.m	$$⊢\underset{\dot{}}{-}={-}_P$$
5		linevalexample.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
6		linevalexample.g	$$⊢G=X\underset{\dot{}}{-}A\left(3\right)$$
7		linevalexample.o	$$⊢O={\mathrm{eval}}_1\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
8		zringcrng	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
9		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
10		eqid	$$⊢X\underset{\dot{}}{-}A\left(3\right)=X\underset{\dot{}}{-}A\left(3\right)$$
11		3z	$$⊢3\in \mathbb{Z}$$
12	11	a1i	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}\to 3\in \mathbb{Z}$$
13		id	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
14		5nn0	$$⊢5\in {\mathbb{N}}_0$$
15	14	nn0zi	$$⊢5\in \mathbb{Z}$$
16	15	a1i	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}\to 5\in \mathbb{Z}$$
17	1 2 9 3 4 5 10 12 7 13 16	lineval	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}\to O\left(X\underset{\dot{}}{-}A\left(3\right)\right)\left(5\right)=5{-}_{{\mathbb{Z}}_{\mathrm{ring}}}3$$
18	8 17	ax-mp	$$⊢O\left(X\underset{\dot{}}{-}A\left(3\right)\right)\left(5\right)=5{-}_{{\mathbb{Z}}_{\mathrm{ring}}}3$$
19		eqid	$$⊢{-}_{{\mathbb{Z}}_{\mathrm{ring}}}={-}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
20	19	zringsubgval	$$⊢\left(5\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 5-3=5{-}_{{\mathbb{Z}}_{\mathrm{ring}}}3$$
21	15 11 20	mp2an	$$⊢5-3=5{-}_{{\mathbb{Z}}_{\mathrm{ring}}}3$$
22		5cn	$$⊢5\in ℂ$$
23		3cn	$$⊢3\in ℂ$$
24		2cn	$$⊢2\in ℂ$$
25		3p2e5	$$⊢3+2=5$$
26	22 23 24 25	subaddrii	$$⊢5-3=2$$
27	18 21 26	3eqtr2i	$$⊢O\left(X\underset{\dot{}}{-}A\left(3\right)\right)\left(5\right)=2$$