Theorem evlssca

Description: Polynomial evaluation maps scalars to constant functions. (Contributed by Stefan O'Rear, 13-Mar-2015) (Proof shortened by AV, 18-Sep-2021)

	Ref	Expression
Hypotheses	evlssca.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlssca.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
	evlssca.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlssca.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evlssca.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	evlssca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlssca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlssca.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlssca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion	evlssca	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		evlssca.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlssca.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
3		evlssca.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evlssca.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		evlssca.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
6		evlssca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		evlssca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
8		evlssca.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9		evlssca.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
10		eqid	⊢ ( 𝐼 mVar 𝑈 ) = ( 𝐼 mVar 𝑈 )
11		eqid	⊢ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
12		eqid	⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
13		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) )
14	1 2 10 3 11 4 5 12 13	evlsval2	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) ∧ ( ( 𝑄 ∘ 𝐴 ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑄 ∘ ( 𝐼 mVar 𝑈 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) ) ) ) )
15	6 7 8 14	syl3anc	⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) ∧ ( ( 𝑄 ∘ 𝐴 ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑄 ∘ ( 𝐼 mVar 𝑈 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) ) ) ) )
16	15	simprld	⊢ ( 𝜑 → ( 𝑄 ∘ 𝐴 ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) )
17	16	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ∘ 𝐴 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 𝑋 ) )
18		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
19		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20	3	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
21	8 20	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
22	2 18 19 5 6 21	mplasclf	⊢ ( 𝜑 → 𝐴 : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑊 ) )
23	4	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
24	3 4	ressbas2	⊢ ( 𝑅 ⊆ 𝐵 → 𝑅 = ( Base ‘ 𝑈 ) )
25	8 23 24	3syl	⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
26	25	feq2d	⊢ ( 𝜑 → ( 𝐴 : 𝑅 ⟶ ( Base ‘ 𝑊 ) ↔ 𝐴 : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑊 ) ) )
27	22 26	mpbird	⊢ ( 𝜑 → 𝐴 : 𝑅 ⟶ ( Base ‘ 𝑊 ) )
28		fvco3	⊢ ( ( 𝐴 : 𝑅 ⟶ ( Base ‘ 𝑊 ) ∧ 𝑋 ∈ 𝑅 ) → ( ( 𝑄 ∘ 𝐴 ) ‘ 𝑋 ) = ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) )
29	27 9 28	syl2anc	⊢ ( 𝜑 → ( ( 𝑄 ∘ 𝐴 ) ‘ 𝑋 ) = ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) )
30		sneq	⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
31	30	xpeq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
32		ovex	⊢ ( 𝐵 ↑m 𝐼 ) ∈ V
33		snex	⊢ { 𝑋 } ∈ V
34	32 33	xpex	⊢ ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ∈ V
35	31 12 34	fvmpt	⊢ ( 𝑋 ∈ 𝑅 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 𝑋 ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
36	9 35	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 𝑋 ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
37	17 29 36	3eqtr3d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )