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 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
19 17 18 ply1bas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( 1o mPoly R ) )
20 eqid 
 |-  ( Base ` ( R ^s ( B ^m 1o ) ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) )
21 19 20 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 ) ) ) )
22 ffn 
 |-  ( ( 1o eval R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s ( B ^m 1o ) ) ) -> ( 1o eval R ) Fn ( Base ` ( Poly1 ` R ) ) )
23 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 ) )
24 16 21 22 23 4syl 
 |-  ( F e. E -> ( F e. ran ( 1o eval R ) <-> E. x e. ( Base ` ( Poly1 ` R ) ) ( ( 1o eval R ) ` x ) = F ) )
25 11 24 mpbid 
 |-  ( F e. E -> E. x e. ( Base ` ( Poly1 ` R ) ) ( ( 1o eval R ) ` x ) = F )
26 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
27 26 4 2 13 19 evl1val 
 |-  ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) = ( ( ( 1o eval R ) ` x ) o. ( y e. B |-> ( 1o X. { y } ) ) ) )
28 eqid 
 |-  ( R ^s B ) = ( R ^s B )
29 26 17 28 2 evl1rhm 
 |-  ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
30 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
31 18 30 rhmf 
 |-  ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
32 ffn 
 |-  ( ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
33 29 31 32 3syl 
 |-  ( R e. CRing -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
34 fnfvelrn 
 |-  ( ( ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) e. ran ( eval1 ` R ) )
35 33 34 sylan 
 |-  ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) e. ran ( eval1 ` R ) )
36 35 1 eleqtrrdi 
 |-  ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` x ) e. Q )
37 27 36 eqeltrrd 
 |-  ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( 1o eval R ) ` x ) o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q )
38 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 } ) ) ) )
39 38 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 ) )
40 37 39 syl5ibcom 
 |-  ( ( R e. CRing /\ x e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( 1o eval R ) ` x ) = F -> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q ) )
41 40 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 ) )
42 9 25 41 sylc 
 |-  ( F e. E -> ( F o. ( y e. B |-> ( 1o X. { y } ) ) ) e. Q )