Theorem evls1sca

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

	Ref	Expression
Hypotheses	evls1sca.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	evls1sca.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	evls1sca.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evls1sca.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evls1sca.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	evls1sca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1sca.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evls1sca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion	evls1sca	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		evls1sca.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		evls1sca.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
3		evls1sca.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evls1sca.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		evls1sca.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
6		evls1sca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
7		evls1sca.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8		evls1sca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
9		1on	⊢ 1o ∈ On
10		eqid	⊢ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 1o evalSub 𝑆 ) ‘ 𝑅 )
11		eqid	⊢ ( 1o mPoly 𝑈 ) = ( 1o mPoly 𝑈 )
12		eqid	⊢ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 1o ) )
13	10 11 3 12 4	evlsrhm	⊢ ( ( 1o ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
14	9 6 7 13	mp3an2i	⊢ ( 𝜑 → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
15		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑈 ) ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
16		eqid	⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) )
17	15 16	rhmf	⊢ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 1o mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
18	14 17	syl	⊢ ( 𝜑 → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 1o mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
19		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
20	3	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
21	7 20	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
22	2	ply1ring	⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
23	21 22	syl	⊢ ( 𝜑 → 𝑊 ∈ Ring )
24	2	ply1lmod	⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
25	21 24	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
26		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
27		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
28	5 19 23 25 26 27	asclf	⊢ ( 𝜑 → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) )
29	4	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
30	7 29	syl	⊢ ( 𝜑 → 𝑅 ⊆ 𝐵 )
31	3 4	ressbas2	⊢ ( 𝑅 ⊆ 𝐵 → 𝑅 = ( Base ‘ 𝑈 ) )
32	30 31	syl	⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
33	2	ply1sca	⊢ ( 𝑈 ∈ Ring → 𝑈 = ( Scalar ‘ 𝑊 ) )
34	21 33	syl	⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑊 ) )
35	34	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
36	32 35	eqtrd	⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
37		eqid	⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
38	2 37 27	ply1bas	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
39	38	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) ) )
40	39	eqcomd	⊢ ( 𝜑 → ( Base ‘ ( 1o mPoly 𝑈 ) ) = ( Base ‘ 𝑊 ) )
41	36 40	feq23d	⊢ ( 𝜑 → ( 𝐴 : 𝑅 ⟶ ( Base ‘ ( 1o mPoly 𝑈 ) ) ↔ 𝐴 : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) ) )
42	28 41	mpbird	⊢ ( 𝜑 → 𝐴 : 𝑅 ⟶ ( Base ‘ ( 1o mPoly 𝑈 ) ) )
43	42 8	ffvelrnd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ ( 1o mPoly 𝑈 ) ) )
44		fvco3	⊢ ( ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 1o mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ ( 1o mPoly 𝑈 ) ) ) → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
45	18 43 44	syl2anc	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
46	5	a1i	⊢ ( 𝜑 → 𝐴 = ( algSc ‘ 𝑊 ) )
47		eqid	⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
48	2 47	ply1ascl	⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ ( 1o mPoly 𝑈 ) )
49	46 48	eqtrdi	⊢ ( 𝜑 → 𝐴 = ( algSc ‘ ( 1o mPoly 𝑈 ) ) )
50	49	fveq1d	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) )
51	50	fveq2d	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) ) )
52		eqid	⊢ ( algSc ‘ ( 1o mPoly 𝑈 ) ) = ( algSc ‘ ( 1o mPoly 𝑈 ) )
53	9	a1i	⊢ ( 𝜑 → 1o ∈ On )
54	10 11 3 4 52 53 6 7 8	evlssca	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
55	51 54	eqtrd	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
56	55	fveq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) )
57		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
58		coeq1	⊢ ( 𝑥 = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
59	58	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
60	30 8	sseldd	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
61		fconst6g	⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
62	60 61	syl	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
63	4	fvexi	⊢ 𝐵 ∈ V
64	63	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
65		ovex	⊢ ( 𝐵 ↑m 1o ) ∈ V
66	65	a1i	⊢ ( 𝜑 → ( 𝐵 ↑m 1o ) ∈ V )
67	64 66	elmapd	⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↔ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 ) )
68	62 67	mpbird	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) )
69		snex	⊢ { 𝑋 } ∈ V
70	65 69	xpex	⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V
71	70	a1i	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V )
72	64	mptexd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V )
73		coexg	⊢ ( ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V ∧ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V )
74	71 72 73	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V )
75	57 59 68 74	fvmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
76		fconst6g	⊢ ( 𝑦 ∈ 𝐵 → ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 )
77	76	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 )
78	63 9	pm3.2i	⊢ ( 𝐵 ∈ V ∧ 1o ∈ On )
79	78	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐵 ∈ V ∧ 1o ∈ On ) )
80		elmapg	⊢ ( ( 𝐵 ∈ V ∧ 1o ∈ On ) → ( ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 ) )
81	79 80	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 ) )
82	77 81	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) )
83		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) )
84		fconstmpt	⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 )
85	84	a1i	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 ) )
86		eqidd	⊢ ( 𝑧 = ( 1o × { 𝑦 } ) → 𝑋 = 𝑋 )
87	82 83 85 86	fmptco	⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
88	75 87	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
89	45 56 88	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
90		elpwg	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
91	29 90	mpbird	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ∈ 𝒫 𝐵 )
92	7 91	syl	⊢ ( 𝜑 → 𝑅 ∈ 𝒫 𝐵 )
93		eqid	⊢ ( 1o evalSub 𝑆 ) = ( 1o evalSub 𝑆 )
94	1 93 4	evls1fval	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
95	6 92 94	syl2anc	⊢ ( 𝜑 → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
96	95	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) )
97		fconstmpt	⊢ ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 )
98	97	a1i	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
99	89 96 98	3eqtr4d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )