Theorem evl1var

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

	Ref	Expression
Hypotheses	evl1var.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	evl1var.v	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	evl1var.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	evl1var	⊢ ( 𝑅 ∈ CRing → ( 𝑂 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		evl1var.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		evl1var.v	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		evl1var.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
5		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
7	2 5 6	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
8	4 7	syl	⊢ ( 𝑅 ∈ CRing → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
9		eqid	⊢ ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
10		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
11		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
12	5 11 6	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
13	1 9 3 10 12	evl1val	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( 𝑂 ‘ 𝑋 ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
14	8 13	mpdan	⊢ ( 𝑅 ∈ CRing → ( 𝑂 ‘ 𝑋 ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
15		df1o2	⊢ 1o = { ∅ }
16	3	fvexi	⊢ 𝐵 ∈ V
17		0ex	⊢ ∅ ∈ V
18		eqid	⊢ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) )
19	15 16 17 18	mapsncnv	⊢ ◡ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) )
20	19	coeq2i	⊢ ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ◡ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) )
21	3	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
22	21	oveq2d	⊢ ( 𝑅 ∈ CRing → ( 1o mVar ( 𝑅 ↾s 𝐵 ) ) = ( 1o mVar 𝑅 ) )
23	22	fveq1d	⊢ ( 𝑅 ∈ CRing → ( ( 1o mVar ( 𝑅 ↾s 𝐵 ) ) ‘ ∅ ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
24	2	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
25	23 24	eqtr4di	⊢ ( 𝑅 ∈ CRing → ( ( 1o mVar ( 𝑅 ↾s 𝐵 ) ) ‘ ∅ ) = 𝑋 )
26	25	fveq2d	⊢ ( 𝑅 ∈ CRing → ( ( 1o eval 𝑅 ) ‘ ( ( 1o mVar ( 𝑅 ↾s 𝐵 ) ) ‘ ∅ ) ) = ( ( 1o eval 𝑅 ) ‘ 𝑋 ) )
27	9 3	evlval	⊢ ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
28		eqid	⊢ ( 1o mVar ( 𝑅 ↾s 𝐵 ) ) = ( 1o mVar ( 𝑅 ↾s 𝐵 ) )
29		eqid	⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
30		1on	⊢ 1o ∈ On
31	30	a1i	⊢ ( 𝑅 ∈ CRing → 1o ∈ On )
32		id	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CRing )
33	3	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
34	4 33	syl	⊢ ( 𝑅 ∈ CRing → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
35		0lt1o	⊢ ∅ ∈ 1o
36	35	a1i	⊢ ( 𝑅 ∈ CRing → ∅ ∈ 1o )
37	27 28 29 3 31 32 34 36	evlsvar	⊢ ( 𝑅 ∈ CRing → ( ( 1o eval 𝑅 ) ‘ ( ( 1o mVar ( 𝑅 ↾s 𝐵 ) ) ‘ ∅ ) ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) )
38	26 37	eqtr3d	⊢ ( 𝑅 ∈ CRing → ( ( 1o eval 𝑅 ) ‘ 𝑋 ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) )
39	38	coeq1d	⊢ ( 𝑅 ∈ CRing → ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ◡ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ◡ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) )
40	20 39	eqtr3id	⊢ ( 𝑅 ∈ CRing → ( ( ( 1o eval 𝑅 ) ‘ 𝑋 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ◡ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) )
41	15 16 17 18	mapsnf1o2	⊢ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) : ( 𝐵 ↑m 1o ) –1-1-onto→ 𝐵
42		f1ococnv2	⊢ ( ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) : ( 𝐵 ↑m 1o ) –1-1-onto→ 𝐵 → ( ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ◡ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( I ↾ 𝐵 ) )
43	41 42	mp1i	⊢ ( 𝑅 ∈ CRing → ( ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ∘ ◡ ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑧 ‘ ∅ ) ) ) = ( I ↾ 𝐵 ) )
44	14 40 43	3eqtrd	⊢ ( 𝑅 ∈ CRing → ( 𝑂 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )