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 ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
pf1f.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mpfpf1.q ⊢ 𝐸 = ran ( 1o eval 𝑅 )
Assertion mpfpf1 ( 𝐹 ∈ 𝐸 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 )

Proof

Step Hyp Ref Expression
1 pf1rcl.q ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
2 pf1f.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mpfpf1.q ⊢ 𝐸 = ran ( 1o eval 𝑅 )
4 eqid ⊢ ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
5 4 2 evlval ⊢ ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
6 5 rneqi ⊢ ran ( 1o eval 𝑅 ) = ran ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
7 3 6 eqtri ⊢ 𝐸 = ran ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
8 7 mpfrcl ⊢ ( 𝐹 ∈ 𝐸 → ( 1o ∈ V ∧ 𝑅 ∈ CRing ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) )
9 8 simp2d ⊢ ( 𝐹 ∈ 𝐸 → 𝑅 ∈ CRing )
10 id ⊢ ( 𝐹 ∈ 𝐸 → 𝐹 ∈ 𝐸 )
11 10 3 eleqtrdi ⊢ ( 𝐹 ∈ 𝐸 → 𝐹 ∈ ran ( 1o eval 𝑅 ) )
12 1on ⊢ 1o ∈ On
13 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
14 eqid ⊢ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) = ( 𝑅 ↑s ( 𝐵 ↑m 1o ) )
15 4 2 13 14 evlrhm ⊢ ( ( 1o ∈ On ∧ 𝑅 ∈ CRing ) → ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
16 12 9 15 sylancr ⊢ ( 𝐹 ∈ 𝐸 → ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
17 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
18 eqid ⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
19 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
20 17 18 19 ply1bas ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
21 eqid ⊢ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) )
22 20 21 rhmf ⊢ ( ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) → ( 1o eval 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
23 ffn ⊢ ( ( 1o eval 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) → ( 1o eval 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
24 fvelrnb ⊢ ( ( 1o eval 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) → ( 𝐹 ∈ ran ( 1o eval 𝑅 ) ↔ ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 ) )
25 16 22 23 24 4syl ⊢ ( 𝐹 ∈ 𝐸 → ( 𝐹 ∈ ran ( 1o eval 𝑅 ) ↔ ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 ) )
26 11 25 mpbid ⊢ ( 𝐹 ∈ 𝐸 → ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 )
27 eqid ⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
28 27 4 2 13 20 evl1val ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
29 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
30 27 17 29 2 evl1rhm ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
31 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
32 19 31 rhmf ⊢ ( ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
33 ffn ⊢ ( ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
34 30 32 33 3syl ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
35 fnfvelrn ⊢ ( ( ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ran ( eval1 ‘ 𝑅 ) )
36 34 35 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ran ( eval1 ‘ 𝑅 ) )
37 36 1 eleqtrrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑄 )
38 28 37 eqeltrrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 )
39 coeq1 ⊢ ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
40 39 eleq1d ⊢ ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ↔ ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ) )
41 38 40 syl5ibcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ) )
42 41 rexlimdva ⊢ ( 𝑅 ∈ CRing → ( ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ) )
43 9 26 42 sylc ⊢ ( 𝐹 ∈ 𝐸 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 )