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 โŠข ๐‘ƒ = ( 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 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) )