Theorem evl1sca

Description: Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	evl1sca.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	evl1sca.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	evl1sca.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evl1sca.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	evl1sca	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		evl1sca.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		evl1sca.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		evl1sca.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evl1sca.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
5		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6	5	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
7		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8	2 4 3 7	ply1sclf	⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) )
9	6 8	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) )
10		ffvelrn	⊢ ( ( 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
11	9 10	sylancom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
12		eqid	⊢ ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
13		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
14		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
15	2 14 7	ply1bas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
16	1 12 3 13 15	evl1val	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
17	11 16	syldan	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
18	2 4	ply1ascl	⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )
19	3	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
20	19	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
21	20	oveq2d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 1o mPoly 𝑅 ) )
22	21	fveq2d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly 𝑅 ) ) )
23	18 22	eqtr4id	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝐴 = ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) )
24	23	fveq1d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) = ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑋 ) )
25	24	fveq2d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) )
26	12 3	evlval	⊢ ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
27		eqid	⊢ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 1o mPoly ( 𝑅 ↾s 𝐵 ) )
28		eqid	⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
29		eqid	⊢ ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) )
30		1on	⊢ 1o ∈ On
31	30	a1i	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 1o ∈ On )
32		simpl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ CRing )
33	3	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
34	6 33	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
35		simpr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
36	26 27 28 3 29 31 32 34 35	evlssca	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
37	25 36	eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
38	37	coeq1d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
39		df1o2	⊢ 1o = { ∅ }
40	3	fvexi	⊢ 𝐵 ∈ V
41		0ex	⊢ ∅ ∈ V
42		eqid	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) )
43	39 40 41 42	mapsnf1o3	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o )
44		f1of	⊢ ( ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o ) → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
45	43 44	mp1i	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
46	42	fmpt	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
47	45 46	sylibr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) )
48		eqidd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) )
49		fconstmpt	⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑥 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 )
50	49	a1i	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑥 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 ) )
51		eqidd	⊢ ( 𝑥 = ( 1o × { 𝑦 } ) → 𝑋 = 𝑋 )
52	47 48 50 51	fmptcof	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
53		fconstmpt	⊢ ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 )
54	52 53	eqtr4di	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝐵 × { 𝑋 } ) )
55	17 38 54	3eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )