Metamath Proof Explorer

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 
|- 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 pmatcollpw3fi1 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN 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 8 9 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 ) ) ) ) ) )
11 df-n0 
 |-  NN0 = ( NN u. { 0 } )
12 11 rexeqi 
 |-  ( E. s e. NN0 E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> E. s e. ( NN u. { 0 } ) E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
13 rexun 
 |-  ( E. s e. ( NN u. { 0 } ) E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> ( E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) \/ E. s e. { 0 } E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
14 12 13 bitri 
 |-  ( E. s e. NN0 E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> ( E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) \/ E. s e. { 0 } E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
15 c0ex 
 |-  0 e. _V
16 oveq2 
 |-  ( s = 0 -> ( 0 ... s ) = ( 0 ... 0 ) )
17 0z 
 |-  0 e. ZZ
18 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
19 17 18 mp1i 
 |-  ( s = 0 -> ( 0 ... 0 ) = { 0 } )
20 16 19 eqtrd 
 |-  ( s = 0 -> ( 0 ... s ) = { 0 } )
21 20 oveq2d 
 |-  ( s = 0 -> ( D ^m ( 0 ... s ) ) = ( D ^m { 0 } ) )
22 20 mpteq1d 
 |-  ( s = 0 -> ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) = ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) )
23 22 oveq2d 
 |-  ( s = 0 -> ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
24 23 eqeq2d 
 |-  ( s = 0 -> ( M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
25 21 24 rexeqbidv 
 |-  ( s = 0 -> ( E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> E. f e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
26 15 25 rexsn 
 |-  ( E. s e. { 0 } E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> E. f e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )
27 1 2 3 4 5 6 7 8 9 pmatcollpw3fi1lem2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. f e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
28 27 com12 
 |-  ( E. f e. ( D ^m { 0 } ) M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
29 26 28 sylbi 
 |-  ( E. s e. { 0 } E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
30 29 jao1i 
 |-  ( ( E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) \/ E. s e. { 0 } E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
31 14 30 sylbi 
 |-  ( E. s e. NN0 E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )
32 10 31 mpcom 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. f e. ( D ^m ( 0 ... s ) ) M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) )