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		ffvelcdm	$⊢ (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	2 7	ply1bas	$⊢ {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
15	1 12 3 13 14	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\})$
16	11 15	syldan	$⊢ (R \in CRing \land X \in B) \to O (A (X)) = (1_{𝑜} eval R) (A (X)) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
17	2 4	ply1ascl	$⊢ A = algSc (1_{𝑜} mPoly R)$
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	17 21	eqtr4id	$⊢ (R \in CRing \land X \in B) \to A = algSc (1_{𝑜} mPoly (R ↾_{𝑠} B))$
23	22	fveq1d	$⊢ (R \in CRing \land X \in B) \to A (X) = algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (X)$
24	23	fveq2d	$⊢ (R \in CRing \land X \in B) \to (1_{𝑜} eval R) (A (X)) = (1_{𝑜} eval R) (algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (X))$
25	12 3	evlval	$⊢ 1_{𝑜} eval R = (1_{𝑜} evalSub R) (B)$
26		eqid	$⊢ 1_{𝑜} mPoly (R ↾_{𝑠} B) = 1_{𝑜} mPoly (R ↾_{𝑠} B)$
27		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
28		eqid	$⊢ algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) = algSc (1_{𝑜} mPoly (R ↾_{𝑠} B))$
29		1on	$⊢ 1_{𝑜} \in On$
30	29	a1i	$⊢ (R \in CRing \land X \in B) \to 1_{𝑜} \in On$
31		simpl	$⊢ (R \in CRing \land X \in B) \to R \in CRing$
32	3	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
33	6 32	syl	$⊢ (R \in CRing \land X \in B) \to B \in SubRing (R)$
34		simpr	$⊢ (R \in CRing \land X \in B) \to X \in B$
35	25 26 27 3 28 30 31 33 34	evlssca	$⊢ (R \in CRing \land X \in B) \to (1_{𝑜} eval R) (algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (X)) = (B^{1_{𝑜}}) \times \{X\}$
36	24 35	eqtrd	$⊢ (R \in CRing \land X \in B) \to (1_{𝑜} eval R) (A (X)) = (B^{1_{𝑜}}) \times \{X\}$
37	36	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\})$
38		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
39	3	fvexi	$⊢ B \in V$
40		0ex	$⊢ \emptyset \in V$
41		eqid	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
42	38 39 40 41	mapsnf1o3	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) : B \underset{1-1 onto}{⟶} B^{1_{𝑜}}$
43		f1of	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) : B \underset{1-1 onto}{⟶} B^{1_{𝑜}} \to (y \in B ⟼ 1_{𝑜} \times \{y\}) : B ⟶ B^{1_{𝑜}}$
44	42 43	mp1i	$⊢ (R \in CRing \land X \in B) \to (y \in B ⟼ 1_{𝑜} \times \{y\}) : B ⟶ B^{1_{𝑜}}$
45	41	fmpt	$⊢ \forall y \in B 1_{𝑜} \times \{y\} \in (B^{1_{𝑜}}) \leftrightarrow (y \in B ⟼ 1_{𝑜} \times \{y\}) : B ⟶ B^{1_{𝑜}}$
46	44 45	sylibr	$⊢ (R \in CRing \land X \in B) \to \forall y \in B 1_{𝑜} \times \{y\} \in (B^{1_{𝑜}})$
47		eqidd	$⊢ (R \in CRing \land X \in B) \to (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
48		fconstmpt	$⊢ (B^{1_{𝑜}}) \times \{X\} = (x \in (B^{1_{𝑜}}) ⟼ X)$
49	48	a1i	$⊢ (R \in CRing \land X \in B) \to (B^{1_{𝑜}}) \times \{X\} = (x \in (B^{1_{𝑜}}) ⟼ X)$
50		eqidd	$⊢ x = 1_{𝑜} \times \{y\} \to X = X$
51	46 47 49 50	fmptcof	$⊢ (R \in CRing \land X \in B) \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ X)$
52		fconstmpt	$⊢ B \times \{X\} = (y \in B ⟼ X)$
53	51 52	eqtr4di	$⊢ (R \in CRing \land X \in B) \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = B \times \{X\}$
54	16 37 53	3eqtrd	$⊢ (R \in CRing \land X \in B) \to O (A (X)) = B \times \{X\}$

Metamath Proof Explorer

Theorem evl1sca

Proof