Theorem pmatcollpw3

Description: Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 27-Oct-2019) (Revised by AV, 4-Dec-2019) (Proof shortened by AV, 8-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatcollpw.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmatcollpw.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pmatcollpw.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
	pmatcollpw.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	pmatcollpw.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	pmatcollpw.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	pmatcollpw3.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pmatcollpw3.d	⊢ 𝐷 = ( Base ‘ 𝐴 )
Assertion	pmatcollpw3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑓 ∈ ( 𝐷 ↑m ℕ0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatcollpw.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmatcollpw.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pmatcollpw.m	⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5		pmatcollpw.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		pmatcollpw.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		pmatcollpw.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8		pmatcollpw3.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
9		pmatcollpw3.d	⊢ 𝐷 = ( Base ‘ 𝐴 )
10	1 2 3 4 5 6 7	pmatcollpw	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
11		ssid	⊢ ℕ0 ⊆ ℕ0
12		0nn0	⊢ 0 ∈ ℕ0
13	12	ne0ii	⊢ ℕ0 ≠ ∅
14	1 2 3 4 5 6 7 8 9	pmatcollpw3lem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( ℕ0 ⊆ ℕ0 ∧ ℕ0 ≠ ∅ ) ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷 ↑m ℕ0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
15	11 13 14	mpanr12	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷 ↑m ℕ0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
16	10 15	mpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑓 ∈ ( 𝐷 ↑m ℕ0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )