pf1mpf

Description: Convert a univariate polynomial function to multivariate. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pf1rcl.q	⊢ 𝑄 = ran ( eval₁ ‘ 𝑅 )
	pf1f.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mpfpf1.q	⊢ 𝐸 = ran ( 1_o eval 𝑅 )
Assertion	pf1mpf	⊢ ( 𝐹 ∈ 𝑄 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 )

Proof

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

Metamath Proof Explorer

Theorem pf1mpf

Proof