Metamath Proof Explorer

Theorem mat2pmatbas

Description: The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 1-Aug-2019)

Ref Expression
Hypotheses mat2pmatbas.t 
|- T = ( N matToPolyMat R )
mat2pmatbas.a 
|- A = ( N Mat R )
mat2pmatbas.b 
|- B = ( Base ` A )
mat2pmatbas.p 
|- P = ( Poly1 ` R )
mat2pmatbas.c 
|- C = ( N Mat P )
Assertion mat2pmatbas 
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` C ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 
 |-  T = ( N matToPolyMat R )
2 mat2pmatbas.a 
 |-  A = ( N Mat R )
3 mat2pmatbas.b 
 |-  B = ( Base ` A )
4 mat2pmatbas.p 
 |-  P = ( Poly1 ` R )
5 mat2pmatbas.c 
 |-  C = ( N Mat P )
6 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
7 1 2 3 4 6 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) = ( x e. N , y e. N |-> ( ( algSc ` P ) ` ( x M y ) ) ) )
8 eqid 
 |-  ( Base ` P ) = ( Base ` P )
9 eqid 
 |-  ( Base ` C ) = ( Base ` C )
10 simp1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> N e. Fin )
11 4 fvexi 
 |-  P e. _V
12 11 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. _V )
13 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
14 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 14 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. Ring )
16 15 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> P e. Ring )
17 4 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
18 17 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. LMod )
19 18 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> P e. LMod )
20 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
21 6 13 16 19 20 8 asclf 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> ( algSc ` P ) : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) )
22 4 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
23 22 fveq2d 
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
24 23 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
25 24 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
26 25 feq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> ( ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) <-> ( algSc ` P ) : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) ) )
27 21 26 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> ( algSc ` P ) : ( Base ` R ) --> ( Base ` P ) )
28 simp2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> x e. N )
29 simp3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> y e. N )
30 3 eleq2i 
 |-  ( M e. B <-> M e. ( Base ` A ) )
31 30 biimpi 
 |-  ( M e. B -> M e. ( Base ` A ) )
32 31 3ad2ant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M e. ( Base ` A ) )
33 32 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> M e. ( Base ` A ) )
34 eqid 
 |-  ( Base ` R ) = ( Base ` R )
35 2 34 matecl 
 |-  ( ( x e. N /\ y e. N /\ M e. ( Base ` A ) ) -> ( x M y ) e. ( Base ` R ) )
36 28 29 33 35 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> ( x M y ) e. ( Base ` R ) )
37 27 36 ffvelcdmd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ x e. N /\ y e. N ) -> ( ( algSc ` P ) ` ( x M y ) ) e. ( Base ` P ) )
38 5 8 9 10 12 37 matbas2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( x e. N , y e. N |-> ( ( algSc ` P ) ` ( x M y ) ) ) e. ( Base ` C ) )
39 7 38 eqeltrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` C ) )