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 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
22 8 21 12 ply1bas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( 1o mPoly R ) )
23 7 19 2 20 22 evl1val 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` y ) = ( ( ( 1o eval R ) ` y ) o. ( z e. B |-> ( 1o X. { z } ) ) ) )
24 23 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 ` (/) ) ) ) )
25 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 ` (/) ) ) ) )
26 df1o2 
 |-  1o = { (/) }
27 2 fvexi 
 |-  B e. _V
28 0ex 
 |-  (/) e. _V
29 eqid 
 |-  ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) = ( x e. ( B ^m 1o ) |-> ( x ` (/) ) )
30 26 27 28 29 mapsncnv 
 |-  `' ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) = ( z e. B |-> ( 1o X. { z } ) )
31 30 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 ` (/) ) ) )
32 26 27 28 29 mapsnf1o2 
 |-  ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) : ( B ^m 1o ) -1-1-onto-> B
33 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 ) ) )
34 32 33 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 ) ) )
35 31 34 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 ) ) )
36 35 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 ) ) ) )
37 25 36 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 ) ) ) )
38 eqid 
 |-  ( R ^s ( B ^m 1o ) ) = ( R ^s ( B ^m 1o ) )
39 eqid 
 |-  ( Base ` ( R ^s ( B ^m 1o ) ) ) = ( Base ` ( R ^s ( B ^m 1o ) ) )
40 simpl 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> R e. CRing )
41 ovexd 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( B ^m 1o ) e. _V )
42 1on 
 |-  1o e. On
43 19 2 20 38 evlrhm 
 |-  ( ( 1o e. On /\ R e. CRing ) -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
44 42 43 mpan 
 |-  ( R e. CRing -> ( 1o eval R ) e. ( ( 1o mPoly R ) RingHom ( R ^s ( B ^m 1o ) ) ) )
45 22 39 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 ) ) ) )
46 44 45 syl 
 |-  ( R e. CRing -> ( 1o eval R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s ( B ^m 1o ) ) ) )
47 46 ffvelrnda 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. ( Base ` ( R ^s ( B ^m 1o ) ) ) )
48 38 2 39 40 41 47 pwselbas 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) : ( B ^m 1o ) --> B )
49 fcoi1 
 |-  ( ( ( 1o eval R ) ` y ) : ( B ^m 1o ) --> B -> ( ( ( 1o eval R ) ` y ) o. ( _I |` ( B ^m 1o ) ) ) = ( ( 1o eval R ) ` y ) )
50 48 49 syl 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( 1o eval R ) ` y ) o. ( _I |` ( B ^m 1o ) ) ) = ( ( 1o eval R ) ` y ) )
51 24 37 50 3eqtrd 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( ( 1o eval R ) ` y ) )
52 46 ffnd 
 |-  ( R e. CRing -> ( 1o eval R ) Fn ( Base ` ( Poly1 ` R ) ) )
53 fnfvelrn 
 |-  ( ( ( 1o eval R ) Fn ( Base ` ( Poly1 ` R ) ) /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. ran ( 1o eval R ) )
54 52 53 sylan 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. ran ( 1o eval R ) )
55 54 3 eleqtrrdi 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( 1o eval R ) ` y ) e. E )
56 51 55 eqeltrd 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E )
57 coeq1 
 |-  ( ( ( eval1 ` R ) ` y ) = F -> ( ( ( eval1 ` R ) ` y ) o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) = ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) )
58 57 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 ) )
59 56 58 syl5ibcom 
 |-  ( ( R e. CRing /\ y e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( eval1 ` R ) ` y ) = F -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E ) )
60 59 rexlimdva 
 |-  ( R e. CRing -> ( E. y e. ( Base ` ( Poly1 ` R ) ) ( ( eval1 ` R ) ` y ) = F -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E ) )
61 4 18 60 sylc 
 |-  ( F e. Q -> ( F o. ( x e. ( B ^m 1o ) |-> ( x ` (/) ) ) ) e. E )