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	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
19	17 18	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
20		eqid	$⊢ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
21	19 20	rhmf	$⊢ 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}}))) \to (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
22		ffn	$⊢ (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} \to (1_{𝑜} eval R) Fn {Base}_{{Poly}_{1} (R)}$
23		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)$
24	16 21 22 23	4syl	$⊢ F \in E \to (F \in ran (1_{𝑜} eval R) \leftrightarrow \exists x \in {Base}_{{Poly}_{1} (R)} (1_{𝑜} eval R) (x) = F)$
25	11 24	mpbid	$⊢ F \in E \to \exists x \in {Base}_{{Poly}_{1} (R)} (1_{𝑜} eval R) (x) = F$
26		eqid	$⊢ {eval}_{1} (R) = {eval}_{1} (R)$
27	26 4 2 13 19	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\})$
28		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
29	26 17 28 2	evl1rhm	$⊢ R \in CRing \to {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B))$
30		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
31	18 30	rhmf	$⊢ {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B)) \to {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)}$
32		ffn	$⊢ {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)} \to {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)}$
33	29 31 32	3syl	$⊢ R \in CRing \to {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)}$
34		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)$
35	33 34	sylan	$⊢ (R \in CRing \land x \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (x) \in ran {eval}_{1} (R)$
36	35 1	eleqtrrdi	$⊢ (R \in CRing \land x \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (x) \in Q$
37	27 36	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$
38		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\})$
39	38	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)$
40	37 39	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)$
41	40	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)$
42	9 25 41	sylc	$⊢ F \in E \to F \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in Q$

Metamath Proof Explorer

Theorem mpfpf1

Proof