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 )