Metamath Proof Explorer

Theorem evlsscasrng

Description: The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 12-Sep-2019)

Ref Expression
Hypotheses evlsscasrng.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsscasrng.o ⊢ 𝑂 = ( 𝐼 eval 𝑆 )
evlsscasrng.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
evlsscasrng.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsscasrng.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
evlsscasrng.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evlsscasrng.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
evlsscasrng.c ⊢ 𝐶 = ( algSc ‘ 𝑃 )
evlsscasrng.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsscasrng.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsscasrng.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsscasrng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion evlsscasrng ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 evlsscasrng.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsscasrng.o ⊢ 𝑂 = ( 𝐼 eval 𝑆 )
3 evlsscasrng.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
4 evlsscasrng.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evlsscasrng.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
6 evlsscasrng.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
7 evlsscasrng.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
8 evlsscasrng.c ⊢ 𝐶 = ( algSc ‘ 𝑃 )
9 evlsscasrng.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10 evlsscasrng.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
11 evlsscasrng.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
12 evlsscasrng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
13 6 ressid ⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
14 13 eqcomd ⊢ ( 𝑆 ∈ CRing → 𝑆 = ( 𝑆 ↾s 𝐵 ) )
15 10 14 syl ⊢ ( 𝜑 → 𝑆 = ( 𝑆 ↾s 𝐵 ) )
16 15 oveq2d ⊢ ( 𝜑 → ( 𝐼 mPoly 𝑆 ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) )
17 5 16 syl5eq ⊢ ( 𝜑 → 𝑃 = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) )
18 17 fveq2d ⊢ ( 𝜑 → ( algSc ‘ 𝑃 ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) )
19 8 18 syl5eq ⊢ ( 𝜑 → 𝐶 = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) )
20 19 fveq1d ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) = ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) )
21 20 fveq2d ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝐶 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) )
22 eqid ⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
23 eqid ⊢ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) )
24 eqid ⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
25 eqid ⊢ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) )
26 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
27 6 subrgid ⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
28 10 26 27 3syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
29 6 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
30 11 29 syl ⊢ ( 𝜑 → 𝑅 ⊆ 𝐵 )
31 30 12 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
32 22 23 24 6 25 9 10 28 31 evlssca ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
33 21 32 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝐶 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
34 2 6 evlval ⊢ 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
35 34 a1i ⊢ ( 𝜑 → 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) )
36 35 fveq1d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝐶 ‘ 𝑋 ) ) )
37 1 3 4 6 7 9 10 11 12 evlssca ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
38 33 36 37 3eqtr4rd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) )