Theorem pmatcollpw3fi1

Description: Write a polynomial matrix (over a commutative ring) as a finite sum of (at least two) products of variable powers and constant matrices with scalar entries. (Contributed by AV, 6-Nov-2019) (Revised by AV, 4-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	pmatcollpw3fi1	⊢ ( ( 𝑁 ∈ 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 8 9	pmatcollpw3fi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )
11		df-n0	⊢ ℕ0 = ( ℕ ∪ { 0 } )
12	11	rexeqi	⊢ ( ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ↔ ∃ 𝑠 ∈ ( ℕ ∪ { 0 } ) ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )
13		rexun	⊢ ( ∃ 𝑠 ∈ ( ℕ ∪ { 0 } ) ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ↔ ( ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ∨ ∃ 𝑠 ∈ { 0 } ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
14	12 13	bitri	⊢ ( ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ↔ ( ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ∨ ∃ 𝑠 ∈ { 0 } ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
15		c0ex	⊢ 0 ∈ V
16		oveq2	⊢ ( 𝑠 = 0 → ( 0 ... 𝑠 ) = ( 0 ... 0 ) )
17		0z	⊢ 0 ∈ ℤ
18		fzsn	⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
19	17 18	mp1i	⊢ ( 𝑠 = 0 → ( 0 ... 0 ) = { 0 } )
20	16 19	eqtrd	⊢ ( 𝑠 = 0 → ( 0 ... 𝑠 ) = { 0 } )
21	20	oveq2d	⊢ ( 𝑠 = 0 → ( 𝐷 ↑m ( 0 ... 𝑠 ) ) = ( 𝐷 ↑m { 0 } ) )
22	20	mpteq1d	⊢ ( 𝑠 = 0 → ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
23	22	oveq2d	⊢ ( 𝑠 = 0 → ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )
24	23	eqeq2d	⊢ ( 𝑠 = 0 → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ↔ 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
25	21 24	rexeqbidv	⊢ ( 𝑠 = 0 → ( ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐷 ↑m { 0 } ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
26	15 25	rexsn	⊢ ( ∃ 𝑠 ∈ { 0 } ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ↔ ∃ 𝑓 ∈ ( 𝐷 ↑m { 0 } ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )
27	1 2 3 4 5 6 7 8 9	pmatcollpw3fi1lem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑓 ∈ ( 𝐷 ↑m { 0 } ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) → ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
28	27	com12	⊢ ( ∃ 𝑓 ∈ ( 𝐷 ↑m { 0 } ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
29	26 28	sylbi	⊢ ( ∃ 𝑠 ∈ { 0 } ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
30	29	jao1i	⊢ ( ( ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ∨ ∃ 𝑠 ∈ { 0 } ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
31	14 30	sylbi	⊢ ( ∃ 𝑠 ∈ ℕ0 ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )
32	10 31	mpcom	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) )