Metamath Proof Explorer

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	\|- 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	pmatcollpw3	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. f e. ( D ^m NN0 ) M = ( C gsum ( n e. NN0 \|-> ( ( 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	pmatcollpw	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M = ( C gsum ( n e. NN0 \|-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
11		ssid	\|- NN0 C_ NN0
12		0nn0	\|- 0 e. NN0
13	12	ne0ii	\|- NN0 =/= (/)
14	1 2 3 4 5 6 7 8 9	pmatcollpw3lem	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( NN0 C_ NN0 /\ NN0 =/= (/) ) ) -> ( M = ( C gsum ( n e. NN0 \|-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. f e. ( D ^m NN0 ) M = ( C gsum ( n e. NN0 \|-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
15	11 13 14	mpanr12	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( M = ( C gsum ( n e. NN0 \|-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. f e. ( D ^m NN0 ) M = ( C gsum ( n e. NN0 \|-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
16	10 15	mpd	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. f e. ( D ^m NN0 ) M = ( C gsum ( n e. NN0 \|-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )