Metamath Proof Explorer


Theorem evlsval2

Description: Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses evlsval.q Q = I evalSub S R
evlsval.w W = I mPoly U
evlsval.v V = I mVar U
evlsval.u U = S 𝑠 R
evlsval.t T = S 𝑠 B I
evlsval.b B = Base S
evlsval.a A = algSc W
evlsval.x X = x R B I × x
evlsval.y Y = x I g B I g x
Assertion evlsval2 I Z S CRing R SubRing S Q W RingHom T Q A = X Q V = Y

Proof

Step Hyp Ref Expression
1 evlsval.q Q = I evalSub S R
2 evlsval.w W = I mPoly U
3 evlsval.v V = I mVar U
4 evlsval.u U = S 𝑠 R
5 evlsval.t T = S 𝑠 B I
6 evlsval.b B = Base S
7 evlsval.a A = algSc W
8 evlsval.x X = x R B I × x
9 evlsval.y Y = x I g B I g x
10 1 2 3 4 5 6 7 8 9 evlsval I Z S CRing R SubRing S Q = ι m W RingHom T | m A = X m V = Y
11 eqid Base T = Base T
12 elex I Z I V
13 12 3ad2ant1 I Z S CRing R SubRing S I V
14 4 subrgcrng S CRing R SubRing S U CRing
15 14 3adant1 I Z S CRing R SubRing S U CRing
16 simp2 I Z S CRing R SubRing S S CRing
17 ovex B I V
18 5 pwscrng S CRing B I V T CRing
19 16 17 18 sylancl I Z S CRing R SubRing S T CRing
20 6 subrgss R SubRing S R B
21 20 3ad2ant3 I Z S CRing R SubRing S R B
22 21 resmptd I Z S CRing R SubRing S x B B I × x R = x R B I × x
23 22 8 syl6eqr I Z S CRing R SubRing S x B B I × x R = X
24 crngring S CRing S Ring
25 24 3ad2ant2 I Z S CRing R SubRing S S Ring
26 eqid x B B I × x = x B B I × x
27 5 6 26 pwsdiagrhm S Ring B I V x B B I × x S RingHom T
28 25 17 27 sylancl I Z S CRing R SubRing S x B B I × x S RingHom T
29 simp3 I Z S CRing R SubRing S R SubRing S
30 4 resrhm x B B I × x S RingHom T R SubRing S x B B I × x R U RingHom T
31 28 29 30 syl2anc I Z S CRing R SubRing S x B B I × x R U RingHom T
32 23 31 eqeltrrd I Z S CRing R SubRing S X U RingHom T
33 6 fvexi B V
34 simpl1 I Z S CRing R SubRing S x I I Z
35 elmapg B V I Z g B I g : I B
36 33 34 35 sylancr I Z S CRing R SubRing S x I g B I g : I B
37 36 biimpa I Z S CRing R SubRing S x I g B I g : I B
38 simplr I Z S CRing R SubRing S x I g B I x I
39 37 38 ffvelrnd I Z S CRing R SubRing S x I g B I g x B
40 39 fmpttd I Z S CRing R SubRing S x I g B I g x : B I B
41 simpl2 I Z S CRing R SubRing S x I S CRing
42 5 6 11 pwselbasb S CRing B I V g B I g x Base T g B I g x : B I B
43 41 17 42 sylancl I Z S CRing R SubRing S x I g B I g x Base T g B I g x : B I B
44 40 43 mpbird I Z S CRing R SubRing S x I g B I g x Base T
45 44 9 fmptd I Z S CRing R SubRing S Y : I Base T
46 2 11 7 3 13 15 19 32 45 evlseu I Z S CRing R SubRing S ∃! m W RingHom T m A = X m V = Y
47 riotacl2 ∃! m W RingHom T m A = X m V = Y ι m W RingHom T | m A = X m V = Y m W RingHom T | m A = X m V = Y
48 46 47 syl I Z S CRing R SubRing S ι m W RingHom T | m A = X m V = Y m W RingHom T | m A = X m V = Y
49 10 48 eqeltrd I Z S CRing R SubRing S Q m W RingHom T | m A = X m V = Y
50 coeq1 m = Q m A = Q A
51 50 eqeq1d m = Q m A = X Q A = X
52 coeq1 m = Q m V = Q V
53 52 eqeq1d m = Q m V = Y Q V = Y
54 51 53 anbi12d m = Q m A = X m V = Y Q A = X Q V = Y
55 54 elrab Q m W RingHom T | m A = X m V = Y Q W RingHom T Q A = X Q V = Y
56 49 55 sylib I Z S CRing R SubRing S Q W RingHom T Q A = X Q V = Y