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

Metamath Proof Explorer

Theorem evlsvarsrng

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

Ref Expression
Hypotheses evlsvarsrng.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsvarsrng.o ⊢ 𝑂 = ( 𝐼 eval 𝑆 )
evlsvarsrng.v ⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
evlsvarsrng.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsvarsrng.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evlsvarsrng.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
evlsvarsrng.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsvarsrng.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsvarsrng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion evlsvarsrng ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 evlsvarsrng.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsvarsrng.o ⊢ 𝑂 = ( 𝐼 eval 𝑆 )
3 evlsvarsrng.v ⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
4 evlsvarsrng.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evlsvarsrng.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
6 evlsvarsrng.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
7 evlsvarsrng.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
8 evlsvarsrng.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9 evlsvarsrng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
10 1 3 4 5 6 7 8 9 evlsvar ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
11 2 5 evlval ⊢ 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
12 11 a1i ⊢ ( 𝜑 → 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) )
13 12 fveq1d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝑉 ‘ 𝑋 ) ) )
14 3 a1i ⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar 𝑈 ) )
15 eqid ⊢ ( 𝐼 mVar 𝑆 ) = ( 𝐼 mVar 𝑆 )
16 15 6 8 4 subrgmvr ⊢ ( 𝜑 → ( 𝐼 mVar 𝑆 ) = ( 𝐼 mVar 𝑈 ) )
17 5 ressid ⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
18 7 17 syl ⊢ ( 𝜑 → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
19 18 eqcomd ⊢ ( 𝜑 → 𝑆 = ( 𝑆 ↾s 𝐵 ) )
20 19 oveq2d ⊢ ( 𝜑 → ( 𝐼 mVar 𝑆 ) = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) )
21 14 16 20 3eqtr2d ⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) )
22 21 fveq1d ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) )
23 22 fveq2d ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝑉 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) )
24 eqid ⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
25 eqid ⊢ ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) )
26 eqid ⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
27 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
28 5 subrgid ⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
29 7 27 28 3syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
30 24 25 26 5 6 7 29 9 evlsvar ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
31 13 23 30 3eqtrrd ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) )
32 10 31 eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) )