# Metamath Proof Explorer

## Theorem evls1scasrng

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, 13-Sep-2019)

Ref Expression
Hypotheses evls1scasrng.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1scasrng.o 𝑂 = ( eval1𝑆 )
evls1scasrng.w 𝑊 = ( Poly1𝑈 )
evls1scasrng.u 𝑈 = ( 𝑆s 𝑅 )
evls1scasrng.p 𝑃 = ( Poly1𝑆 )
evls1scasrng.b 𝐵 = ( Base ‘ 𝑆 )
evls1scasrng.a 𝐴 = ( algSc ‘ 𝑊 )
evls1scasrng.c 𝐶 = ( algSc ‘ 𝑃 )
evls1scasrng.s ( 𝜑𝑆 ∈ CRing )
evls1scasrng.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1scasrng.x ( 𝜑𝑋𝑅 )
Assertion evls1scasrng ( 𝜑 → ( 𝑄 ‘ ( 𝐴𝑋 ) ) = ( 𝑂 ‘ ( 𝐶𝑋 ) ) )

### Proof

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