Theorem mplascl

Description: Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015)

	Ref	Expression
Hypotheses	mplascl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplascl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mplascl.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mplascl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mplascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	mplascl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mplascl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mplascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	mplascl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplascl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplascl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3		mplascl.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mplascl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
5		mplascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
6		mplascl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7		mplascl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		mplascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9	1 6 7	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
10	9	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
11	4 10	eqtrid	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
12	8 11	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
13		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
14		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
15		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
16		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
17	5 13 14 15 16	asclval	⊢ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
18	12 17	syl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
19		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20	1 2 3 19 16 6 7	mpl1	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) )
21	20	oveq2d	⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
22	2	psrbag0	⊢ ( 𝐼 ∈ 𝑊 → ( 𝐼 × { 0 } ) ∈ 𝐷 )
23	6 22	syl	⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐷 )
24	1 15 2 19 3 4 6 7 23 8	mplmon2	⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )
25	18 21 24	3eqtrd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )