pf1mpf

Description: Convert a univariate polynomial function to multivariate. (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	pf1mpf	$⊢ F \in Q \to F \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E$

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	1	pf1rcl	$⊢ F \in Q \to R \in CRing$
5		id	$⊢ F \in Q \to F \in Q$
6	5 1	eleqtrdi	$⊢ F \in Q \to F \in ran {eval}_{1} (R)$
7		eqid	$⊢ {eval}_{1} (R) = {eval}_{1} (R)$
8		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
9		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
10	7 8 9 2	evl1rhm	$⊢ R \in CRing \to {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B))$
11	4 10	syl	$⊢ F \in Q \to {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B))$
12		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
13		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
14	12 13	rhmf	$⊢ {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B)) \to {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)}$
15		ffn	$⊢ {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)} \to {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)}$
16		fvelrnb	$⊢ {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)} \to (F \in ran {eval}_{1} (R) \leftrightarrow \exists y \in {Base}_{{Poly}_{1} (R)} {eval}_{1} (R) (y) = F)$
17	11 14 15 16	4syl	$⊢ F \in Q \to (F \in ran {eval}_{1} (R) \leftrightarrow \exists y \in {Base}_{{Poly}_{1} (R)} {eval}_{1} (R) (y) = F)$
18	6 17	mpbid	$⊢ F \in Q \to \exists y \in {Base}_{{Poly}_{1} (R)} {eval}_{1} (R) (y) = F$
19		eqid	$⊢ 1_{𝑜} eval R = 1_{𝑜} eval R$
20		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
21		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
22	8 21 12	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
23	7 19 2 20 22	evl1val	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (y) = (1_{𝑜} eval R) (y) \circ (z \in B ⟼ 1_{𝑜} \times \{z\})$
24	23	coeq1d	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (y) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = ((1_{𝑜} eval R) (y) \circ (z \in B ⟼ 1_{𝑜} \times \{z\})) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))$
25		coass	$⊢ ((1_{𝑜} eval R) (y) \circ (z \in B ⟼ 1_{𝑜} \times \{z\})) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = (1_{𝑜} eval R) (y) \circ ((z \in B ⟼ 1_{𝑜} \times \{z\}) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)))$
26		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
27	2	fvexi	$⊢ B \in V$
28		0ex	$⊢ \emptyset \in V$
29		eqid	$⊢ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))$
30	26 27 28 29	mapsncnv	$⊢ {(x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))}^{-1} = (z \in B ⟼ 1_{𝑜} \times \{z\})$
31	30	coeq1i	$⊢ {(x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))}^{-1} \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = (z \in B ⟼ 1_{𝑜} \times \{z\}) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))$
32	26 27 28 29	mapsnf1o2	$⊢ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B$
33		f1ococnv1	$⊢ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B \to {(x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))}^{-1} \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = {I ↾}_{(B^{1_{𝑜}})}$
34	32 33	mp1i	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to {(x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))}^{-1} \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = {I ↾}_{(B^{1_{𝑜}})}$
35	31 34	eqtr3id	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (z \in B ⟼ 1_{𝑜} \times \{z\}) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = {I ↾}_{(B^{1_{𝑜}})}$
36	35	coeq2d	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \circ ((z \in B ⟼ 1_{𝑜} \times \{z\}) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))) = (1_{𝑜} eval R) (y) \circ ({I ↾}_{(B^{1_{𝑜}})})$
37	25 36	eqtrid	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to ((1_{𝑜} eval R) (y) \circ (z \in B ⟼ 1_{𝑜} \times \{z\})) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = (1_{𝑜} eval R) (y) \circ ({I ↾}_{(B^{1_{𝑜}})})$
38		eqid	$⊢ R ↑_{𝑠} (B^{1_{𝑜}}) = R ↑_{𝑠} (B^{1_{𝑜}})$
39		eqid	$⊢ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
40		simpl	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to R \in CRing$
41		ovexd	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to B^{1_{𝑜}} \in V$
42		1on	$⊢ 1_{𝑜} \in On$
43	19 2 20 38	evlrhm	$⊢ (1_{𝑜} \in On \land R \in CRing) \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
44	42 43	mpan	$⊢ R \in CRing \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
45	22 39	rhmf	$⊢ 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}}))) \to (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
46	44 45	syl	$⊢ R \in CRing \to (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
47	46	ffvelcdmda	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
48	38 2 39 40 41 47	pwselbas	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) : B^{1_{𝑜}} ⟶ B$
49		fcoi1	$⊢ (1_{𝑜} eval R) (y) : B^{1_{𝑜}} ⟶ B \to (1_{𝑜} eval R) (y) \circ ({I ↾}_{(B^{1_{𝑜}})}) = (1_{𝑜} eval R) (y)$
50	48 49	syl	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \circ ({I ↾}_{(B^{1_{𝑜}})}) = (1_{𝑜} eval R) (y)$
51	24 37 50	3eqtrd	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (y) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = (1_{𝑜} eval R) (y)$
52	46	ffnd	$⊢ R \in CRing \to (1_{𝑜} eval R) Fn {Base}_{{Poly}_{1} (R)}$
53		fnfvelrn	$⊢ ((1_{𝑜} eval R) Fn {Base}_{{Poly}_{1} (R)} \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \in ran (1_{𝑜} eval R)$
54	52 53	sylan	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \in ran (1_{𝑜} eval R)$
55	54 3	eleqtrrdi	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \in E$
56	51 55	eqeltrd	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) (y) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E$
57		coeq1	$⊢ {eval}_{1} (R) (y) = F \to {eval}_{1} (R) (y) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = F \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))$
58	57	eleq1d	$⊢ {eval}_{1} (R) (y) = F \to ({eval}_{1} (R) (y) \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E \leftrightarrow F \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E)$
59	56 58	syl5ibcom	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to ({eval}_{1} (R) (y) = F \to F \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E)$
60	59	rexlimdva	$⊢ R \in CRing \to (\exists y \in {Base}_{{Poly}_{1} (R)} {eval}_{1} (R) (y) = F \to F \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E)$
61	4 18 60	sylc	$⊢ F \in Q \to F \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E$

Metamath Proof Explorer

Theorem pf1mpf

Proof