Metamath Proof Explorer

Theorem mat2pmatscmxcl

Description: A transformed matrix multiplied with a power of the variable of a polynomial is a polynomial matrix. (Contributed by AV, 6-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses mat2pmatscmxcl.a 
|- A = ( N Mat R )
mat2pmatscmxcl.k 
|- K = ( Base ` A )
mat2pmatscmxcl.t 
|- T = ( N matToPolyMat R )
mat2pmatscmxcl.p 
|- P = ( Poly1 ` R )
mat2pmatscmxcl.c 
|- C = ( N Mat P )
mat2pmatscmxcl.b 
|- B = ( Base ` C )
mat2pmatscmxcl.m 
|- .* = ( .s ` C )
mat2pmatscmxcl.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
mat2pmatscmxcl.x 
|- X = ( var1 ` R )
Assertion mat2pmatscmxcl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( ( L .^ X ) .* ( T ` M ) ) e. B )

Proof

Step Hyp Ref Expression
1 mat2pmatscmxcl.a 
 |-  A = ( N Mat R )
2 mat2pmatscmxcl.k 
 |-  K = ( Base ` A )
3 mat2pmatscmxcl.t 
 |-  T = ( N matToPolyMat R )
4 mat2pmatscmxcl.p 
 |-  P = ( Poly1 ` R )
5 mat2pmatscmxcl.c 
 |-  C = ( N Mat P )
6 mat2pmatscmxcl.b 
 |-  B = ( Base ` C )
7 mat2pmatscmxcl.m 
 |-  .* = ( .s ` C )
8 mat2pmatscmxcl.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
9 mat2pmatscmxcl.x 
 |-  X = ( var1 ` R )
10 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> N e. Fin )
11 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
12 11 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> P e. Ring )
13 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
14 eqid 
 |-  ( Base ` P ) = ( Base ` P )
15 4 9 13 8 14 ply1moncl 
 |-  ( ( R e. Ring /\ L e. NN0 ) -> ( L .^ X ) e. ( Base ` P ) )
16 15 ad2ant2l 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( L .^ X ) e. ( Base ` P ) )
17 simpl 
 |-  ( ( M e. K /\ L e. NN0 ) -> M e. K )
18 17 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ M e. K ) )
19 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) <-> ( ( N e. Fin /\ R e. Ring ) /\ M e. K ) )
20 18 19 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( N e. Fin /\ R e. Ring /\ M e. K ) )
21 3 1 2 4 5 6 mat2pmatbas0 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( T ` M ) e. B )
22 20 21 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( T ` M ) e. B )
23 14 5 6 7 matvscl 
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( ( L .^ X ) e. ( Base ` P ) /\ ( T ` M ) e. B ) ) -> ( ( L .^ X ) .* ( T ` M ) ) e. B )
24 10 12 16 22 23 syl22anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( ( L .^ X ) .* ( T ` M ) ) e. B )