Metamath Proof Explorer


Theorem evls1var

Description: Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019)

Ref Expression
Hypotheses evls1var.q Q = S evalSub 1 R
evls1var.x X = var 1 U
evls1var.u U = S 𝑠 R
evls1var.b B = Base S
evls1var.s φ S CRing
evls1var.r φ R SubRing S
Assertion evls1var φ Q X = I B

Proof

Step Hyp Ref Expression
1 evls1var.q Q = S evalSub 1 R
2 evls1var.x X = var 1 U
3 evls1var.u U = S 𝑠 R
4 evls1var.b B = Base S
5 evls1var.s φ S CRing
6 evls1var.r φ R SubRing S
7 eqid var 1 S = var 1 S
8 7 6 3 subrgvr1 φ var 1 S = var 1 U
9 2 8 eqtr4id φ X = var 1 S
10 9 fveq2d φ Q X = Q var 1 S
11 eqid 1 𝑜 evalSub S R = 1 𝑜 evalSub S R
12 eqid 1 𝑜 eval S = 1 𝑜 eval S
13 eqid 1 𝑜 mVar U = 1 𝑜 mVar U
14 1on 1 𝑜 On
15 14 a1i φ 1 𝑜 On
16 0lt1o 1 𝑜
17 16 a1i φ 1 𝑜
18 11 12 13 3 4 15 5 6 17 evlsvarsrng φ 1 𝑜 evalSub S R 1 𝑜 mVar U = 1 𝑜 eval S 1 𝑜 mVar U
19 7 vr1val var 1 S = 1 𝑜 mVar S
20 eqid 1 𝑜 mVar S = 1 𝑜 mVar S
21 20 15 6 3 subrgmvr φ 1 𝑜 mVar S = 1 𝑜 mVar U
22 21 fveq1d φ 1 𝑜 mVar S = 1 𝑜 mVar U
23 19 22 syl5eq φ var 1 S = 1 𝑜 mVar U
24 23 fveq2d φ 1 𝑜 evalSub S R var 1 S = 1 𝑜 evalSub S R 1 𝑜 mVar U
25 23 fveq2d φ 1 𝑜 eval S var 1 S = 1 𝑜 eval S 1 𝑜 mVar U
26 18 24 25 3eqtr4d φ 1 𝑜 evalSub S R var 1 S = 1 𝑜 eval S var 1 S
27 26 coeq1d φ 1 𝑜 evalSub S R var 1 S y B 1 𝑜 × y = 1 𝑜 eval S var 1 S y B 1 𝑜 × y
28 eqid Poly 1 U = Poly 1 U
29 eqid Poly 1 S 𝑠 R = Poly 1 S 𝑠 R
30 eqid PwSer 1 S 𝑠 R = PwSer 1 S 𝑠 R
31 3 fveq2i Poly 1 U = Poly 1 S 𝑠 R
32 31 fveq2i Base Poly 1 U = Base Poly 1 S 𝑠 R
33 29 30 32 ply1bas Base Poly 1 U = Base 1 𝑜 mPoly S 𝑠 R
34 33 eqcomi Base 1 𝑜 mPoly S 𝑠 R = Base Poly 1 U
35 7 6 3 28 34 subrgvr1cl φ var 1 S Base 1 𝑜 mPoly S 𝑠 R
36 eqid 1 𝑜 evalSub S = 1 𝑜 evalSub S
37 eqid 1 𝑜 mPoly S 𝑠 R = 1 𝑜 mPoly S 𝑠 R
38 eqid Base 1 𝑜 mPoly S 𝑠 R = Base 1 𝑜 mPoly S 𝑠 R
39 1 36 4 37 38 evls1val S CRing R SubRing S var 1 S Base 1 𝑜 mPoly S 𝑠 R Q var 1 S = 1 𝑜 evalSub S R var 1 S y B 1 𝑜 × y
40 5 6 35 39 syl3anc φ Q var 1 S = 1 𝑜 evalSub S R var 1 S y B 1 𝑜 × y
41 crngring S CRing S Ring
42 eqid Poly 1 S = Poly 1 S
43 eqid PwSer 1 S = PwSer 1 S
44 eqid Base Poly 1 S = Base Poly 1 S
45 42 43 44 ply1bas Base Poly 1 S = Base 1 𝑜 mPoly S
46 45 eqcomi Base 1 𝑜 mPoly S = Base Poly 1 S
47 7 42 46 vr1cl S Ring var 1 S Base 1 𝑜 mPoly S
48 5 41 47 3syl φ var 1 S Base 1 𝑜 mPoly S
49 eqid eval 1 S = eval 1 S
50 eqid 1 𝑜 mPoly S = 1 𝑜 mPoly S
51 eqid Base 1 𝑜 mPoly S = Base 1 𝑜 mPoly S
52 49 12 4 50 51 evl1val S CRing var 1 S Base 1 𝑜 mPoly S eval 1 S var 1 S = 1 𝑜 eval S var 1 S y B 1 𝑜 × y
53 5 48 52 syl2anc φ eval 1 S var 1 S = 1 𝑜 eval S var 1 S y B 1 𝑜 × y
54 27 40 53 3eqtr4d φ Q var 1 S = eval 1 S var 1 S
55 49 7 4 evl1var S CRing eval 1 S var 1 S = I B
56 5 55 syl φ eval 1 S var 1 S = I B
57 10 54 56 3eqtrd φ Q X = I B