Theorem mplcoe2

Description: Decompose a monomial into a finite product of powers of variables. (The assumption that R is a commutative ring is not strictly necessary, because the submonoid of monomials is in the center of the multiplicative monoid of polynomials, but it simplifies the proof.) (Contributed by Mario Carneiro, 10-Jan-2015) (Proof shortened by AV, 18-Oct-2019)

	Ref	Expression
Hypotheses	mplcoe1.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplcoe1.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mplcoe1.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mplcoe1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	mplcoe1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mplcoe2.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	mplcoe2.m	⊢ ↑ = ( .g ‘ 𝐺 )
	mplcoe2.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	mplcoe2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mplcoe2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion	mplcoe2	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplcoe1.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplcoe1.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3		mplcoe1.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mplcoe1.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		mplcoe1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		mplcoe2.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
7		mplcoe2.m	⊢ ↑ = ( .g ‘ 𝐺 )
8		mplcoe2.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
9		mplcoe2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
10		mplcoe2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
12	9 11	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
13	1	mplcrng	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ CRing )
14	5 9 13	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ CRing )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → 𝑃 ∈ CRing )
16		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
17	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → 𝐼 ∈ 𝑊 )
18	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → 𝑅 ∈ Ring )
19		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → 𝑦 ∈ 𝐼 )
20	1 8 16 17 18 19	mvrcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → ( 𝑉 ‘ 𝑦 ) ∈ ( Base ‘ 𝑃 ) )
21		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → 𝑥 ∈ 𝐼 )
22	1 8 16 17 18 21	mvrcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → ( 𝑉 ‘ 𝑥 ) ∈ ( Base ‘ 𝑃 ) )
23		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
24	6 23	mgpplusg	⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝐺 )
25	24	eqcomi	⊢ ( +g ‘ 𝐺 ) = ( .r ‘ 𝑃 )
26	16 25	crngcom	⊢ ( ( 𝑃 ∈ CRing ∧ ( 𝑉 ‘ 𝑦 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑉 ‘ 𝑥 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
27	15 20 22 26	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
28	27	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
29	1 2 3 4 5 6 7 8 12 10 28	mplcoe5	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )