Metamath Proof Explorer

Theorem evls1val

Description: Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019)

Ref Expression
Hypotheses evls1fval.q 
|- Q = ( S evalSub1 R )
evls1fval.e 
|- E = ( 1o evalSub S )
evls1fval.b 
|- B = ( Base ` S )
evls1val.m 
|- M = ( 1o mPoly ( S |`s R ) )
evls1val.k 
|- K = ( Base ` M )
Assertion evls1val 
|- ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( Q ` A ) = ( ( ( E ` R ) ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )

Proof

Step Hyp Ref Expression
1 evls1fval.q 
 |-  Q = ( S evalSub1 R )
2 evls1fval.e 
 |-  E = ( 1o evalSub S )
3 evls1fval.b 
 |-  B = ( Base ` S )
4 evls1val.m 
 |-  M = ( 1o mPoly ( S |`s R ) )
5 evls1val.k 
 |-  K = ( Base ` M )
6 3 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
7 6 adantl 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> R C_ B )
8 elpwg 
 |-  ( R e. ( SubRing ` S ) -> ( R e. ~P B <-> R C_ B ) )
9 8 adantl 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( R e. ~P B <-> R C_ B ) )
10 7 9 mpbird 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> R e. ~P B )
11 1 2 3 evls1fval 
 |-  ( ( S e. CRing /\ R e. ~P B ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )
12 10 11 syldan 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) )
13 12 fveq1d 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Q ` A ) = ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) ` A ) )
14 13 3adant3 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( Q ` A ) = ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) ` A ) )
15 1on 
 |-  1o e. On
16 simp1 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> S e. CRing )
17 simp2 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> R e. ( SubRing ` S ) )
18 2 fveq1i 
 |-  ( E ` R ) = ( ( 1o evalSub S ) ` R )
19 eqid 
 |-  ( S |`s R ) = ( S |`s R )
20 eqid 
 |-  ( S ^s ( B ^m 1o ) ) = ( S ^s ( B ^m 1o ) )
21 18 4 19 20 3 evlsrhm 
 |-  ( ( 1o e. On /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( E ` R ) e. ( M RingHom ( S ^s ( B ^m 1o ) ) ) )
22 15 16 17 21 mp3an2i 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( E ` R ) e. ( M RingHom ( S ^s ( B ^m 1o ) ) ) )
23 eqid 
 |-  ( Base ` ( S ^s ( B ^m 1o ) ) ) = ( Base ` ( S ^s ( B ^m 1o ) ) )
24 5 23 rhmf 
 |-  ( ( E ` R ) e. ( M RingHom ( S ^s ( B ^m 1o ) ) ) -> ( E ` R ) : K --> ( Base ` ( S ^s ( B ^m 1o ) ) ) )
25 22 24 syl 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( E ` R ) : K --> ( Base ` ( S ^s ( B ^m 1o ) ) ) )
26 simp3 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> A e. K )
27 fvco3 
 |-  ( ( ( E ` R ) : K --> ( Base ` ( S ^s ( B ^m 1o ) ) ) /\ A e. K ) -> ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) ` A ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( E ` R ) ` A ) ) )
28 25 26 27 syl2anc 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. ( E ` R ) ) ` A ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( E ` R ) ` A ) ) )
29 25 26 ffvelrnd 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( ( E ` R ) ` A ) e. ( Base ` ( S ^s ( B ^m 1o ) ) ) )
30 ovex 
 |-  ( B ^m 1o ) e. _V
31 20 3 pwsbas 
 |-  ( ( S e. CRing /\ ( B ^m 1o ) e. _V ) -> ( B ^m ( B ^m 1o ) ) = ( Base ` ( S ^s ( B ^m 1o ) ) ) )
32 16 30 31 sylancl 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( B ^m ( B ^m 1o ) ) = ( Base ` ( S ^s ( B ^m 1o ) ) ) )
33 29 32 eleqtrrd 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( ( E ` R ) ` A ) e. ( B ^m ( B ^m 1o ) ) )
34 coeq1 
 |-  ( x = ( ( E ` R ) ` A ) -> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( ( ( E ` R ) ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
35 eqid 
 |-  ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) = ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) )
36 fvex 
 |-  ( ( E ` R ) ` A ) e. _V
37 3 fvexi 
 |-  B e. _V
38 37 mptex 
 |-  ( y e. B |-> ( 1o X. { y } ) ) e. _V
39 36 38 coex 
 |-  ( ( ( E ` R ) ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. _V
40 34 35 39 fvmpt 
 |-  ( ( ( E ` R ) ` A ) e. ( B ^m ( B ^m 1o ) ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( E ` R ) ` A ) ) = ( ( ( E ` R ) ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
41 33 40 syl 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( ( E ` R ) ` A ) ) = ( ( ( E ` R ) ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
42 14 28 41 3eqtrd 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) /\ A e. K ) -> ( Q ` A ) = ( ( ( E ` R ) ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )