Theorem mplmon2mul

Description: Product of scaled monomials. (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	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mplmon2mul.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mplmon2mul.t	⊢ ∙ = ( .r ‘ 𝑃 )
	mplmon2mul.u	⊢ · = ( .r ‘ 𝑅 )
	mplmon2mul.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	mplmon2mul.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
	mplmon2mul.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
	mplmon2mul.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
Assertion	mplmon2mul	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 𝐹 , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 𝐺 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 𝐹 · 𝐺 ) , 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		mplmon2mul.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7		mplmon2mul.t	⊢ ∙ = ( .r ‘ 𝑃 )
8		mplmon2mul.u	⊢ · = ( .r ‘ 𝑅 )
9		mplmon2mul.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
10		mplmon2mul.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11		mplmon2mul.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
12		mplmon2mul.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
13	1	mplassa	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ AssAlg )
14	5 6 13	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ AssAlg )
15	1 5 6	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
17	4 16	eqtrid	⊢ ( 𝜑 → 𝐶 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
18	11 17	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
19		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
21		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22	6 21	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
23	1 19 3 20 2 5 22 9	mplmon	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) )
24		assalmod	⊢ ( 𝑃 ∈ AssAlg → 𝑃 ∈ LMod )
25	14 24	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
26	12 17	eleqtrd	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
27	1 19 3 20 2 5 22 10	mplmon	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) )
28		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
29		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
30		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
31	19 28 29 30	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∈ ( Base ‘ 𝑃 ) )
32	25 26 27 31	syl3anc	⊢ ( 𝜑 → ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∈ ( Base ‘ 𝑃 ) )
33	19 28 30 29 7	assaass	⊢ ( ( 𝑃 ∈ AssAlg ∧ ( 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) = ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) ) )
34	14 18 23 32 33	syl13anc	⊢ ( 𝜑 → ( ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) = ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) ) )
35	19 28 30 29 7	assaassr	⊢ ( ( 𝑃 ∈ AssAlg ∧ ( 𝐺 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) = ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) )
36	14 26 23 27 35	syl13anc	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) = ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) )
37	36	oveq2d	⊢ ( 𝜑 → ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) ) = ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) ) )
38	1 19 3 20 2 5 22 9 7 10	mplmonmul	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) )
39	38	oveq2d	⊢ ( 𝜑 → ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) = ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
40	39	oveq2d	⊢ ( 𝜑 → ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) ) = ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) )
41	2	psrbagaddcl	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( 𝑋 ∘f + 𝑌 ) ∈ 𝐷 )
42	9 10 41	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∘f + 𝑌 ) ∈ 𝐷 )
43	1 19 3 20 2 5 22 42	mplmon	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) )
44		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑃 ) ) = ( .r ‘ ( Scalar ‘ 𝑃 ) )
45	19 28 29 30 44	lmodvsass	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝐺 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝐹 ( .r ‘ ( Scalar ‘ 𝑃 ) ) 𝐺 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) )
46	25 18 26 43 45	syl13anc	⊢ ( 𝜑 → ( ( 𝐹 ( .r ‘ ( Scalar ‘ 𝑃 ) ) 𝐺 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) )
47	15	fveq2d	⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑃 ) ) )
48	8 47	eqtr2id	⊢ ( 𝜑 → ( .r ‘ ( Scalar ‘ 𝑃 ) ) = · )
49	48	oveqd	⊢ ( 𝜑 → ( 𝐹 ( .r ‘ ( Scalar ‘ 𝑃 ) ) 𝐺 ) = ( 𝐹 · 𝐺 ) )
50	49	oveq1d	⊢ ( 𝜑 → ( ( 𝐹 ( .r ‘ ( Scalar ‘ 𝑃 ) ) 𝐺 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( ( 𝐹 · 𝐺 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
51	40 46 50	3eqtr2d	⊢ ( 𝜑 → ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) ) = ( ( 𝐹 · 𝐺 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
52	34 37 51	3eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) = ( ( 𝐹 · 𝐺 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
53	1 29 2 20 3 4 5 22 9 11	mplmon2	⊢ ( 𝜑 → ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 𝐹 , 0 ) ) )
54	1 29 2 20 3 4 5 22 10 12	mplmon2	⊢ ( 𝜑 → ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 𝐺 , 0 ) ) )
55	53 54	oveq12d	⊢ ( 𝜑 → ( ( 𝐹 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∙ ( 𝐺 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 𝐹 , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 𝐺 , 0 ) ) ) )
56	4 8	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 · 𝐺 ) ∈ 𝐶 )
57	22 11 12 56	syl3anc	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐶 )
58	1 29 2 20 3 4 5 22 42 57	mplmon2	⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 𝐹 · 𝐺 ) , 0 ) ) )
59	52 55 58	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 𝐹 , 0 ) ) ∙ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 𝐺 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , ( 𝐹 · 𝐺 ) , 0 ) ) )