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 = ( Poly1 ` ZZring )
	linevalexample.b	|- B = ( Base ` P )
	linevalexample.x	|- X = ( var1 ` ZZring )
	linevalexample.m	|- .- = ( -g ` P )
	linevalexample.a	|- A = ( algSc ` P )
	linevalexample.g	|- G = ( X .- ( A ` 3 ) )
	linevalexample.o	|- O = ( eval1 ` ZZring )
Assertion	linevalexample	|- ( ( O ` ( X .- ( A ` 3 ) ) ) ` 5 ) = 2

Proof

Step	Hyp	Ref	Expression
1		linevalexample.p	|- P = ( Poly1 ` ZZring )
2		linevalexample.b	|- B = ( Base ` P )
3		linevalexample.x	|- X = ( var1 ` ZZring )
4		linevalexample.m	|- .- = ( -g ` P )
5		linevalexample.a	|- A = ( algSc ` P )
6		linevalexample.g	|- G = ( X .- ( A ` 3 ) )
7		linevalexample.o	|- O = ( eval1 ` ZZring )
8		zringcrng	|- ZZring e. CRing
9		zringbas	|- ZZ = ( Base ` ZZring )
10		eqid	|- ( X .- ( A ` 3 ) ) = ( X .- ( A ` 3 ) )
11		3z	|- 3 e. ZZ
12	11	a1i	|- ( ZZring e. CRing -> 3 e. ZZ )
13		id	|- ( ZZring e. CRing -> ZZring e. CRing )
14		5nn0	|- 5 e. NN0
15	14	nn0zi	|- 5 e. ZZ
16	15	a1i	|- ( ZZring e. CRing -> 5 e. ZZ )
17	1 2 9 3 4 5 10 12 7 13 16	lineval	|- ( ZZring e. CRing -> ( ( O ` ( X .- ( A ` 3 ) ) ) ` 5 ) = ( 5 ( -g ` ZZring ) 3 ) )
18	8 17	ax-mp	|- ( ( O ` ( X .- ( A ` 3 ) ) ) ` 5 ) = ( 5 ( -g ` ZZring ) 3 )
19		eqid	|- ( -g ` ZZring ) = ( -g ` ZZring )
20	19	zringsubgval	|- ( ( 5 e. ZZ /\ 3 e. ZZ ) -> ( 5 - 3 ) = ( 5 ( -g ` ZZring ) 3 ) )
21	15 11 20	mp2an	|- ( 5 - 3 ) = ( 5 ( -g ` ZZring ) 3 )
22		5cn	|- 5 e. CC
23		3cn	|- 3 e. CC
24		2cn	|- 2 e. CC
25		3p2e5	|- ( 3 + 2 ) = 5
26	22 23 24 25	subaddrii	|- ( 5 - 3 ) = 2
27	18 21 26	3eqtr2i	|- ( ( O ` ( X .- ( A ` 3 ) ) ) ` 5 ) = 2