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 𝑄 = ran ( eval1𝑅 )
pf1f.b 𝐵 = ( Base ‘ 𝑅 )
mpfpf1.q 𝐸 = ran ( 1o eval 𝑅 )
Assertion pf1mpf ( 𝐹𝑄 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 pf1rcl.q 𝑄 = ran ( eval1𝑅 )
2 pf1f.b 𝐵 = ( Base ‘ 𝑅 )
3 mpfpf1.q 𝐸 = ran ( 1o eval 𝑅 )
4 1 pf1rcl ( 𝐹𝑄𝑅 ∈ CRing )
5 id ( 𝐹𝑄𝐹𝑄 )
6 5 1 eleqtrdi ( 𝐹𝑄𝐹 ∈ ran ( eval1𝑅 ) )
7 eqid ( eval1𝑅 ) = ( eval1𝑅 )
8 eqid ( Poly1𝑅 ) = ( Poly1𝑅 )
9 eqid ( 𝑅s 𝐵 ) = ( 𝑅s 𝐵 )
10 7 8 9 2 evl1rhm ( 𝑅 ∈ CRing → ( eval1𝑅 ) ∈ ( ( Poly1𝑅 ) RingHom ( 𝑅s 𝐵 ) ) )
11 4 10 syl ( 𝐹𝑄 → ( eval1𝑅 ) ∈ ( ( Poly1𝑅 ) RingHom ( 𝑅s 𝐵 ) ) )
12 eqid ( Base ‘ ( Poly1𝑅 ) ) = ( Base ‘ ( Poly1𝑅 ) )
13 eqid ( Base ‘ ( 𝑅s 𝐵 ) ) = ( Base ‘ ( 𝑅s 𝐵 ) )
14 12 13 rhmf ( ( eval1𝑅 ) ∈ ( ( Poly1𝑅 ) RingHom ( 𝑅s 𝐵 ) ) → ( eval1𝑅 ) : ( Base ‘ ( Poly1𝑅 ) ) ⟶ ( Base ‘ ( 𝑅s 𝐵 ) ) )
15 ffn ( ( eval1𝑅 ) : ( Base ‘ ( Poly1𝑅 ) ) ⟶ ( Base ‘ ( 𝑅s 𝐵 ) ) → ( eval1𝑅 ) Fn ( Base ‘ ( Poly1𝑅 ) ) )
16 fvelrnb ( ( eval1𝑅 ) Fn ( Base ‘ ( Poly1𝑅 ) ) → ( 𝐹 ∈ ran ( eval1𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ( ( eval1𝑅 ) ‘ 𝑦 ) = 𝐹 ) )
17 11 14 15 16 4syl ( 𝐹𝑄 → ( 𝐹 ∈ ran ( eval1𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ( ( eval1𝑅 ) ‘ 𝑦 ) = 𝐹 ) )
18 6 17 mpbid ( 𝐹𝑄 → ∃ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ( ( eval1𝑅 ) ‘ 𝑦 ) = 𝐹 )
19 eqid ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
20 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
21 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
22 8 21 12 ply1bas ( Base ‘ ( Poly1𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
23 7 19 2 20 22 evl1val ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( eval1𝑅 ) ‘ 𝑦 ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ) )
24 23 coeq1d ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( ( eval1𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
25 coass ( ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
26 df1o2 1o = { ∅ }
27 2 fvexi 𝐵 ∈ V
28 0ex ∅ ∈ V
29 eqid ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) )
30 26 27 28 29 mapsncnv ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) )
31 30 coeq1i ( ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) )
32 26 27 28 29 mapsnf1o2 ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( 𝐵m 1o ) –1-1-onto𝐵
33 f1ococnv1 ( ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( 𝐵m 1o ) –1-1-onto𝐵 → ( ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( I ↾ ( 𝐵m 1o ) ) )
34 32 33 mp1i ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( I ↾ ( 𝐵m 1o ) ) )
35 31 34 syl5eqr ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( I ↾ ( 𝐵m 1o ) ) )
36 35 coeq2d ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵m 1o ) ) ) )
37 25 36 syl5eq ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧𝐵 ↦ ( 1o × { 𝑧 } ) ) ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵m 1o ) ) ) )
38 eqid ( 𝑅s ( 𝐵m 1o ) ) = ( 𝑅s ( 𝐵m 1o ) )
39 eqid ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) = ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) )
40 simpl ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → 𝑅 ∈ CRing )
41 ovexd ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( 𝐵m 1o ) ∈ V )
42 1on 1o ∈ On
43 19 2 20 38 evlrhm ( ( 1o ∈ On ∧ 𝑅 ∈ CRing ) → ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
44 42 43 mpan ( 𝑅 ∈ CRing → ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
45 22 39 rhmf ( ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅s ( 𝐵m 1o ) ) ) → ( 1o eval 𝑅 ) : ( Base ‘ ( Poly1𝑅 ) ) ⟶ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
46 44 45 syl ( 𝑅 ∈ CRing → ( 1o eval 𝑅 ) : ( Base ‘ ( Poly1𝑅 ) ) ⟶ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
47 46 ffvelrnda ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
48 38 2 39 40 41 47 pwselbas ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( 1o eval 𝑅 ) ‘ 𝑦 ) : ( 𝐵m 1o ) ⟶ 𝐵 )
49 fcoi1 ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) : ( 𝐵m 1o ) ⟶ 𝐵 → ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵m 1o ) ) ) = ( ( 1o eval 𝑅 ) ‘ 𝑦 ) )
50 48 49 syl ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵m 1o ) ) ) = ( ( 1o eval 𝑅 ) ‘ 𝑦 ) )
51 24 37 50 3eqtrd ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( ( eval1𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( 1o eval 𝑅 ) ‘ 𝑦 ) )
52 46 ffnd ( 𝑅 ∈ CRing → ( 1o eval 𝑅 ) Fn ( Base ‘ ( Poly1𝑅 ) ) )
53 fnfvelrn ( ( ( 1o eval 𝑅 ) Fn ( Base ‘ ( Poly1𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∈ ran ( 1o eval 𝑅 ) )
54 52 53 sylan ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∈ ran ( 1o eval 𝑅 ) )
55 54 3 eleqtrrdi ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( 1o eval 𝑅 ) ‘ 𝑦 ) ∈ 𝐸 )
56 51 55 eqeltrd ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( ( eval1𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 )
57 coeq1 ( ( ( eval1𝑅 ) ‘ 𝑦 ) = 𝐹 → ( ( ( eval1𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
58 57 eleq1d ( ( ( eval1𝑅 ) ‘ 𝑦 ) = 𝐹 → ( ( ( ( eval1𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ↔ ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ) )
59 56 58 syl5ibcom ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ) → ( ( ( eval1𝑅 ) ‘ 𝑦 ) = 𝐹 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ) )
60 59 rexlimdva ( 𝑅 ∈ CRing → ( ∃ 𝑦 ∈ ( Base ‘ ( Poly1𝑅 ) ) ( ( eval1𝑅 ) ‘ 𝑦 ) = 𝐹 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ) )
61 4 18 60 sylc ( 𝐹𝑄 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵m 1o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 )