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	2 27	ply1bas	$⊢ {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
38	37	a1i	$⊢ φ \to {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
39	38	eqcomd	$⊢ φ \to {Base}_{(1_{𝑜} mPoly U)} = {Base}_{W}$
40	36 39	feq23d	$⊢ φ \to (A : R ⟶ {Base}_{(1_{𝑜} mPoly U)} \leftrightarrow A : {Base}_{Scalar (W)} ⟶ {Base}_{W})$
41	28 40	mpbird	$⊢ φ \to A : R ⟶ {Base}_{(1_{𝑜} mPoly U)}$
42	41 8	ffvelcdmd	$⊢ φ \to A (X) \in {Base}_{(1_{𝑜} mPoly U)}$
43		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)))$
44	18 42 43	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)))$
45	5	a1i	$⊢ φ \to A = algSc (W)$
46		eqid	$⊢ algSc (W) = algSc (W)$
47	2 46	ply1ascl	$⊢ algSc (W) = algSc (1_{𝑜} mPoly U)$
48	45 47	eqtrdi	$⊢ φ \to A = algSc (1_{𝑜} mPoly U)$
49	48	fveq1d	$⊢ φ \to A (X) = algSc (1_{𝑜} mPoly U) (X)$
50	49	fveq2d	$⊢ φ \to (1_{𝑜} evalSub S) (R) (A (X)) = (1_{𝑜} evalSub S) (R) (algSc (1_{𝑜} mPoly U) (X))$
51		eqid	$⊢ algSc (1_{𝑜} mPoly U) = algSc (1_{𝑜} mPoly U)$
52	9	a1i	$⊢ φ \to 1_{𝑜} \in On$
53	10 11 3 4 51 52 6 7 8	evlssca	$⊢ φ \to (1_{𝑜} evalSub S) (R) (algSc (1_{𝑜} mPoly U) (X)) = (B^{1_{𝑜}}) \times \{X\}$
54	50 53	eqtrd	$⊢ φ \to (1_{𝑜} evalSub S) (R) (A (X)) = (B^{1_{𝑜}}) \times \{X\}$
55	54	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\})$
56		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\}))$
57		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\})$
58	57	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\})$
59	30 8	sseldd	$⊢ φ \to X \in B$
60		fconst6g	$⊢ X \in B \to ((B^{1_{𝑜}}) \times \{X\}) : B^{1_{𝑜}} ⟶ B$
61	59 60	syl	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\}) : B^{1_{𝑜}} ⟶ B$
62	4	fvexi	$⊢ B \in V$
63	62	a1i	$⊢ φ \to B \in V$
64		ovex	$⊢ B^{1_{𝑜}} \in V$
65	64	a1i	$⊢ φ \to B^{1_{𝑜}} \in V$
66	63 65	elmapd	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\} \in (B^{(B^{1_{𝑜}})}) \leftrightarrow ((B^{1_{𝑜}}) \times \{X\}) : B^{1_{𝑜}} ⟶ B)$
67	61 66	mpbird	$⊢ φ \to (B^{1_{𝑜}}) \times \{X\} \in (B^{(B^{1_{𝑜}})})$
68		snex	$⊢ \{X\} \in V$
69	64 68	xpex	$⊢ (B^{1_{𝑜}}) \times \{X\} \in V$
70	69	a1i	$⊢ φ \to (B^{1_{𝑜}}) \times \{X\} \in V$
71	63	mptexd	$⊢ φ \to (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
72		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$
73	70 71 72	syl2anc	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) \in V$
74	56 58 67 73	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\})$
75		fconst6g	$⊢ y \in B \to (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B$
76	75	adantl	$⊢ (φ \land y \in B) \to (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B$
77	62 9	pm3.2i	$⊢ (B \in V \land 1_{𝑜} \in On)$
78	77	a1i	$⊢ (φ \land y \in B) \to (B \in V \land 1_{𝑜} \in On)$
79		elmapg	$⊢ (B \in V \land 1_{𝑜} \in On) \to (1_{𝑜} \times \{y\} \in (B^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B)$
80	78 79	syl	$⊢ (φ \land y \in B) \to (1_{𝑜} \times \{y\} \in (B^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{y\}) : 1_{𝑜} ⟶ B)$
81	76 80	mpbird	$⊢ (φ \land y \in B) \to 1_{𝑜} \times \{y\} \in (B^{1_{𝑜}})$
82		eqidd	$⊢ φ \to (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
83		fconstmpt	$⊢ (B^{1_{𝑜}}) \times \{X\} = (z \in (B^{1_{𝑜}}) ⟼ X)$
84	83	a1i	$⊢ φ \to (B^{1_{𝑜}}) \times \{X\} = (z \in (B^{1_{𝑜}}) ⟼ X)$
85		eqidd	$⊢ z = 1_{𝑜} \times \{y\} \to X = X$
86	81 82 84 85	fmptco	$⊢ φ \to ((B^{1_{𝑜}}) \times \{X\}) \circ (y \in B ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ X)$
87	74 86	eqtrd	$⊢ φ \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) ((B^{1_{𝑜}}) \times \{X\}) = (y \in B ⟼ X)$
88	44 55 87	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)$
89		elpwg	$⊢ R \in SubRing (S) \to (R \in 𝒫 B \leftrightarrow R \subseteq B)$
90	29 89	mpbird	$⊢ R \in SubRing (S) \to R \in 𝒫 B$
91	7 90	syl	$⊢ φ \to R \in 𝒫 B$
92		eqid	$⊢ 1_{𝑜} evalSub S = 1_{𝑜} evalSub S$
93	1 92 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)$
94	6 91 93	syl2anc	$⊢ φ \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)$
95	94	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))$
96		fconstmpt	$⊢ B \times \{X\} = (y \in B ⟼ X)$
97	96	a1i	$⊢ φ \to B \times \{X\} = (y \in B ⟼ X)$
98	88 95 97	3eqtr4d	$⊢ φ \to Q (A (X)) = B \times \{X\}$

Metamath Proof Explorer

Theorem evls1sca

Proof