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 )