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	8 12	ply1bas	⊢ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) = ( Base ‘ ( 1_o mPoly 𝑅 ) )
22	7 19 2 20 21	evl1val	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) = ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ) )
23	22	coeq1d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
24		coass	⊢ ( ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
25		df1o2	⊢ 1_o = { ∅ }
26	2	fvexi	⊢ 𝐵 ∈ V
27		0ex	⊢ ∅ ∈ V
28		eqid	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) )
29	25 26 27 28	mapsncnv	⊢ ^◡ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) )
30	29	coeq1i	⊢ ( ^◡ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) )
31	25 26 27 28	mapsnf1o2	⊢ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( 𝐵 ↑_m 1_o ) –1-1-onto→ 𝐵
32		f1ococnv1	⊢ ( ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) : ( 𝐵 ↑_m 1_o ) –1-1-onto→ 𝐵 → ( ^◡ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( I ↾ ( 𝐵 ↑_m 1_o ) ) )
33	31 32	mp1i	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ^◡ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( I ↾ ( 𝐵 ↑_m 1_o ) ) )
34	30 33	eqtr3id	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( I ↾ ( 𝐵 ↑_m 1_o ) ) )
35	34	coeq2d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ) = ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵 ↑_m 1_o ) ) ) )
36	24 35	eqtrid	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑧 ∈ 𝐵 ↦ ( 1_o × { 𝑧 } ) ) ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵 ↑_m 1_o ) ) ) )
37		eqid	⊢ ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) = ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) )
38		eqid	⊢ ( Base ‘ ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) ) = ( Base ‘ ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) )
39		simpl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → 𝑅 ∈ CRing )
40		ovexd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( 𝐵 ↑_m 1_o ) ∈ V )
41		1on	⊢ 1_o ∈ On
42	19 2 20 37	evlrhm	⊢ ( ( 1_o ∈ On ∧ 𝑅 ∈ CRing ) → ( 1_o eval 𝑅 ) ∈ ( ( 1_o mPoly 𝑅 ) RingHom ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) ) )
43	41 42	mpan	⊢ ( 𝑅 ∈ CRing → ( 1_o eval 𝑅 ) ∈ ( ( 1_o mPoly 𝑅 ) RingHom ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) ) )
44	21 38	rhmf	⊢ ( ( 1_o eval 𝑅 ) ∈ ( ( 1_o mPoly 𝑅 ) RingHom ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) ) → ( 1_o eval 𝑅 ) : ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) ) )
45	43 44	syl	⊢ ( 𝑅 ∈ CRing → ( 1_o eval 𝑅 ) : ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) ) )
46	45	ffvelcdmda	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ↑_s ( 𝐵 ↑_m 1_o ) ) ) )
47	37 2 38 39 40 46	pwselbas	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) : ( 𝐵 ↑_m 1_o ) ⟶ 𝐵 )
48		fcoi1	⊢ ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) : ( 𝐵 ↑_m 1_o ) ⟶ 𝐵 → ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵 ↑_m 1_o ) ) ) = ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) )
49	47 48	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∘ ( I ↾ ( 𝐵 ↑_m 1_o ) ) ) = ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) )
50	23 36 49	3eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) )
51	45	ffnd	⊢ ( 𝑅 ∈ CRing → ( 1_o eval 𝑅 ) Fn ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
52		fnfvelrn	⊢ ( ( ( 1_o eval 𝑅 ) Fn ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∈ ran ( 1_o eval 𝑅 ) )
53	51 52	sylan	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∈ ran ( 1_o eval 𝑅 ) )
54	53 3	eleqtrrdi	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( 1_o eval 𝑅 ) ‘ 𝑦 ) ∈ 𝐸 )
55	50 54	eqeltrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 )
56		coeq1	⊢ ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) = 𝐹 → ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) = ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) )
57	56	eleq1d	⊢ ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) = 𝐹 → ( ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ↔ ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ) )
58	55 57	syl5ibcom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) = 𝐹 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ) )
59	58	rexlimdva	⊢ ( 𝑅 ∈ CRing → ( ∃ 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( eval₁ ‘ 𝑅 ) ‘ 𝑦 ) = 𝐹 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 ) )
60	4 18 59	sylc	⊢ ( 𝐹 ∈ 𝑄 → ( 𝐹 ∘ ( 𝑥 ∈ ( 𝐵 ↑_m 1_o ) ↦ ( 𝑥 ‘ ∅ ) ) ) ∈ 𝐸 )

Metamath Proof Explorer

Theorem pf1mpf

Proof