Metamath Proof Explorer

Theorem mplmon2

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

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

Proof

Step Hyp Ref Expression
1 mplmon2.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplmon2.v ⊢ · = ( ·𝑠 ‘ 𝑃 )
3 mplmon2.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
4 mplmon2.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 mplmon2.z ⊢ 0 = ( 0g ‘ 𝑅 )
6 mplmon2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
7 mplmon2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
8 mplmon2.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 mplmon2.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
10 mplmon2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 1 11 5 4 3 7 8 9 mplmon ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 1 , 0 ) ) ∈ ( Base ‘ 𝑃 ) )
14 1 2 6 11 12 3 10 13 mplvsca ⊢ ( 𝜑 → ( 𝑋 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 1 , 0 ) ) ) = ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 1 , 0 ) ) ) )
15 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
16 3 15 rabex2 ⊢ 𝐷 ∈ V
17 16 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
18 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑋 ∈ 𝐵 )
19 4 fvexi ⊢ 1 ∈ V
20 5 fvexi ⊢ 0 ∈ V
21 19 20 ifex ⊢ if ( 𝑦 = 𝐾 , 1 , 0 ) ∈ V
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 = 𝐾 , 1 , 0 ) ∈ V )
23 fconstmpt ⊢ ( 𝐷 × { 𝑋 } ) = ( 𝑦 ∈ 𝐷 ↦ 𝑋 )
24 23 a1i ⊢ ( 𝜑 → ( 𝐷 × { 𝑋 } ) = ( 𝑦 ∈ 𝐷 ↦ 𝑋 ) )
25 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 1 , 0 ) ) )
26 17 18 22 24 25 offval2 ⊢ ( 𝜑 → ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = 𝐾 , 1 , 0 ) ) ) )
27 oveq2 ⊢ ( 1 = if ( 𝑦 = 𝐾 , 1 , 0 ) → ( 𝑋 ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = 𝐾 , 1 , 0 ) ) )
28 27 eqeq1d ⊢ ( 1 = if ( 𝑦 = 𝐾 , 1 , 0 ) → ( ( 𝑋 ( .r ‘ 𝑅 ) 1 ) = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ↔ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = 𝐾 , 1 , 0 ) ) = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ) )
29 oveq2 ⊢ ( 0 = if ( 𝑦 = 𝐾 , 1 , 0 ) → ( 𝑋 ( .r ‘ 𝑅 ) 0 ) = ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = 𝐾 , 1 , 0 ) ) )
30 29 eqeq1d ⊢ ( 0 = if ( 𝑦 = 𝐾 , 1 , 0 ) → ( ( 𝑋 ( .r ‘ 𝑅 ) 0 ) = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ↔ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = 𝐾 , 1 , 0 ) ) = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ) )
31 6 12 4 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) 1 ) = 𝑋 )
32 8 10 31 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) 1 ) = 𝑋 )
33 iftrue ⊢ ( 𝑦 = 𝐾 → if ( 𝑦 = 𝐾 , 𝑋 , 0 ) = 𝑋 )
34 33 eqcomd ⊢ ( 𝑦 = 𝐾 → 𝑋 = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) )
35 32 34 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐾 ) → ( 𝑋 ( .r ‘ 𝑅 ) 1 ) = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) )
36 6 12 5 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) 0 ) = 0 )
37 8 10 36 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) 0 ) = 0 )
38 iffalse ⊢ ( ¬ 𝑦 = 𝐾 → if ( 𝑦 = 𝐾 , 𝑋 , 0 ) = 0 )
39 38 eqcomd ⊢ ( ¬ 𝑦 = 𝐾 → 0 = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) )
40 37 39 sylan9eq ⊢ ( ( 𝜑 ∧ ¬ 𝑦 = 𝐾 ) → ( 𝑋 ( .r ‘ 𝑅 ) 0 ) = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) )
41 28 30 35 40 ifbothda ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = 𝐾 , 1 , 0 ) ) = if ( 𝑦 = 𝐾 , 𝑋 , 0 ) )
42 41 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = 𝐾 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ) )
43 14 26 42 3eqtrd ⊢ ( 𝜑 → ( 𝑋 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝐾 , 𝑋 , 0 ) ) )