Metamath Proof Explorer


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