This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝜑 → 𝑃 = ( Poly1 ‘ ( 𝑆 ↾s 𝐵 ) ) )
17 16 fveq2d ⊢ ( 𝜑 → ( algSc ‘ 𝑃 ) = ( algSc ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐵 ) ) ) )
18 8 17 eqtrid ⊢ ( 𝜑 → 𝐶 = ( 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 ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) )