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 ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
19 17 18 ply1bas ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
20 eqid ⊢ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) )
21 19 20 rhmf ⊢ ( ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) → ( 1o eval 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
22 ffn ⊢ ( ( 1o eval 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) → ( 1o eval 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
23 fvelrnb ⊢ ( ( 1o eval 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) → ( 𝐹 ∈ ran ( 1o eval 𝑅 ) ↔ ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 ) )
24 16 21 22 23 4syl ⊢ ( 𝐹 ∈ 𝐸 → ( 𝐹 ∈ ran ( 1o eval 𝑅 ) ↔ ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 ) )
25 11 24 mpbid ⊢ ( 𝐹 ∈ 𝐸 → ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 )
26 eqid ⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
27 26 4 2 13 19 evl1val ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
28 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
29 26 17 28 2 evl1rhm ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
30 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
31 18 30 rhmf ⊢ ( ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
32 ffn ⊢ ( ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
33 29 31 32 3syl ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
34 fnfvelrn ⊢ ( ( ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ran ( eval1 ‘ 𝑅 ) )
35 33 34 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ran ( eval1 ‘ 𝑅 ) )
36 35 1 eleqtrrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑄 )
37 27 36 eqeltrrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 )
38 coeq1 ⊢ ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
39 38 eleq1d ⊢ ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ↔ ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ) )
40 37 39 syl5ibcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ) )
41 40 rexlimdva ⊢ ( 𝑅 ∈ CRing → ( ∃ 𝑥 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ( ( 1o eval 𝑅 ) ‘ 𝑥 ) = 𝐹 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 ) )
42 9 25 41 sylc ⊢ ( 𝐹 ∈ 𝐸 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ 𝑄 )