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	2 27	ply1bas	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
38	37	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) ) )
39	38	eqcomd	⊢ ( 𝜑 → ( Base ‘ ( 1o mPoly 𝑈 ) ) = ( Base ‘ 𝑊 ) )
40	36 39	feq23d	⊢ ( 𝜑 → ( 𝐴 : 𝑅 ⟶ ( Base ‘ ( 1o mPoly 𝑈 ) ) ↔ 𝐴 : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) ) )
41	28 40	mpbird	⊢ ( 𝜑 → 𝐴 : 𝑅 ⟶ ( Base ‘ ( 1o mPoly 𝑈 ) ) )
42	41 8	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ ( 1o mPoly 𝑈 ) ) )
43		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 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
44	18 42 43	syl2anc	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
45	5	a1i	⊢ ( 𝜑 → 𝐴 = ( algSc ‘ 𝑊 ) )
46		eqid	⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
47	2 46	ply1ascl	⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ ( 1o mPoly 𝑈 ) )
48	45 47	eqtrdi	⊢ ( 𝜑 → 𝐴 = ( algSc ‘ ( 1o mPoly 𝑈 ) ) )
49	48	fveq1d	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) )
50	49	fveq2d	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) ) )
51		eqid	⊢ ( algSc ‘ ( 1o mPoly 𝑈 ) ) = ( algSc ‘ ( 1o mPoly 𝑈 ) )
52	9	a1i	⊢ ( 𝜑 → 1o ∈ On )
53	10 11 3 4 51 52 6 7 8	evlssca	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly 𝑈 ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
54	50 53	eqtrd	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
55	54	fveq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) )
56		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
57		coeq1	⊢ ( 𝑥 = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
58	57	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
59	30 8	sseldd	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
60		fconst6g	⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
61	59 60	syl	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
62	4	fvexi	⊢ 𝐵 ∈ V
63	62	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
64		ovex	⊢ ( 𝐵 ↑m 1o ) ∈ V
65	64	a1i	⊢ ( 𝜑 → ( 𝐵 ↑m 1o ) ∈ V )
66	63 65	elmapd	⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↔ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) : ( 𝐵 ↑m 1o ) ⟶ 𝐵 ) )
67	61 66	mpbird	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) )
68		snex	⊢ { 𝑋 } ∈ V
69	64 68	xpex	⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V
70	69	a1i	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V )
71	63	mptexd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V )
72		coexg	⊢ ( ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∈ V ∧ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V )
73	70 71 72	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V )
74	56 58 67 73	fvmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
75		fconst6g	⊢ ( 𝑦 ∈ 𝐵 → ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 )
76	75	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 )
77	62 9	pm3.2i	⊢ ( 𝐵 ∈ V ∧ 1o ∈ On )
78	77	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐵 ∈ V ∧ 1o ∈ On ) )
79		elmapg	⊢ ( ( 𝐵 ∈ V ∧ 1o ∈ On ) → ( ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 ) )
80	78 79	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 1o × { 𝑦 } ) : 1o ⟶ 𝐵 ) )
81	76 80	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) )
82		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) )
83		fconstmpt	⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 )
84	83	a1i	⊢ ( 𝜑 → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑧 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 ) )
85		eqidd	⊢ ( 𝑧 = ( 1o × { 𝑦 } ) → 𝑋 = 𝑋 )
86	81 82 84 85	fmptco	⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
87	74 86	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
88	44 55 87	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
89		elpwg	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
90	29 89	mpbird	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ∈ 𝒫 𝐵 )
91	7 90	syl	⊢ ( 𝜑 → 𝑅 ∈ 𝒫 𝐵 )
92		eqid	⊢ ( 1o evalSub 𝑆 ) = ( 1o evalSub 𝑆 )
93	1 92 4	evls1fval	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
94	6 91 93	syl2anc	⊢ ( 𝜑 → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
95	94	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) )
96		fconstmpt	⊢ ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 )
97	96	a1i	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
98	88 95 97	3eqtr4d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )