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 ⊢ Q = I evalSub S ⁡ R
evlsvarsrng.o ⊢ O = I eval S
evlsvarsrng.v ⊢ V = I mVar U
evlsvarsrng.u ⊢ U = S ↾ 𝑠 R
evlsvarsrng.b ⊢ B = Base S
evlsvarsrng.i ⊢ φ → I ∈ A
evlsvarsrng.s ⊢ φ → S ∈ CRing
evlsvarsrng.r ⊢ φ → R ∈ SubRing ⁡ S
evlsvarsrng.x ⊢ φ → X ∈ I
Assertion evlsvarsrng ⊢ φ → Q ⁡ V ⁡ X = O ⁡ V ⁡ X

Proof

Step Hyp Ref Expression
1 evlsvarsrng.q ⊢ Q = I evalSub S ⁡ R
2 evlsvarsrng.o ⊢ O = I eval S
3 evlsvarsrng.v ⊢ V = I mVar U
4 evlsvarsrng.u ⊢ U = S ↾ 𝑠 R
5 evlsvarsrng.b ⊢ B = Base S
6 evlsvarsrng.i ⊢ φ → I ∈ A
7 evlsvarsrng.s ⊢ φ → S ∈ CRing
8 evlsvarsrng.r ⊢ φ → R ∈ SubRing ⁡ S
9 evlsvarsrng.x ⊢ φ → X ∈ I
10 1 3 4 5 6 7 8 9 evlsvar ⊢ φ → Q ⁡ V ⁡ X = g ∈ B I ⟼ g ⁡ X
11 2 5 evlval ⊢ O = I evalSub S ⁡ B
12 11 a1i ⊢ φ → O = I evalSub S ⁡ B
13 12 fveq1d ⊢ φ → O ⁡ V ⁡ X = I evalSub S ⁡ B ⁡ V ⁡ X
14 3 a1i ⊢ φ → V = I mVar U
15 eqid ⊢ I mVar S = I mVar S
16 15 6 8 4 subrgmvr ⊢ φ → I mVar S = I mVar U
17 5 ressid ⊢ S ∈ CRing → S ↾ 𝑠 B = S
18 7 17 syl ⊢ φ → S ↾ 𝑠 B = S
19 18 eqcomd ⊢ φ → S = S ↾ 𝑠 B
20 19 oveq2d ⊢ φ → I mVar S = I mVar S ↾ 𝑠 B
21 14 16 20 3eqtr2d ⊢ φ → V = I mVar S ↾ 𝑠 B
22 21 fveq1d ⊢ φ → V ⁡ X = I mVar S ↾ 𝑠 B ⁡ X
23 22 fveq2d ⊢ φ → I evalSub S ⁡ B ⁡ V ⁡ X = I evalSub S ⁡ B ⁡ I mVar S ↾ 𝑠 B ⁡ X
24 eqid ⊢ I evalSub S ⁡ B = I evalSub S ⁡ B
25 eqid ⊢ I mVar S ↾ 𝑠 B = I mVar S ↾ 𝑠 B
26 eqid ⊢ S ↾ 𝑠 B = S ↾ 𝑠 B
27 crngring ⊢ S ∈ CRing → S ∈ Ring
28 5 subrgid ⊢ S ∈ Ring → B ∈ SubRing ⁡ S
29 7 27 28 3syl ⊢ φ → B ∈ SubRing ⁡ S
30 24 25 26 5 6 7 29 9 evlsvar ⊢ φ → I evalSub S ⁡ B ⁡ I mVar S ↾ 𝑠 B ⁡ X = g ∈ B I ⟼ g ⁡ X
31 13 23 30 3eqtrrd ⊢ φ → g ∈ B I ⟼ g ⁡ X = O ⁡ V ⁡ X
32 10 31 eqtrd ⊢ φ → Q ⁡ V ⁡ X = O ⁡ V ⁡ X