This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 5 6 mpllmodd ⊢ ( 𝜑 → 𝑃 ∈ LMod )
14 1 5 6 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
15 14 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
16 4 15 eqtrid ⊢ ( 𝜑 → 𝐶 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
17 8 16 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
18 1 7 3 11 2 5 6 9 mplmon ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ 𝐵 )
19 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
20 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
21 7 19 10 20 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∈ 𝐵 )
22 13 17 18 21 syl3anc ⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , ( 1r ‘ 𝑅 ) , 0 ) ) ) ∈ 𝐵 )
23 12 22 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ) ∈ 𝐵 )