Step |
Hyp |
Ref |
Expression |
1 |
|
pf1rcl.q |
|- Q = ran ( eval1 ` R ) |
2 |
|
pf1f.b |
|- B = ( Base ` R ) |
3 |
|
mpfpf1.q |
|- E = ran ( 1o eval R ) |
4 |
|
eqid |
|- ( 1o eval R ) = ( 1o eval R ) |
5 |
4 2
|
evlval |
|- ( 1o eval R ) = ( ( 1o evalSub R ) ` B ) |
6 |
5
|
rneqi |
|- ran ( 1o eval R ) = ran ( ( 1o evalSub R ) ` B ) |
7 |
3 6
|
eqtri |
|- E = ran ( ( 1o evalSub R ) ` B ) |
8 |
7
|
mpfrcl |
|- ( F e. E -> ( 1o e. _V /\ R e. CRing /\ B e. ( SubRing ` R ) ) ) |
9 |
8
|
simp2d |
|- ( F e. E -> R e. CRing ) |
10 |
|
id |
|- ( F e. E -> F e. E ) |
11 |
10 3
|
eleqtrdi |
|- ( F e. E -> F e. ran ( 1o eval R ) ) |
12 |
|
1on |
|- 1o e. On |
13 |
|
eqid |
|- ( 1o mPoly R ) = ( 1o mPoly R ) |
14 |
|
eqid |
|- ( R ^s ( B ^m 1o ) ) = ( R ^s ( B ^m 1o ) ) |
15 |
4 2 13 14
|
evlrhm |
|- ( ( 1o e. On /\ R e. CRing ) -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) ) |
16 |
12 9 15
|
sylancr |
|- ( F e. E -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) ) |
17 |
|
eqid |
|- ( Poly1 ` R ) = ( Poly1 ` R ) |
18 |
|
eqid |
|- ( PwSer1 ` R ) = ( PwSer1 ` R ) |
19 |
|
eqid |
|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) ) |
20 |
17 18 19
|
ply1bas |
|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( 1o mPoly R ) ) |
21 |
|
eqid |
|- ( Base ` ( R ^s ( B ^m 1o ) ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) ) |
22 |
20 21
|
rhmf |
|- ( ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) -> ( 1o eval R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s ( B ^m 1o ) ) ) ) |
23 |
|
ffn |
|- ( ( 1o eval R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s ( B ^m 1o ) ) ) -> ( 1o eval R ) Fn ( Base ` ( Poly1 ` R ) ) ) |
24 |
|
fvelrnb |
|- ( ( 1o eval R ) Fn ( Base ` ( Poly1 ` R ) ) -> ( F e. ran ( 1o eval R ) <-> E. x e. ( Base ` ( Poly1 ` R ) ) ( ( 1o eval R ) ` x ) = F ) ) |
25 |
16 22 23 24
|
4syl |
|- ( F e. E -> ( F e. ran ( 1o eval R ) <-> E. x e. ( Base ` ( Poly1 ` R ) ) ( ( 1o eval R ) ` x ) = F ) ) |
26 |
11 25
|
mpbid |
|- ( F e. E -> E. x e. ( Base ` ( Poly1 ` R ) ) ( ( 1o eval R ) ` x ) = F ) |
27 |
|
eqid |
|- ( eval1 ` R ) = ( eval1 ` R ) |
28 |
27 4 2 13 20
|
evl1val |
|- ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) = ( ( ( 1o eval R ) ` x ) o. ( y e. B |-> ( 1o X. { y } ) ) ) ) |
29 |
|
eqid |
|- ( R ^s B ) = ( R ^s B ) |
30 |
27 17 29 2
|
evl1rhm |
|- ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) ) |
31 |
|
eqid |
|- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) ) |
32 |
19 31
|
rhmf |
|- ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) ) |
33 |
|
ffn |
|- ( ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) ) |
34 |
30 32 33
|
3syl |
|- ( R e. CRing -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) ) |
35 |
|
fnfvelrn |
|- ( ( ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) e. ran ( eval1 ` R ) ) |
36 |
34 35
|
sylan |
|- ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) e. ran ( eval1 ` R ) ) |
37 |
36 1
|
eleqtrrdi |
|- ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) e. Q ) |
38 |
28 37
|
eqeltrrd |
|- ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( 1o eval R ) ` x ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q ) |
39 |
|
coeq1 |
|- ( ( ( 1o eval R ) ` x ) = F -> ( ( ( 1o eval R ) ` x ) o. ( y e. B |-> ( 1o X. { y } ) ) ) = ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) ) |
40 |
39
|
eleq1d |
|- ( ( ( 1o eval R ) ` x ) = F -> ( ( ( ( 1o eval R ) ` x ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q <-> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q ) ) |
41 |
38 40
|
syl5ibcom |
|- ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( 1o eval R ) ` x ) = F -> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q ) ) |
42 |
41
|
rexlimdva |
|- ( R e. CRing -> ( E. x e. ( Base ` ( Poly1 ` R ) ) ( ( 1o eval R ) ` x ) = F -> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q ) ) |
43 |
9 26 42
|
sylc |
|- ( F e. E -> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q ) |