Step |
Hyp |
Ref |
Expression |
1 |
|
evlsca.q |
⊢ 𝑄 = ( 𝐼 eval 𝑆 ) |
2 |
|
evlsca.w |
⊢ 𝑊 = ( 𝐼 mPoly 𝑆 ) |
3 |
|
evlsca.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
4 |
|
evlsca.a |
⊢ 𝐴 = ( algSc ‘ 𝑊 ) |
5 |
|
evlsca.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
6 |
|
evlsca.s |
⊢ ( 𝜑 → 𝑆 ∈ CRing ) |
7 |
|
evlsca.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
8 |
|
eqid |
⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) |
9 |
|
eqid |
⊢ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) |
10 |
|
eqid |
⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 ) |
11 |
|
eqid |
⊢ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) |
12 |
|
crngring |
⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring ) |
13 |
3
|
subrgid |
⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) |
14 |
6 12 13
|
3syl |
⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) |
15 |
8 1 9 10 2 3 11 4 5 6 14 7
|
evlsscasrng |
⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ) |
16 |
8 9 10 3 11 5 6 14 7
|
evlssca |
⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ) |
17 |
15 16
|
eqtr3d |
⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ) |