mpfpf1

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

	Ref	Expression
Hypotheses	pf1rcl.q	$⊢ Q = ran {eval}_{1} (R)$
	pf1f.b	$⊢ B = {Base}_{R}$
	mpfpf1.q	$⊢ E = ran (1_{𝑜} eval R)$
Assertion	mpfpf1	$⊢ F \in E \to F \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q$

Proof

Step	Hyp	Ref	Expression
1		pf1rcl.q	$⊢ Q = ran {eval}_{1} (R)$
2		pf1f.b	$⊢ B = {Base}_{R}$
3		mpfpf1.q	$⊢ E = ran (1_{𝑜} eval R)$
4		eqid	$⊢ 1_{𝑜} eval R = 1_{𝑜} eval R$
5	4 2	evlval	$⊢ 1_{𝑜} eval R = (1_{𝑜} evalSub R) (B)$
6	5	rneqi	$⊢ ran (1_{𝑜} eval R) = ran (1_{𝑜} evalSub R) (B)$
7	3 6	eqtri	$⊢ E = ran (1_{𝑜} evalSub R) (B)$
8	7	mpfrcl	$⊢ F \in E \to (1_{𝑜} \in V \land R \in CRing \land B \in SubRing (R))$
9	8	simp2d	$⊢ F \in E \to R \in CRing$
10		id	$⊢ F \in E \to F \in E$
11	10 3	eleqtrdi	$⊢ F \in E \to F \in ran (1_{𝑜} eval R)$
12		1on	$⊢ 1_{𝑜} \in On$
13		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
14		eqid	$⊢ R ↑_{𝑠} (B^{1_{𝑜}}) = R ↑_{𝑠} (B^{1_{𝑜}})$
15	4 2 13 14	evlrhm	$⊢ (1_{𝑜} \in On \land R \in CRing) \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
16	12 9 15	sylancr	$⊢ F \in E \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
17		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
18		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
19		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
20	17 18 19	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
21		eqid	$⊢ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
22	20 21	rhmf	$⊢ 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}}))) \to (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
23		ffn	$⊢ (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} \to (1_{𝑜} eval R) Fn {Base}_{{Poly}_{1} (R)}$
24		fvelrnb	$⊢ (1_{𝑜} eval R) Fn {Base}_{{Poly}_{1} (R)} \to (F \in ran (1_{𝑜} eval R) \leftrightarrow \exists x \in {Base}_{{Poly}_{1} (R)} (1_{𝑜} eval R) (x) = F)$
25	16 22 23 24	4syl	$⊢ F \in E \to (F \in ran (1_{𝑜} eval R) \leftrightarrow \exists x \in {Base}_{{Poly}_{1} (R)} (1_{𝑜} eval R) (x) = F)$
26	11 25	mpbid	$⊢ F \in E \to \exists x \in {Base}_{{Poly}_{1} (R)} (1_{𝑜} eval R) (x) = F$
27		eqid	$⊢ {eval}_{1} (R) = {eval}_{1} (R)$
28	27 4 2 13 20	evl1val	$⊢ (R \in CRing \land x \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (x) = (1_{𝑜} eval R) (x) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
29		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
30	27 17 29 2	evl1rhm	$⊢ R \in CRing \to {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B))$
31		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
32	19 31	rhmf	$⊢ {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B)) \to {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)}$
33		ffn	$⊢ {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)} \to {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)}$
34	30 32 33	3syl	$⊢ R \in CRing \to {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)}$
35		fnfvelrn	$⊢ ({eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)} \land x \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (x) \in ran {eval}_{1} (R)$
36	34 35	sylan	$⊢ (R \in CRing \land x \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (x) \in ran {eval}_{1} (R)$
37	36 1	eleqtrrdi	$⊢ (R \in CRing \land x \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (x) \in Q$
38	28 37	eqeltrrd	$⊢ (R \in CRing \land x \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (x) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q$
39		coeq1	$⊢ (1_{𝑜} eval R) (x) = F \to (1_{𝑜} eval R) (x) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = F \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
40	39	eleq1d	$⊢ (1_{𝑜} eval R) (x) = F \to ((1_{𝑜} eval R) (x) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q \leftrightarrow F \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q)$
41	38 40	syl5ibcom	$⊢ (R \in CRing \land x \in {Base}_{{Poly}_{1} (R)}) \to ((1_{𝑜} eval R) (x) = F \to F \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q)$
42	41	rexlimdva	$⊢ R \in CRing \to (\exists x \in {Base}_{{Poly}_{1} (R)} (1_{𝑜} eval R) (x) = F \to F \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q)$
43	9 26 42	sylc	$⊢ F \in E \to F \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q$

Metamath Proof Explorer

Theorem mpfpf1

Proof