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 eval 1 R
pf1f.b B = Base R
mpfpf1.q E = ran 1 𝑜 eval R
Assertion pf1mpf F Q F x B 1 𝑜 x E

Proof

Step Hyp Ref Expression
1 pf1rcl.q Q = ran eval 1 R
2 pf1f.b B = Base R
3 mpfpf1.q E = ran 1 𝑜 eval R
4 1 pf1rcl F Q R CRing
5 id F Q F Q
6 5 1 eleqtrdi F Q F ran eval 1 R
7 eqid eval 1 R = eval 1 R
8 eqid Poly 1 R = Poly 1 R
9 eqid R 𝑠 B = R 𝑠 B
10 7 8 9 2 evl1rhm R CRing eval 1 R Poly 1 R RingHom R 𝑠 B
11 4 10 syl F Q eval 1 R Poly 1 R RingHom R 𝑠 B
12 eqid Base Poly 1 R = Base Poly 1 R
13 eqid Base R 𝑠 B = Base R 𝑠 B
14 12 13 rhmf eval 1 R Poly 1 R RingHom R 𝑠 B eval 1 R : Base Poly 1 R Base R 𝑠 B
15 ffn eval 1 R : Base Poly 1 R Base R 𝑠 B eval 1 R Fn Base Poly 1 R
16 fvelrnb eval 1 R Fn Base Poly 1 R F ran eval 1 R y Base Poly 1 R eval 1 R y = F
17 11 14 15 16 4syl F Q F ran eval 1 R y Base Poly 1 R eval 1 R y = F
18 6 17 mpbid F Q y Base Poly 1 R eval 1 R y = F
19 eqid 1 𝑜 eval R = 1 𝑜 eval R
20 eqid 1 𝑜 mPoly R = 1 𝑜 mPoly R
21 eqid PwSer 1 R = PwSer 1 R
22 8 21 12 ply1bas Base Poly 1 R = Base 1 𝑜 mPoly R
23 7 19 2 20 22 evl1val R CRing y Base Poly 1 R eval 1 R y = 1 𝑜 eval R y z B 1 𝑜 × z
24 23 coeq1d R CRing y Base Poly 1 R eval 1 R y x B 1 𝑜 x = 1 𝑜 eval R y z B 1 𝑜 × z x B 1 𝑜 x
25 coass 1 𝑜 eval R y z B 1 𝑜 × z x B 1 𝑜 x = 1 𝑜 eval R y z B 1 𝑜 × z x B 1 𝑜 x
26 df1o2 1 𝑜 =
27 2 fvexi B V
28 0ex V
29 eqid x B 1 𝑜 x = x B 1 𝑜 x
30 26 27 28 29 mapsncnv x B 1 𝑜 x -1 = z B 1 𝑜 × z
31 30 coeq1i x B 1 𝑜 x -1 x B 1 𝑜 x = z B 1 𝑜 × z x B 1 𝑜 x
32 26 27 28 29 mapsnf1o2 x B 1 𝑜 x : B 1 𝑜 1-1 onto B
33 f1ococnv1 x B 1 𝑜 x : B 1 𝑜 1-1 onto B x B 1 𝑜 x -1 x B 1 𝑜 x = I B 1 𝑜
34 32 33 mp1i R CRing y Base Poly 1 R x B 1 𝑜 x -1 x B 1 𝑜 x = I B 1 𝑜
35 31 34 eqtr3id R CRing y Base Poly 1 R z B 1 𝑜 × z x B 1 𝑜 x = I B 1 𝑜
36 35 coeq2d R CRing y Base Poly 1 R 1 𝑜 eval R y z B 1 𝑜 × z x B 1 𝑜 x = 1 𝑜 eval R y I B 1 𝑜
37 25 36 syl5eq R CRing y Base Poly 1 R 1 𝑜 eval R y z B 1 𝑜 × z x B 1 𝑜 x = 1 𝑜 eval R y I B 1 𝑜
38 eqid R 𝑠 B 1 𝑜 = R 𝑠 B 1 𝑜
39 eqid Base R 𝑠 B 1 𝑜 = Base R 𝑠 B 1 𝑜
40 simpl R CRing y Base Poly 1 R R CRing
41 ovexd R CRing y Base Poly 1 R B 1 𝑜 V
42 1on 1 𝑜 On
43 19 2 20 38 evlrhm 1 𝑜 On R CRing 1 𝑜 eval R 1 𝑜 mPoly R RingHom R 𝑠 B 1 𝑜
44 42 43 mpan R CRing 1 𝑜 eval R 1 𝑜 mPoly R RingHom R 𝑠 B 1 𝑜
45 22 39 rhmf 1 𝑜 eval R 1 𝑜 mPoly R RingHom R 𝑠 B 1 𝑜 1 𝑜 eval R : Base Poly 1 R Base R 𝑠 B 1 𝑜
46 44 45 syl R CRing 1 𝑜 eval R : Base Poly 1 R Base R 𝑠 B 1 𝑜
47 46 ffvelrnda R CRing y Base Poly 1 R 1 𝑜 eval R y Base R 𝑠 B 1 𝑜
48 38 2 39 40 41 47 pwselbas R CRing y Base Poly 1 R 1 𝑜 eval R y : B 1 𝑜 B
49 fcoi1 1 𝑜 eval R y : B 1 𝑜 B 1 𝑜 eval R y I B 1 𝑜 = 1 𝑜 eval R y
50 48 49 syl R CRing y Base Poly 1 R 1 𝑜 eval R y I B 1 𝑜 = 1 𝑜 eval R y
51 24 37 50 3eqtrd R CRing y Base Poly 1 R eval 1 R y x B 1 𝑜 x = 1 𝑜 eval R y
52 46 ffnd R CRing 1 𝑜 eval R Fn Base Poly 1 R
53 fnfvelrn 1 𝑜 eval R Fn Base Poly 1 R y Base Poly 1 R 1 𝑜 eval R y ran 1 𝑜 eval R
54 52 53 sylan R CRing y Base Poly 1 R 1 𝑜 eval R y ran 1 𝑜 eval R
55 54 3 eleqtrrdi R CRing y Base Poly 1 R 1 𝑜 eval R y E
56 51 55 eqeltrd R CRing y Base Poly 1 R eval 1 R y x B 1 𝑜 x E
57 coeq1 eval 1 R y = F eval 1 R y x B 1 𝑜 x = F x B 1 𝑜 x
58 57 eleq1d eval 1 R y = F eval 1 R y x B 1 𝑜 x E F x B 1 𝑜 x E
59 56 58 syl5ibcom R CRing y Base Poly 1 R eval 1 R y = F F x B 1 𝑜 x E
60 59 rexlimdva R CRing y Base Poly 1 R eval 1 R y = F F x B 1 𝑜 x E
61 4 18 60 sylc F Q F x B 1 𝑜 x E