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	|- P = ( Poly1 ` R )
	pmatcollpw.c	|- C = ( N Mat P )
	pmatcollpw.b	|- B = ( Base ` C )
	pmatcollpw.m	|- .* = ( .s ` C )
	pmatcollpw.e	|- .^ = ( .g ` ( mulGrp ` P ) )
	pmatcollpw.x	|- X = ( var1 ` R )
	pmatcollpw.t	|- T = ( N matToPolyMat R )
	pmatcollpw3.a	|- A = ( N Mat R )
	pmatcollpw3.d	|- D = ( Base ` A )
Assertion	pmatcollpw3fi	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	|- P = ( Poly1 ` R )
2		pmatcollpw.c	|- C = ( N Mat P )
3		pmatcollpw.b	|- B = ( Base ` C )
4		pmatcollpw.m	|- .* = ( .s ` C )
5		pmatcollpw.e	|- .^ = ( .g ` ( mulGrp ` P ) )
6		pmatcollpw.x	|- X = ( var1 ` R )
7		pmatcollpw.t	|- T = ( N matToPolyMat R )
8		pmatcollpw3.a	|- A = ( N Mat R )
9		pmatcollpw3.d	|- D = ( Base ` A )
10	1 2 3 4 5 6 7	pmatcollpwfi	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
11		elnn0uz	|- ( s e. NN0 <-> s e. ( ZZ>= ` 0 ) )
12		fzn0	|- ( ( 0 ... s ) =/= (/) <-> s e. ( ZZ>= ` 0 ) )
13	11 12	sylbb2	|- ( s e. NN0 -> ( 0 ... s ) =/= (/) )
14		fz0ssnn0	|- ( 0 ... s ) C_ NN0
15	13 14	jctil	|- ( s e. NN0 -> ( ( 0 ... s ) C_ NN0 /\ ( 0 ... s ) =/= (/) ) )
16	1 2 3 4 5 6 7 8 9	pmatcollpw3lem	|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( ( 0 ... s ) C_ NN0 /\ ( 0 ... s ) =/= (/) ) ) -> ( M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
17	15 16	sylan2	|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) -> ( M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
18	17	reximdva	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN0 M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. s e. NN0 E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
19	10 18	mpd	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )