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		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
12	5 11 6	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
13	1 9 3 10 12	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\})$
14	8 13	mpdan	$⊢ R \in CRing \to O (X) = (1_{𝑜} eval R) (X) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
15		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
16	3	fvexi	$⊢ B \in V$
17		0ex	$⊢ \emptyset \in V$
18		eqid	$⊢ (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))$
19	15 16 17 18	mapsncnv	$⊢ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = (y \in B ⟼ 1_{𝑜} \times \{y\})$
20	19	coeq2i	$⊢ (1_{𝑜} eval R) (X) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = (1_{𝑜} eval R) (X) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
21	3	ressid	$⊢ R \in CRing \to R ↾_{𝑠} B = R$
22	21	oveq2d	$⊢ R \in CRing \to 1_{𝑜} mVar (R ↾_{𝑠} B) = 1_{𝑜} mVar R$
23	22	fveq1d	$⊢ R \in CRing \to (1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset) = (1_{𝑜} mVar R) (\emptyset)$
24	2	vr1val	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$
25	23 24	syl6eqr	$⊢ R \in CRing \to (1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset) = X$
26	25	fveq2d	$⊢ R \in CRing \to (1_{𝑜} eval R) ((1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset)) = (1_{𝑜} eval R) (X)$
27	9 3	evlval	$⊢ 1_{𝑜} eval R = (1_{𝑜} evalSub R) (B)$
28		eqid	$⊢ 1_{𝑜} mVar (R ↾_{𝑠} B) = 1_{𝑜} mVar (R ↾_{𝑠} B)$
29		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
30		1on	$⊢ 1_{𝑜} \in On$
31	30	a1i	$⊢ R \in CRing \to 1_{𝑜} \in On$
32		id	$⊢ R \in CRing \to R \in CRing$
33	3	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
34	4 33	syl	$⊢ R \in CRing \to B \in SubRing (R)$
35		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
36	35	a1i	$⊢ R \in CRing \to \emptyset \in 1_{𝑜}$
37	27 28 29 3 31 32 34 36	evlsvar	$⊢ R \in CRing \to (1_{𝑜} eval R) ((1_{𝑜} mVar (R ↾_{𝑠} B)) (\emptyset)) = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))$
38	26 37	eqtr3d	$⊢ R \in CRing \to (1_{𝑜} eval R) (X) = (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))$
39	38	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}$
40	20 39	syl5eqr	$⊢ 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}$
41	15 16 17 18	mapsnf1o2	$⊢ (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B$
42		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}$
43	41 42	mp1i	$⊢ R \in CRing \to (z \in (B^{1_{𝑜}}) ⟼ z (\emptyset)) \circ {(z \in (B^{1_{𝑜}}) ⟼ z (\emptyset))}^{-1} = {I ↾}_{B}$
44	14 40 43	3eqtrd	$⊢ R \in CRing \to O (X) = {I ↾}_{B}$

Metamath Proof Explorer

Theorem evl1var

Proof