Metamath Proof Explorer

Theorem evl1val

Description: Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1fval.o 
|- O = ( eval1 ` R )
evl1fval.q 
|- Q = ( 1o eval R )
evl1fval.b 
|- B = ( Base ` R )
evl1val.m 
|- M = ( 1o mPoly R )
evl1val.k 
|- K = ( Base ` M )
Assertion evl1val 
|- ( ( R e. CRing /\ A e. K ) -> ( O ` A ) = ( ( Q ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1fval.o 
 |-  O = ( eval1 ` R )
2 evl1fval.q 
 |-  Q = ( 1o eval R )
3 evl1fval.b 
 |-  B = ( Base ` R )
4 evl1val.m 
 |-  M = ( 1o mPoly R )
5 evl1val.k 
 |-  K = ( Base ` M )
6 1 2 3 evl1fval 
 |-  O = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q )
7 6 fveq1i 
 |-  ( O ` A ) = ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) ` A )
8 1on 
 |-  1o e. On
9 simpl 
 |-  ( ( R e. CRing /\ A e. K ) -> R e. CRing )
10 eqid 
 |-  ( R ^s ( B ^m 1o ) ) = ( R ^s ( B ^m 1o ) )
11 2 3 4 10 evlrhm 
 |-  ( ( 1o e. On /\ R e. CRing ) -> Q e. ( M RingHom ( R ^s ( B ^m 1o ) ) ) )
12 8 9 11 sylancr 
 |-  ( ( R e. CRing /\ A e. K ) -> Q e. ( M RingHom ( R ^s ( B ^m 1o ) ) ) )
13 eqid 
 |-  ( Base ` ( R ^s ( B ^m 1o ) ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) )
14 5 13 rhmf 
 |-  ( Q e. ( M RingHom ( R ^s ( B ^m 1o ) ) ) -> Q : K --> ( Base ` ( R ^s ( B ^m 1o ) ) ) )
15 12 14 syl 
 |-  ( ( R e. CRing /\ A e. K ) -> Q : K --> ( Base ` ( R ^s ( B ^m 1o ) ) ) )
16 fvco3 
 |-  ( ( Q : K --> ( Base ` ( R ^s ( B ^m 1o ) ) ) /\ A e. K ) -> ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) ` A ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( Q ` A ) ) )
17 15 16 sylancom 
 |-  ( ( R e. CRing /\ A e. K ) -> ( ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) o. Q ) ` A ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( Q ` A ) ) )
18 7 17 syl5eq 
 |-  ( ( R e. CRing /\ A e. K ) -> ( O ` A ) = ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( Q ` A ) ) )
19 ffvelrn 
 |-  ( ( Q : K --> ( Base ` ( R ^s ( B ^m 1o ) ) ) /\ A e. K ) -> ( Q ` A ) e. ( Base ` ( R ^s ( B ^m 1o ) ) ) )
20 15 19 sylancom 
 |-  ( ( R e. CRing /\ A e. K ) -> ( Q ` A ) e. ( Base ` ( R ^s ( B ^m 1o ) ) ) )
21 crngring 
 |-  ( R e. CRing -> R e. Ring )
22 21 adantr 
 |-  ( ( R e. CRing /\ A e. K ) -> R e. Ring )
23 ovex 
 |-  ( B ^m 1o ) e. _V
24 10 3 pwsbas 
 |-  ( ( R e. Ring /\ ( B ^m 1o ) e. _V ) -> ( B ^m ( B ^m 1o ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) ) )
25 22 23 24 sylancl 
 |-  ( ( R e. CRing /\ A e. K ) -> ( B ^m ( B ^m 1o ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) ) )
26 20 25 eleqtrrd 
 |-  ( ( R e. CRing /\ A e. K ) -> ( Q ` A ) e. ( B ^m ( B ^m 1o ) ) )
27 coeq1 
 |-  ( x = ( Q ` A ) -> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( ( Q ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
28 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 } ) ) ) )
29 fvex 
 |-  ( Q ` A ) e. _V
30 3 fvexi 
 |-  B e. _V
31 30 mptex 
 |-  ( y e. B |-> ( 1o X. { y } ) ) e. _V
32 29 31 coex 
 |-  ( ( Q ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. _V
33 27 28 32 fvmpt 
 |-  ( ( Q ` A ) e. ( B ^m ( B ^m 1o ) ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( Q ` A ) ) = ( ( Q ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
34 26 33 syl 
 |-  ( ( R e. CRing /\ A e. K ) -> ( ( x e. ( B ^m ( B ^m 1o ) ) |-> ( x o. ( y e. B |-> ( 1o X. { y } ) ) ) ) ` ( Q ` A ) ) = ( ( Q ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
35 18 34 eqtrd 
 |-  ( ( R e. CRing /\ A e. K ) -> ( O ` A ) = ( ( Q ` A ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )