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