Theorem mplmon2cl

Description: A scaled monomial is a polynomial. (Contributed by Stefan O'Rear, 8-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mplmon2cl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplmon2cl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3		mplmon2cl.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mplmon2cl.c	⊢ 𝐶 = ( Base ‘ 𝑅 )
5		mplmon2cl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		mplmon2cl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		mplmon2cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
8		mplmon2cl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
9		mplmon2cl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
10		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
11		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12	1 10 2 11 3 4 5 6 9 8	mplmon2	⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ) )
13	1	mpllmod	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
14	5 6 13	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ LMod )
15	1 5 6	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
17	4 16	syl5eq	⊢ ( 𝜑 → 𝐶 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
18	8 17	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
19	1 7 3 11 2 5 6 9	mplmon	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ 𝐵 )
20		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
21		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
22	7 20 10 21	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∈ 𝐵 )
23	14 18 19 22	syl3anc	⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∈ 𝐵 )
24	12 23	eqeltrrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ) ∈ 𝐵 )