evl1var

Description: Polynomial evaluation maps the variable to the identity function. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	evl1var.q	$⊢ O = {eval}_{1} (R)$
	evl1var.v	$⊢ X = {var}_{1} (R)$
	evl1var.b	$⊢ B = {Base}_{R}$
Assertion	evl1var	$⊢ R \in CRing \to O (X) = {I ↾}_{B}$

Proof

Step	Hyp	Ref	Expression
1		evl1var.q	$⊢ O = {eval}_{1} (R)$
2		evl1var.v	$⊢ X = {var}_{1} (R)$
3		evl1var.b	$⊢ B = {Base}_{R}$
4		crngring	$⊢ R \in CRing \to R \in Ring$
5		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
6		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
7	2 5 6	vr1cl	$⊢ R \in Ring \to X \in {Base}_{{Poly}_{1} (R)}$
8	4 7	syl	$⊢ R \in CRing \to X \in {Base}_{{Poly}_{1} (R)}$
9		eqid	$⊢ 1_{𝑜} eval R = 1_{𝑜} eval R$
10		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
11	5 6	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
12	1 9 3 10 11	evl1val	$⊢ (R \in CRing \land X \in {Base}_{{Poly}_{1} (R)}) \to O (X) = (1_{𝑜} eval R) (X) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
13	8 12	mpdan	$⊢ R \in CRing \to O (X) = (1_{𝑜} eval R) (X) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
14		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
15	3	fvexi	$⊢ B \in V$
16		0ex	$⊢ \emptyset \in V$
17		eqid	$⊢ (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))$
18	14 15 16 17	mapsncnv	$⊢ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = (y \in B ⟼ 1_{𝑜} \times \{y\})$
19	18	coeq2i	$⊢ (1_{𝑜} eval R) (X) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = (1_{𝑜} eval R) (X) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
20	3	ressid	$⊢ R \in CRing \to R ↾_{𝑠} B = R$
21	20	oveq2d	$⊢ R \in CRing \to 1_{𝑜} mVar (R ↾_{𝑠} B) = 1_{𝑜} mVar R$
22	21	fveq1d	$⊢ R \in CRing \to (1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset) = (1_{𝑜} mVar R) (\emptyset)$
23	2	vr1val	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$
24	22 23	eqtr4di	$⊢ R \in CRing \to (1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset) = X$
25	24	fveq2d	$⊢ R \in CRing \to (1_{𝑜} eval R) ((1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset)) = (1_{𝑜} eval R) (X)$
26	9 3	evlval	$⊢ 1_{𝑜} eval R = (1_{𝑜} evalSub R) (B)$
27		eqid	$⊢ 1_{𝑜} mVar (R ↾_{𝑠} B) = 1_{𝑜} mVar (R ↾_{𝑠} B)$
28		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
29		1on	$⊢ 1_{𝑜} \in On$
30	29	a1i	$⊢ R \in CRing \to 1_{𝑜} \in On$
31		id	$⊢ R \in CRing \to R \in CRing$
32	3	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
33	4 32	syl	$⊢ R \in CRing \to B \in SubRing (R)$
34		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
35	34	a1i	$⊢ R \in CRing \to \emptyset \in 1_{𝑜}$
36	26 27 28 3 30 31 33 35	evlsvar	$⊢ R \in CRing \to (1_{𝑜} eval R) ((1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset)) = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))$
37	25 36	eqtr3d	$⊢ R \in CRing \to (1_{𝑜} eval R) (X) = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))$
38	37	coeq1d	$⊢ R \in CRing \to (1_{𝑜} eval R) (X) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1}$
39	19 38	eqtr3id	$⊢ R \in CRing \to (1_{𝑜} eval R) (X) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1}$
40	14 15 16 17	mapsnf1o2	$⊢ (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B$
41		f1ococnv2	$⊢ (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B \to (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = {I ↾}_{B}$
42	40 41	mp1i	$⊢ R \in CRing \to (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = {I ↾}_{B}$
43	13 39 42	3eqtrd	$⊢ R \in CRing \to O (X) = {I ↾}_{B}$

Metamath Proof Explorer

Theorem evl1var

Proof