Theorem pmatcollpw2

Description: Write a polynomial matrix as a sum of matrices whose entries are products of variable powers and constant polynomials collecting like powers. (Contributed by AV, 3-Oct-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatcollpw1.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmatcollpw1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pmatcollpw1.m	⊢ × = ( ·𝑠 ‘ 𝑃 )
	pmatcollpw1.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	pmatcollpw1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
Assertion	pmatcollpw2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatcollpw1.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmatcollpw1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pmatcollpw1.m	⊢ × = ( ·𝑠 ‘ 𝑃 )
5		pmatcollpw1.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		pmatcollpw1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7	1 2 3 4 5 6	pmatcollpw1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
8		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
9		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
10		nn0ex	⊢ ℕ0 ∈ V
11	10	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ℕ0 ∈ V )
12	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
13	12	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
14		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15	9	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ Fin )
16	13	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑃 ∈ Ring )
17		simp1l2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
18		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
19		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
21		simp2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
22		simp3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
23		simp2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
24	23	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
25		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
26	25	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
27		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
28	24 26 27	3jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) )
29	28	3ad2ant1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) )
30	1 2 3 18 20	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
31	29 30	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
32	18 19 20 21 22 31	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
33		simp1r	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑛 ∈ ℕ0 )
34		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
35	19 1 6 4 34 5 14	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
36	17 32 33 35	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑃 ) )
37	2 14 3 15 16 36	matbas2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ∈ 𝐵 )
38	1 2 3 4 5 6	pmatcollpw2lem	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) finSupp ( 0g ‘ 𝐶 ) )
39	2 3 8 9 11 13 37 38	matgsum	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) )
40	7 39	eqtr4d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑀 decompPMat 𝑛 ) 𝑗 ) × ( 𝑛 ↑ 𝑋 ) ) ) ) ) )