Metamath Proof Explorer

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 ) ) )