Theorem pmatcollpw3fi

Description: Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-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	pmatcollpw3fi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐷 ↑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	pmatcollpwfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
11		elnn0uz	⊢ ( 𝑠 ∈ ℕ0 ↔ 𝑠 ∈ ( ℤ≥ ‘ 0 ) )
12		fzn0	⊢ ( ( 0 ... 𝑠 ) ≠ ∅ ↔ 𝑠 ∈ ( ℤ≥ ‘ 0 ) )
13	11 12	sylbb2	⊢ ( 𝑠 ∈ ℕ0 → ( 0 ... 𝑠 ) ≠ ∅ )
14		fz0ssnn0	⊢ ( 0 ... 𝑠 ) ⊆ ℕ0
15	13 14	jctil	⊢ ( 𝑠 ∈ ℕ0 → ( ( 0 ... 𝑠 ) ⊆ ℕ0 ∧ ( 0 ... 𝑠 ) ≠ ∅ ) )
16	1 2 3 4 5 6 7 8 9	pmatcollpw3lem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( ( 0 ... 𝑠 ) ⊆ ℕ0 ∧ ( 0 ... 𝑠 ) ≠ ∅ ) ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
17	15 16	sylan2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
18	17	reximdva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ0 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
19	10 18	mpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )