evls1sca

Description: Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019)

	Ref	Expression
Hypotheses	evls1sca.q	$⊢ Q = S {evalSub}_{1} R$
	evls1sca.w	$⊢ W = {Poly}_{1} (U)$
	evls1sca.u	$⊢ U = S ↾_{𝑠} R$
	evls1sca.b	$⊢ B = {Base}_{S}$
	evls1sca.a	$⊢ A = algSc (W)$
	evls1sca.s	$⊢ φ \to S \in CRing$
	evls1sca.r	$⊢ φ \to R \in SubRing (S)$
	evls1sca.x	$⊢ φ \to X \in R$
Assertion	evls1sca	$⊢ φ \to Q (A (X)) = B \times \{X\}$

Proof

Step	Hyp	Ref	Expression
1		evls1sca.q	$⊢ Q = S {evalSub}_{1} R$
2		evls1sca.w	$⊢ W = {Poly}_{1} (U)$
3		evls1sca.u	$⊢ U = S ↾_{𝑠} R$
4		evls1sca.b	$⊢ B = {Base}_{S}$
5		evls1sca.a	$⊢ A = algSc (W)$
6		evls1sca.s	$⊢ φ \to S \in CRing$
7		evls1sca.r	$⊢ φ \to R \in SubRing (S)$
8		evls1sca.x	$⊢ φ \to X \in R$
9		1on	$⊢ 1_{𝑜} \in On$
10		eqid	$⊢ (1_{𝑜} evalSub S) (R) = (1_{𝑜} evalSub S) (R)$
11		eqid	$⊢ 1_{𝑜} mPoly U = 1_{𝑜} mPoly U$
12		eqid	$⊢ S ↑_{𝑠} (B^{1_{𝑜}}) = S ↑_{𝑠} (B^{1_{𝑜}})$
13	10 11 3 12 4	evlsrhm	$⊢ (1_{𝑜} \in On \land S \in CRing \land R \in SubRing (S)) \to (1_{𝑜} evalSub S) (R) \in ((1_{𝑜} mPoly U) RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
14	9 6 7 13	mp3an2i	$⊢ φ \to (1_{𝑜} evalSub S) (R) \in ((1_{𝑜} mPoly U) RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
15		eqid	$⊢ {Base}_{(1_{𝑜} mPoly U)} = {Base}_{(1_{𝑜} mPoly U)}$
16		eqid	$⊢ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
17	15 16	rhmf	$⊢ (1_{𝑜} evalSub S) (R) \in ((1_{𝑜} mPoly U) RingHom (S ↑_{𝑠} (B^{1_{𝑜}}))) \to (1_{𝑜} evalSub S) (R) : {Base}_{(1_{𝑜} mPoly U)} ⟶ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
18	14 17	syl	$⊢ φ \to (1_{𝑜} evalSub S) (R) : {Base}_{(1_{𝑜} mPoly U)} ⟶ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
19		eqid	$⊢ Scalar (W) = Scalar (W)$
20	3	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
21	7 20	syl	$⊢ φ \to U \in Ring$
22	2	ply1ring	$⊢ U \in Ring \to W \in Ring$
23	21 22	syl	$⊢ φ \to W \in Ring$
24	2	ply1lmod	$⊢ U \in Ring \to W \in LMod$
25	21 24	syl	$⊢ φ \to W \in LMod$
26		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
27		eqid	$⊢ {Base}_{W} = {Base}_{W}$
28	5 19 23 25 26 27	asclf	$⊢ φ \to A : {Base}_{Scalar (W)} ⟶ {Base}_{W}$
29	4	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
30	7 29	syl	$⊢ φ \to R \subseteq B$
31	3 4	ressbas2	$⊢ R \subseteq B \to R = {Base}_{U}$
32	30 31	syl	$⊢ φ \to R = {Base}_{U}$
33	2	ply1sca	$⊢ U \in Ring \to U = Scalar (W)$
34	21 33	syl	$⊢ φ \to U = Scalar (W)$
35	34	fveq2d	$⊢ φ \to {Base}_{U} = {Base}_{Scalar (W)}$
36	32 35	eqtrd	$⊢ φ \to R = {Base}_{Scalar (W)}$
37		eqid	$⊢ {PwSer}_{1} (U) = {PwSer}_{1} (U)$
38	2 37 27	ply1bas	$⊢ {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
39	38	a1i	$⊢ φ \to {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
40	39	eqcomd	$⊢ φ \to {Base}_{(1_{𝑜} mPoly U)} = {Base}_{W}$
41	36 40	feq23d	$⊢ φ \to (A : R ⟶ {Base}_{(1_{𝑜} mPoly U)} \leftrightarrow A : {Base}_{Scalar (W)} ⟶ {Base}_{W})$
42	28 41	mpbird	$⊢ φ \to A : R ⟶ {Base}_{(1_{𝑜} mPoly U)}$
43	42 8	ffvelcdmd	$⊢ φ \to A (X) \in {Base}_{(1_{𝑜} mPoly U)}$
44		fvco3	$⊢ ((1_{𝑜} evalSub S) (R) : {Base}_{(1_{𝑜} mPoly U)} ⟶ {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))} \land A (X) \in {Base}_{(1_{𝑜} mPoly U)}) \to ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)) (A (X)) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) ((1_{𝑜} evalSub S) (R) (A (X)))$
45	18 43 44	syl2anc	$⊢ φ \to ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)) (A (X)) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) ((1_{𝑜} evalSub S) (R) (A (X)))$
46	5	a1i	$⊢ φ \to A = algSc (W)$
47		eqid	$⊢ algSc (W) = algSc (W)$
48	2 47	ply1ascl	$⊢ algSc (W) = algSc (1_{𝑜} mPoly U)$
49	46 48	eqtrdi	$⊢ φ \to A = algSc (1_{𝑜} mPoly U)$
50	49	fveq1d	$⊢ φ \to A (X) = algSc (1_{𝑜} mPoly U) (X)$
51	50	fveq2d	$⊢ φ \to (1_{𝑜} evalSub S) (R) (A (X)) = (1_{𝑜} evalSub S) (R) (algSc (1_{𝑜} mPoly U) (X))$
52		eqid	$⊢ algSc (1_{𝑜} mPoly U) = algSc (1_{𝑜} mPoly U)$
53	9	a1i	$⊢ φ \to 1_{𝑜} \in On$
54	10 11 3 4 52 53 6 7 8	evlssca	$⊢ φ \to (1_{𝑜} evalSub S) (R) (algSc (1_{𝑜} mPoly U) (X)) = (B^{1_{𝑜}}) \times \{X\}$
55	51 54	eqtrd	$⊢ φ \to (1_{𝑜} evalSub S) (R) (A (X)) = (B^{1_{𝑜}}) \times \{X\}$
56	55	fveq2d	$⊢ φ \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) ((1_{𝑜} evalSub S) (R) (A (X))) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) ((B^{1_{𝑜}}) \times \{X\})$
57		eqidd	$⊢ φ \to (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\}))$
58		coeq1	$⊢ x = (B^{1_{𝑜}}) \times \{X\} \to x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
59	58	adantl	$⊢ (φ \land x = (B^{1_{𝑜}}) \times \{X\}) \to x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
60	30 8	sseldd	$⊢ φ \to X \in B$
61		fconst6g	$⊢ X \in B \to ((B^{1_{𝑜}}) \times \{X\}) : B^{1_{𝑜}} ⟶ B$
62	60 61	syl	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\}) : B^{1_{𝑜}} ⟶ B$
63	4	fvexi	$⊢ B \in V$
64	63	a1i	$⊢ φ \to B \in V$
65		ovex	$⊢ B^{1_{𝑜}} \in V$
66	65	a1i	$⊢ φ \to B^{1_{𝑜}} \in V$
67	64 66	elmapd	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\} \in (B^{(B^{1_{𝑜}})}) \leftrightarrow ((B^{1_{𝑜}}) \times \{X\}) : B^{1_{𝑜}} ⟶ B)$
68	62 67	mpbird	$⊢ φ \to (B^{1_{𝑜}}) \times \{X\} \in (B^{(B^{1_{𝑜}})})$
69		snex	$⊢ \{X\} \in V$
70	65 69	xpex	$⊢ (B^{1_{𝑜}}) \times \{X\} \in V$
71	70	a1i	$⊢ φ \to (B^{1_{𝑜}}) \times \{X\} \in V$
72	64	mptexd	$⊢ φ \to (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
73		coexg	$⊢ ((B^{1_{𝑜}}) \times \{X\} \in V \land (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V) \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
74	71 72 73	syl2anc	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
75	57 59 68 74	fvmptd	$⊢ φ \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) ((B^{1_{𝑜}}) \times \{X\}) = ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
76		fconst6g	$⊢ y \in B \to (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B$
77	76	adantl	$⊢ (φ \land y \in B) \to (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B$
78	63 9	pm3.2i	$⊢ (B \in V \land 1_{𝑜} \in On)$
79	78	a1i	$⊢ (φ \land y \in B) \to (B \in V \land 1_{𝑜} \in On)$
80		elmapg	$⊢ (B \in V \land 1_{𝑜} \in On) \to (1_{𝑜} \times \{y\} \in (B^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B)$
81	79 80	syl	$⊢ (φ \land y \in B) \to (1_{𝑜} \times \{y\} \in (B^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B)$
82	77 81	mpbird	$⊢ (φ \land y \in B) \to 1_{𝑜} \times \{y\} \in (B^{1_{𝑜}})$
83		eqidd	$⊢ φ \to (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
84		fconstmpt	$⊢ (B^{1_{𝑜}}) \times \{X\} = (z \in (B^{1_{𝑜}}) ⟼ X)$
85	84	a1i	$⊢ φ \to (B^{1_{𝑜}}) \times \{X\} = (z \in (B^{1_{𝑜}}) ⟼ X)$
86		eqidd	$⊢ z = 1_{𝑜} \times \{y\} \to X = X$
87	82 83 85 86	fmptco	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ X)$
88	75 87	eqtrd	$⊢ φ \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) ((B^{1_{𝑜}}) \times \{X\}) = (y \in B ⟼ X)$
89	45 56 88	3eqtrd	$⊢ φ \to ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)) (A (X)) = (y \in B ⟼ X)$
90		elpwg	$⊢ R \in SubRing (S) \to (R \in 𝒫 B \leftrightarrow R \subseteq B)$
91	29 90	mpbird	$⊢ R \in SubRing (S) \to R \in 𝒫 B$
92	7 91	syl	$⊢ φ \to R \in 𝒫 B$
93		eqid	$⊢ 1_{𝑜} evalSub S = 1_{𝑜} evalSub S$
94	1 93 4	evls1fval	$⊢ (S \in CRing \land R \in 𝒫 B) \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)$
95	6 92 94	syl2anc	$⊢ φ \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)$
96	95	fveq1d	$⊢ φ \to Q (A (X)) = ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)) (A (X))$
97		fconstmpt	$⊢ B \times \{X\} = (y \in B ⟼ X)$
98	97	a1i	$⊢ φ \to B \times \{X\} = (y \in B ⟼ X)$
99	89 96 98	3eqtr4d	$⊢ φ \to Q (A (X)) = B \times \{X\}$

Metamath Proof Explorer

Theorem evls1sca

Proof