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 |`s R )
evlsval.t 
|- T = ( S ^s ( B ^m I ) )
evlsval.b 
|- B = ( Base ` S )
evlsval.a 
|- A = ( algSc ` W )
evlsval.x 
|- X = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
evlsval.y 
|- Y = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) )
Assertion evlsval2 
|- ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Q e. ( W RingHom T ) /\ ( ( Q o. A ) = X /\ ( Q o. 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 |`s R )
5 evlsval.t 
 |-  T = ( S ^s ( B ^m I ) )
6 evlsval.b 
 |-  B = ( Base ` S )
7 evlsval.a 
 |-  A = ( algSc ` W )
8 evlsval.x 
 |-  X = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
9 evlsval.y 
 |-  Y = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) )
10 1 2 3 4 5 6 7 8 9 evlsval 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( iota_ m e. ( W RingHom T ) ( ( m o. A ) = X /\ ( m o. V ) = Y ) ) )
11 eqid 
 |-  ( Base ` T ) = ( Base ` T )
12 simp1 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> I e. Z )
13 4 subrgcrng 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing )
14 13 3adant1 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing )
15 simp2 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> S e. CRing )
16 ovex 
 |-  ( B ^m I ) e. _V
17 5 pwscrng 
 |-  ( ( S e. CRing /\ ( B ^m I ) e. _V ) -> T e. CRing )
18 15 16 17 sylancl 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> T e. CRing )
19 6 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
20 19 3ad2ant3 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> R C_ B )
21 20 resmptd 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( x e. B |-> ( ( B ^m I ) X. { x } ) ) |` R ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) ) )
22 21 8 eqtr4di 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( x e. B |-> ( ( B ^m I ) X. { x } ) ) |` R ) = X )
23 crngring 
 |-  ( S e. CRing -> S e. Ring )
24 23 3ad2ant2 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> S e. Ring )
25 eqid 
 |-  ( x e. B |-> ( ( B ^m I ) X. { x } ) ) = ( x e. B |-> ( ( B ^m I ) X. { x } ) )
26 5 6 25 pwsdiagrhm 
 |-  ( ( S e. Ring /\ ( B ^m I ) e. _V ) -> ( x e. B |-> ( ( B ^m I ) X. { x } ) ) e. ( S RingHom T ) )
27 24 16 26 sylancl 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( x e. B |-> ( ( B ^m I ) X. { x } ) ) e. ( S RingHom T ) )
28 simp3 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> R e. ( SubRing ` S ) )
29 4 resrhm 
 |-  ( ( ( x e. B |-> ( ( B ^m I ) X. { x } ) ) e. ( S RingHom T ) /\ R e. ( SubRing ` S ) ) -> ( ( x e. B |-> ( ( B ^m I ) X. { x } ) ) |` R ) e. ( U RingHom T ) )
30 27 28 29 syl2anc 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( ( x e. B |-> ( ( B ^m I ) X. { x } ) ) |` R ) e. ( U RingHom T ) )
31 22 30 eqeltrrd 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> X e. ( U RingHom T ) )
32 6 fvexi 
 |-  B e. _V
33 simpl1 
 |-  ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) -> I e. Z )
34 elmapg 
 |-  ( ( B e. _V /\ I e. Z ) -> ( g e. ( B ^m I ) <-> g : I --> B ) )
35 32 33 34 sylancr 
 |-  ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) -> ( g e. ( B ^m I ) <-> g : I --> B ) )
36 35 biimpa 
 |-  ( ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) /\ g e. ( B ^m I ) ) -> g : I --> B )
37 simplr 
 |-  ( ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) /\ g e. ( B ^m I ) ) -> x e. I )
38 36 37 ffvelrnd 
 |-  ( ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) /\ g e. ( B ^m I ) ) -> ( g ` x ) e. B )
39 38 fmpttd 
 |-  ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) -> ( g e. ( B ^m I ) |-> ( g ` x ) ) : ( B ^m I ) --> B )
40 simpl2 
 |-  ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) -> S e. CRing )
41 5 6 11 pwselbasb 
 |-  ( ( S e. CRing /\ ( B ^m I ) e. _V ) -> ( ( g e. ( B ^m I ) |-> ( g ` x ) ) e. ( Base ` T ) <-> ( g e. ( B ^m I ) |-> ( g ` x ) ) : ( B ^m I ) --> B ) )
42 40 16 41 sylancl 
 |-  ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) -> ( ( g e. ( B ^m I ) |-> ( g ` x ) ) e. ( Base ` T ) <-> ( g e. ( B ^m I ) |-> ( g ` x ) ) : ( B ^m I ) --> B ) )
43 39 42 mpbird 
 |-  ( ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) /\ x e. I ) -> ( g e. ( B ^m I ) |-> ( g ` x ) ) e. ( Base ` T ) )
44 43 9 fmptd 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Y : I --> ( Base ` T ) )
45 2 11 7 3 12 14 18 31 44 evlseu 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> E! m e. ( W RingHom T ) ( ( m o. A ) = X /\ ( m o. V ) = Y ) )
46 riotacl2 
 |-  ( E! m e. ( W RingHom T ) ( ( m o. A ) = X /\ ( m o. V ) = Y ) -> ( iota_ m e. ( W RingHom T ) ( ( m o. A ) = X /\ ( m o. V ) = Y ) ) e. { m e. ( W RingHom T ) | ( ( m o. A ) = X /\ ( m o. V ) = Y ) } )
47 45 46 syl 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( iota_ m e. ( W RingHom T ) ( ( m o. A ) = X /\ ( m o. V ) = Y ) ) e. { m e. ( W RingHom T ) | ( ( m o. A ) = X /\ ( m o. V ) = Y ) } )
48 10 47 eqeltrd 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. { m e. ( W RingHom T ) | ( ( m o. A ) = X /\ ( m o. V ) = Y ) } )
49 coeq1 
 |-  ( m = Q -> ( m o. A ) = ( Q o. A ) )
50 49 eqeq1d 
 |-  ( m = Q -> ( ( m o. A ) = X <-> ( Q o. A ) = X ) )
51 coeq1 
 |-  ( m = Q -> ( m o. V ) = ( Q o. V ) )
52 51 eqeq1d 
 |-  ( m = Q -> ( ( m o. V ) = Y <-> ( Q o. V ) = Y ) )
53 50 52 anbi12d 
 |-  ( m = Q -> ( ( ( m o. A ) = X /\ ( m o. V ) = Y ) <-> ( ( Q o. A ) = X /\ ( Q o. V ) = Y ) ) )
54 53 elrab 
 |-  ( Q e. { m e. ( W RingHom T ) | ( ( m o. A ) = X /\ ( m o. V ) = Y ) } <-> ( Q e. ( W RingHom T ) /\ ( ( Q o. A ) = X /\ ( Q o. V ) = Y ) ) )
55 48 54 sylib 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Q e. ( W RingHom T ) /\ ( ( Q o. A ) = X /\ ( Q o. V ) = Y ) ) )