evl1sca

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

	Ref	Expression
Hypotheses	evl1sca.o	$⊢ O = {eval}_{1} (R)$
	evl1sca.p	$⊢ P = {Poly}_{1} (R)$
	evl1sca.b	$⊢ B = {Base}_{R}$
	evl1sca.a	$⊢ A = algSc (P)$
Assertion	evl1sca	$⊢ (R \in CRing \land X \in B) \to O (A (X)) = B \times \{X\}$

Proof

Step	Hyp	Ref	Expression
1		evl1sca.o	$⊢ O = {eval}_{1} (R)$
2		evl1sca.p	$⊢ P = {Poly}_{1} (R)$
3		evl1sca.b	$⊢ B = {Base}_{R}$
4		evl1sca.a	$⊢ A = algSc (P)$
5		crngring	$⊢ R \in CRing \to R \in Ring$
6	5	adantr	$⊢ (R \in CRing \land X \in B) \to R \in Ring$
7		eqid	$⊢ {Base}_{P} = {Base}_{P}$
8	2 4 3 7	ply1sclf	$⊢ R \in Ring \to A : B ⟶ {Base}_{P}$
9	6 8	syl	$⊢ (R \in CRing \land X \in B) \to A : B ⟶ {Base}_{P}$
10		ffvelrn	$⊢ (A : B ⟶ {Base}_{P} \land X \in B) \to A (X) \in {Base}_{P}$
11	9 10	sylancom	$⊢ (R \in CRing \land X \in B) \to A (X) \in {Base}_{P}$
12		eqid	$⊢ 1_{𝑜} eval R = 1_{𝑜} eval R$
13		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
14		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
15	2 14 7	ply1bas	$⊢ {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
16	1 12 3 13 15	evl1val	$⊢ (R \in CRing \land A (X) \in {Base}_{P}) \to O (A (X)) = (1_{𝑜} eval R) (A (X)) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
17	11 16	syldan	$⊢ (R \in CRing \land X \in B) \to O (A (X)) = (1_{𝑜} eval R) (A (X)) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
18	3	ressid	$⊢ R \in CRing \to R ↾_{𝑠} B = R$
19	18	adantr	$⊢ (R \in CRing \land X \in B) \to R ↾_{𝑠} B = R$
20	19	oveq2d	$⊢ (R \in CRing \land X \in B) \to 1_{𝑜} mPoly (R ↾_{𝑠} B) = 1_{𝑜} mPoly R$
21	20	fveq2d	$⊢ (R \in CRing \land X \in B) \to algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) = algSc (1_{𝑜} mPoly R)$
22	2 4	ply1ascl	$⊢ A = algSc (1_{𝑜} mPoly R)$
23	21 22	syl6reqr	$⊢ (R \in CRing \land X \in B) \to A = algSc (1_{𝑜} mPoly (R ↾_{𝑠} B))$
24	23	fveq1d	$⊢ (R \in CRing \land X \in B) \to A (X) = algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (X)$
25	24	fveq2d	$⊢ (R \in CRing \land X \in B) \to (1_{𝑜} eval R) (A (X)) = (1_{𝑜} eval R) (algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (X))$
26	12 3	evlval	$⊢ 1_{𝑜} eval R = (1_{𝑜} evalSub R) (B)$
27		eqid	$⊢ 1_{𝑜} mPoly (R ↾_{𝑠} B) = 1_{𝑜} mPoly (R ↾_{𝑠} B)$
28		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
29		eqid	$⊢ algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) = algSc (1_{𝑜} mPoly (R ↾_{𝑠} B))$
30		1on	$⊢ 1_{𝑜} \in On$
31	30	a1i	$⊢ (R \in CRing \land X \in B) \to 1_{𝑜} \in On$
32		simpl	$⊢ (R \in CRing \land X \in B) \to R \in CRing$
33	3	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
34	6 33	syl	$⊢ (R \in CRing \land X \in B) \to B \in SubRing (R)$
35		simpr	$⊢ (R \in CRing \land X \in B) \to X \in B$
36	26 27 28 3 29 31 32 34 35	evlssca	$⊢ (R \in CRing \land X \in B) \to (1_{𝑜} eval R) (algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (X)) = (B^{1_{𝑜}}) \times \{X\}$
37	25 36	eqtrd	$⊢ (R \in CRing \land X \in B) \to (1_{𝑜} eval R) (A (X)) = (B^{1_{𝑜}}) \times \{X\}$
38	37	coeq1d	$⊢ (R \in CRing \land X \in B) \to (1_{𝑜} eval R) (A (X)) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
39		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
40	3	fvexi	$⊢ B \in V$
41		0ex	$⊢ \emptyset \in V$
42		eqid	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
43	39 40 41 42	mapsnf1o3	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) : B \underset{1-1 onto}{⟶} B^{1_{𝑜}}$
44		f1of	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) : B \underset{1-1 onto}{⟶} B^{1_{𝑜}} \to (y \in B ⟼ 1_{𝑜} \times \{y\}) : B ⟶ B^{1_{𝑜}}$
45	43 44	mp1i	$⊢ (R \in CRing \land X \in B) \to (y \in B ⟼ 1_{𝑜} \times \{y\}) : B ⟶ B^{1_{𝑜}}$
46	42	fmpt	$⊢ \forall y \in B 1_{𝑜} \times \{y\} \in (B^{1_{𝑜}}) \leftrightarrow (y \in B ⟼ 1_{𝑜} \times \{y\}) : B ⟶ B^{1_{𝑜}}$
47	45 46	sylibr	$⊢ (R \in CRing \land X \in B) \to \forall y \in B 1_{𝑜} \times \{y\} \in (B^{1_{𝑜}})$
48		eqidd	$⊢ (R \in CRing \land X \in B) \to (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
49		fconstmpt	$⊢ (B^{1_{𝑜}}) \times \{X\} = (x \in (B^{1_{𝑜}}) ⟼ X)$
50	49	a1i	$⊢ (R \in CRing \land X \in B) \to (B^{1_{𝑜}}) \times \{X\} = (x \in (B^{1_{𝑜}}) ⟼ X)$
51		eqidd	$⊢ x = 1_{𝑜} \times \{y\} \to X = X$
52	47 48 50 51	fmptcof	$⊢ (R \in CRing \land X \in B) \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ X)$
53		fconstmpt	$⊢ B \times \{X\} = (y \in B ⟼ X)$
54	52 53	eqtr4di	$⊢ (R \in CRing \land X \in B) \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = B \times \{X\}$
55	17 38 54	3eqtrd	$⊢ (R \in CRing \land X \in B) \to O (A (X)) = B \times \{X\}$

Metamath Proof Explorer

Theorem evl1sca

Proof