Metamath Proof Explorer


Theorem mpfpf1

Description: Convert a multivariate polynomial function to univariate. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pf1rcl.q
|- Q = ran ( eval1 ` R )
pf1f.b
|- B = ( Base ` R )
mpfpf1.q
|- E = ran ( 1o eval R )
Assertion mpfpf1
|- ( F e. E -> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q )

Proof

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 )