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	8 12	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
22	7 19 2 20 21	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\})$
23	22	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))$
24		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)))$
25		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
26	2	fvexi	$⊢ B \in V$
27		0ex	$⊢ \emptyset \in V$
28		eqid	$⊢ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) = (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))$
29	25 26 27 28	mapsncnv	$⊢ {(x \in (B^{1_{𝑜}}) ⟼ x (\emptyset))}^{-1} = (z \in B ⟼ 1_{𝑜} \times \{z\})$
30	29	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))$
31	25 26 27 28	mapsnf1o2	$⊢ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B$
32		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_{𝑜}})}$
33	31 32	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_{𝑜}})}$
34	30 33	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_{𝑜}})}$
35	34	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_{𝑜}})})$
36	24 35	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_{𝑜}})})$
37		eqid	$⊢ R ↑_{𝑠} (B^{1_{𝑜}}) = R ↑_{𝑠} (B^{1_{𝑜}})$
38		eqid	$⊢ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
39		simpl	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to R \in CRing$
40		ovexd	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to B^{1_{𝑜}} \in V$
41		1on	$⊢ 1_{𝑜} \in On$
42	19 2 20 37	evlrhm	$⊢ (1_{𝑜} \in On \land R \in CRing) \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
43	41 42	mpan	$⊢ R \in CRing \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
44	21 38	rhmf	$⊢ 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}}))) \to (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
45	43 44	syl	$⊢ R \in CRing \to (1_{𝑜} eval R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
46	45	ffvelcdmda	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
47	37 2 38 39 40 46	pwselbas	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) : B^{1_{𝑜}} ⟶ B$
48		fcoi1	$⊢ (1_{𝑜} eval R) (y) : B^{1_{𝑜}} ⟶ B \to (1_{𝑜} eval R) (y) \circ ({I ↾}_{(B^{1_{𝑜}})}) = (1_{𝑜} eval R) (y)$
49	47 48	syl	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \circ ({I ↾}_{(B^{1_{𝑜}})}) = (1_{𝑜} eval R) (y)$
50	23 36 49	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)$
51	45	ffnd	$⊢ R \in CRing \to (1_{𝑜} eval R) Fn {Base}_{{Poly}_{1} (R)}$
52		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)$
53	51 52	sylan	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \in ran (1_{𝑜} eval R)$
54	53 3	eleqtrrdi	$⊢ (R \in CRing \land y \in {Base}_{{Poly}_{1} (R)}) \to (1_{𝑜} eval R) (y) \in E$
55	50 54	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$
56		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))$
57	56	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)$
58	55 57	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)$
59	58	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)$
60	4 18 59	sylc	$⊢ F \in Q \to F \circ (x \in (B^{1_{𝑜}}) ⟼ x (\emptyset)) \in E$

Metamath Proof Explorer

Theorem pf1mpf

Proof