evl1val

Description: Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	evl1fval.o	$⊢ O = {eval}_{1} (R)$
	evl1fval.q	$⊢ Q = 1_{𝑜} eval R$
	evl1fval.b	$⊢ B = {Base}_{R}$
	evl1val.m	$⊢ M = 1_{𝑜} mPoly R$
	evl1val.k	$⊢ K = {Base}_{M}$
Assertion	evl1val	$⊢ (R \in CRing \land A \in K) \to O (A) = Q (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$

Proof

Step	Hyp	Ref	Expression
1		evl1fval.o	$⊢ O = {eval}_{1} (R)$
2		evl1fval.q	$⊢ Q = 1_{𝑜} eval R$
3		evl1fval.b	$⊢ B = {Base}_{R}$
4		evl1val.m	$⊢ M = 1_{𝑜} mPoly R$
5		evl1val.k	$⊢ K = {Base}_{M}$
6	1 2 3	evl1fval	$⊢ O = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$
7	6	fveq1i	$⊢ O (A) = ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q) (A)$
8		1on	$⊢ 1_{𝑜} \in On$
9		simpl	$⊢ (R \in CRing \land A \in K) \to R \in CRing$
10		eqid	$⊢ R ↑_{𝑠} (B^{1_{𝑜}}) = R ↑_{𝑠} (B^{1_{𝑜}})$
11	2 3 4 10	evlrhm	$⊢ (1_{𝑜} \in On \land R \in CRing) \to Q \in (M RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
12	8 9 11	sylancr	$⊢ (R \in CRing \land A \in K) \to Q \in (M RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
13		eqid	$⊢ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
14	5 13	rhmf	$⊢ Q \in (M RingHom (R ↑_{𝑠} (B^{1_{𝑜}}))) \to Q : K ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
15	12 14	syl	$⊢ (R \in CRing \land A \in K) \to Q : K ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
16		fvco3	$⊢ (Q : K ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} \land A \in K) \to ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q) (A) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (Q (A))$
17	15 16	sylancom	$⊢ (R \in CRing \land A \in K) \to ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q) (A) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (Q (A))$
18	7 17	syl5eq	$⊢ (R \in CRing \land A \in K) \to O (A) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (Q (A))$
19		ffvelrn	$⊢ (Q : K ⟶ {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} \land A \in K) \to Q (A) \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
20	15 19	sylancom	$⊢ (R \in CRing \land A \in K) \to Q (A) \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
21		crngring	$⊢ R \in CRing \to R \in Ring$
22	21	adantr	$⊢ (R \in CRing \land A \in K) \to R \in Ring$
23		ovex	$⊢ B^{1_{𝑜}} \in V$
24	10 3	pwsbas	$⊢ (R \in Ring \land B^{1_{𝑜}} \in V) \to B^{(B^{1_{𝑜}})} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
25	22 23 24	sylancl	$⊢ (R \in CRing \land A \in K) \to B^{(B^{1_{𝑜}})} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
26	20 25	eleqtrrd	$⊢ (R \in CRing \land A \in K) \to Q (A) \in (B^{(B^{1_{𝑜}})})$
27		coeq1	$⊢ x = Q (A) \to x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = Q (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
28		eqid	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}))$
29		fvex	$⊢ Q (A) \in V$
30	3	fvexi	$⊢ B \in V$
31	30	mptex	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
32	29 31	coex	$⊢ Q (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
33	27 28 32	fvmpt	$⊢ Q (A) \in (B^{(B^{1_{𝑜}})}) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (Q (A)) = Q (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
34	26 33	syl	$⊢ (R \in CRing \land A \in K) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (Q (A)) = Q (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
35	18 34	eqtrd	$⊢ (R \in CRing \land A \in K) \to O (A) = Q (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$

Metamath Proof Explorer

Theorem evl1val

Proof