evls1val

Description: Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019)

	Ref	Expression
Hypotheses	evls1fval.q	$⊢ Q = S {evalSub}_{1} R$
	evls1fval.e	$⊢ E = 1_{𝑜} evalSub S$
	evls1fval.b	$⊢ B = {Base}_{S}$
	evls1val.m	$⊢ M = 1_{𝑜} mPoly (S ↾_{𝑠} R)$
	evls1val.k	$⊢ K = {Base}_{M}$
Assertion	evls1val	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to Q (A) = E (R) (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$

Proof

Step	Hyp	Ref	Expression
1		evls1fval.q	$⊢ Q = S {evalSub}_{1} R$
2		evls1fval.e	$⊢ E = 1_{𝑜} evalSub S$
3		evls1fval.b	$⊢ B = {Base}_{S}$
4		evls1val.m	$⊢ M = 1_{𝑜} mPoly (S ↾_{𝑠} R)$
5		evls1val.k	$⊢ K = {Base}_{M}$
6	3	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
7	6	adantl	$⊢ (S \in CRing \land R \in SubRing (S)) \to R \subseteq B$
8		elpwg	$⊢ R \in SubRing (S) \to (R \in 𝒫 B \leftrightarrow R \subseteq B)$
9	8	adantl	$⊢ (S \in CRing \land R \in SubRing (S)) \to (R \in 𝒫 B \leftrightarrow R \subseteq B)$
10	7 9	mpbird	$⊢ (S \in CRing \land R \in SubRing (S)) \to R \in 𝒫 B$
11	1 2 3	evls1fval	$⊢ (S \in CRing \land R \in 𝒫 B) \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$
12	10 11	syldan	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$
13	12	fveq1d	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q (A) = ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)) (A)$
14	13	3adant3	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to Q (A) = ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)) (A)$
15		1on	$⊢ 1_{𝑜} \in On$
16		simp1	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to S \in CRing$
17		simp2	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to R \in SubRing (S)$
18	2	fveq1i	$⊢ E (R) = (1_{𝑜} evalSub S) (R)$
19		eqid	$⊢ S ↾_{𝑠} R = S ↾_{𝑠} R$
20		eqid	$⊢ S ↑_{𝑠} (B^{1_{𝑜}}) = S ↑_{𝑠} (B^{1_{𝑜}})$
21	18 4 19 20 3	evlsrhm	$⊢ (1_{𝑜} \in On \land S \in CRing \land R \in SubRing (S)) \to E (R) \in (M RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
22	15 16 17 21	mp3an2i	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to E (R) \in (M RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
23		eqid	$⊢ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
24	5 23	rhmf	$⊢ E (R) \in (M RingHom (S ↑_{𝑠} (B^{1_{𝑜}}))) \to E (R) : K ⟶ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
25	22 24	syl	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to E (R) : K ⟶ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
26		simp3	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to A \in K$
27		fvco3	$⊢ (E (R) : K ⟶ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))} \land A \in K) \to ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)) (A) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (E (R) (A))$
28	25 26 27	syl2anc	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)) (A) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (E (R) (A))$
29	25 26	ffvelrnd	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to E (R) (A) \in {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
30		ovex	$⊢ B^{1_{𝑜}} \in V$
31	20 3	pwsbas	$⊢ (S \in CRing \land B^{1_{𝑜}} \in V) \to B^{(B^{1_{𝑜}})} = {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
32	16 30 31	sylancl	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to B^{(B^{1_{𝑜}})} = {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
33	29 32	eleqtrrd	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to E (R) (A) \in (B^{(B^{1_{𝑜}})})$
34		coeq1	$⊢ x = E (R) (A) \to x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = E (R) (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
35		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\}))$
36		fvex	$⊢ E (R) (A) \in V$
37	3	fvexi	$⊢ B \in V$
38	37	mptex	$⊢ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
39	36 38	coex	$⊢ E (R) (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
40	34 35 39	fvmpt	$⊢ E (R) (A) \in (B^{(B^{1_{𝑜}})}) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (E (R) (A)) = E (R) (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
41	33 40	syl	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) (E (R) (A)) = E (R) (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
42	14 28 41	3eqtrd	$⊢ (S \in CRing \land R \in SubRing (S) \land A \in K) \to Q (A) = E (R) (A) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$

Metamath Proof Explorer

Theorem evls1val

Proof