Metamath Proof Explorer

Theorem pf1mpf

Description: Convert a univariate polynomial function to multivariate. (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 pf1mpf 
|- ( F e. Q -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E )

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 1 pf1rcl 
 |-  ( F e. Q -> R e. CRing )
5 id 
 |-  ( F e. Q -> F e. Q )
6 5 1 eleqtrdi 
 |-  ( F e. Q -> F e. ran ( eval1 ` R ) )
7 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
8 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
9 eqid 
 |-  ( R ^s B ) = ( R ^s B )
10 7 8 9 2 evl1rhm 
 |-  ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
11 4 10 syl 
 |-  ( F e. Q -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
12 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
13 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
14 12 13 rhmf 
 |-  ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
15 ffn 
 |-  ( ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
16 fvelrnb 
 |-  ( ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) -> ( F e. ran ( eval1 ` R ) <-> E. y e. ( Base ` ( Poly1 ` R ) ) ( ( eval1 ` R ) ` y ) = F ) )
17 11 14 15 16 4syl 
 |-  ( F e. Q -> ( F e. ran ( eval1 ` R ) <-> E. y e. ( Base ` ( Poly1 ` R ) ) ( ( eval1 ` R ) ` y ) = F ) )
18 6 17 mpbid 
 |-  ( F e. Q -> E. y e. ( Base ` ( Poly1 ` R ) ) ( ( eval1 ` R ) ` y ) = F )
19 eqid 
 |-  ( 1o eval R ) = ( 1o eval R )
20 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
21 8 12 ply1bas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( 1o mPoly R ) )
22 7 19 2 20 21 evl1val 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` y ) = ( ( ( 1o eval R ) ` y ) o. ( z e. B |-> ( 1o X. { z } ) ) ) )
23 22 coeq1d 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( ( ( ( 1o eval R ) ` y ) o. ( z e. B |-> ( 1o X. { z } ) ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) )
24 coass 
 |-  ( ( ( ( 1o eval R ) ` y ) o. ( z e. B |-> ( 1o X. { z } ) ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( ( ( 1o eval R ) ` y ) o. ( ( z e. B |-> ( 1o X. { z } ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) )
25 df1o2 
 |-  1o = { (/) }
26 2 fvexi 
 |-  B e. _V
27 0ex 
 |-  (/) e. _V
28 eqid 
 |-  ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) = ( x e. ( B ^m 1o ) |-> ( x ` (/) ) )
29 25 26 27 28 mapsncnv 
 |-  `' ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) = ( z e. B |-> ( 1o X. { z } ) )
30 29 coeq1i 
 |-  ( `' ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( ( z e. B |-> ( 1o X. { z } ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) )
31 25 26 27 28 mapsnf1o2 
 |-  ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) : ( B ^m 1o ) -1-1-onto-> B
32 f1ococnv1 
 |-  ( ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) : ( B ^m 1o ) -1-1-onto-> B -> ( `' ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( _I |` ( B ^m 1o ) ) )
33 31 32 mp1i 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( `' ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( _I |` ( B ^m 1o ) ) )
34 30 33 eqtr3id 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( z e. B |-> ( 1o X. { z } ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( _I |` ( B ^m 1o ) ) )
35 34 coeq2d 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( 1o eval R ) ` y ) o. ( ( z e. B |-> ( 1o X. { z } ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) ) = ( ( ( 1o eval R ) ` y ) o. ( _I |` ( B ^m 1o ) ) ) )
36 24 35 eqtrid 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( ( 1o eval R ) ` y ) o. ( z e. B |-> ( 1o X. { z } ) ) ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( ( ( 1o eval R ) ` y ) o. ( _I |` ( B ^m 1o ) ) ) )
37 eqid 
 |-  ( R ^s ( B ^m 1o ) ) = ( R ^s ( B ^m 1o ) )
38 eqid 
 |-  ( Base ` ( R ^s ( B ^m 1o ) ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) )
39 simpl 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> R e. CRing )
40 ovexd 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( B ^m 1o ) e. _V )
41 1on 
 |-  1o e. On
42 19 2 20 37 evlrhm 
 |-  ( ( 1o e. On /\ R e. CRing ) -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
43 41 42 mpan 
 |-  ( R e. CRing -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
44 21 38 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 ) ) ) )
45 43 44 syl 
 |-  ( R e. CRing -> ( 1o eval R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s ( B ^m 1o ) ) ) )
46 45 ffvelcdmda 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. ( Base ` ( R ^s ( B ^m 1o ) ) ) )
47 37 2 38 39 40 46 pwselbas 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) : ( B ^m 1o ) --> B )
48 fcoi1 
 |-  ( ( ( 1o eval R ) ` y ) : ( B ^m 1o ) --> B -> ( ( ( 1o eval R ) ` y ) o. ( _I |` ( B ^m 1o ) ) ) = ( ( 1o eval R ) ` y ) )
49 47 48 syl 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( 1o eval R ) ` y ) o. ( _I |` ( B ^m 1o ) ) ) = ( ( 1o eval R ) ` y ) )
50 23 36 49 3eqtrd 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( ( 1o eval R ) ` y ) )
51 45 ffnd 
 |-  ( R e. CRing -> ( 1o eval R ) Fn ( Base ` ( Poly1 ` R ) ) )
52 fnfvelrn 
 |-  ( ( ( 1o eval R ) Fn ( Base ` ( Poly1 ` R ) ) /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. ran ( 1o eval R ) )
53 51 52 sylan 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. ran ( 1o eval R ) )
54 53 3 eleqtrrdi 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. E )
55 50 54 eqeltrd 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E )
56 coeq1 
 |-  ( ( ( eval1 ` R ) ` y ) = F -> ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) )
57 56 eleq1d 
 |-  ( ( ( eval1 ` R ) ` y ) = F -> ( ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E <-> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E ) )
58 55 57 syl5ibcom 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( eval1 ` R ) ` y ) = F -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E ) )
59 58 rexlimdva 
 |-  ( R e. CRing -> ( E. y e. ( Base ` ( Poly1 ` R ) ) ( ( eval1 ` R ) ` y ) = F -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E ) )
60 4 18 59 sylc 
 |-  ( F e. Q -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E )