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 |