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

Metamath Proof Explorer

Theorem evls1varsrng

Description: The evaluation of the variable of univariate 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 evls1varsrng.q ⊢ Q = S evalSub 1 R
evls1varsrng.o ⊢ O = eval 1 ⁡ S
evls1varsrng.v ⊢ V = var 1 ⁡ U
evls1varsrng.u ⊢ U = S ↾ 𝑠 R
evls1varsrng.b ⊢ B = Base S
evls1varsrng.s ⊢ φ → S ∈ CRing
evls1varsrng.r ⊢ φ → R ∈ SubRing ⁡ S
Assertion evls1varsrng ⊢ φ → Q ⁡ V = O ⁡ V

Proof

Step Hyp Ref Expression
1 evls1varsrng.q ⊢ Q = S evalSub 1 R
2 evls1varsrng.o ⊢ O = eval 1 ⁡ S
3 evls1varsrng.v ⊢ V = var 1 ⁡ U
4 evls1varsrng.u ⊢ U = S ↾ 𝑠 R
5 evls1varsrng.b ⊢ B = Base S
6 evls1varsrng.s ⊢ φ → S ∈ CRing
7 evls1varsrng.r ⊢ φ → R ∈ SubRing ⁡ S
8 1 3 4 5 6 7 evls1var ⊢ φ → Q ⁡ V = I ↾ B
9 2 5 evl1fval1 ⊢ O = S evalSub 1 B
10 9 a1i ⊢ φ → O = S evalSub 1 B
11 10 fveq1d ⊢ φ → O ⁡ V = S evalSub 1 B ⁡ V
12 3 a1i ⊢ φ → V = var 1 ⁡ U
13 eqid ⊢ var 1 ⁡ S = var 1 ⁡ S
14 13 7 4 subrgvr1 ⊢ φ → var 1 ⁡ S = var 1 ⁡ U
15 5 ressid ⊢ S ∈ CRing → S ↾ 𝑠 B = S
16 6 15 syl ⊢ φ → S ↾ 𝑠 B = S
17 16 eqcomd ⊢ φ → S = S ↾ 𝑠 B
18 17 fveq2d ⊢ φ → var 1 ⁡ S = var 1 ⁡ S ↾ 𝑠 B
19 12 14 18 3eqtr2d ⊢ φ → V = var 1 ⁡ S ↾ 𝑠 B
20 19 fveq2d ⊢ φ → S evalSub 1 B ⁡ V = S evalSub 1 B ⁡ var 1 ⁡ S ↾ 𝑠 B
21 eqid ⊢ S evalSub 1 B = S evalSub 1 B
22 eqid ⊢ var 1 ⁡ S ↾ 𝑠 B = var 1 ⁡ S ↾ 𝑠 B
23 eqid ⊢ S ↾ 𝑠 B = S ↾ 𝑠 B
24 crngring ⊢ S ∈ CRing → S ∈ Ring
25 5 subrgid ⊢ S ∈ Ring → B ∈ SubRing ⁡ S
26 6 24 25 3syl ⊢ φ → B ∈ SubRing ⁡ S
27 21 22 23 5 6 26 evls1var ⊢ φ → S evalSub 1 B ⁡ var 1 ⁡ S ↾ 𝑠 B = I ↾ B
28 11 20 27 3eqtrrd ⊢ φ → I ↾ B = O ⁡ V
29 8 28 eqtrd ⊢ φ → Q ⁡ V = O ⁡ V