Metamath Proof Explorer

Theorem m2cpmf

Description: The matrix transformation is a function from the matrices to the constant polynomial matrices. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses m2cpm.s 
|- S = ( N ConstPolyMat R )
m2cpm.t 
|- T = ( N matToPolyMat R )
m2cpm.a 
|- A = ( N Mat R )
m2cpm.b 
|- B = ( Base ` A )
Assertion m2cpmf 
|- ( ( N e. Fin /\ R e. Ring ) -> T : B --> S )

Proof

Step Hyp Ref Expression
1 m2cpm.s 
 |-  S = ( N ConstPolyMat R )
2 m2cpm.t 
 |-  T = ( N matToPolyMat R )
3 m2cpm.a 
 |-  A = ( N Mat R )
4 m2cpm.b 
 |-  B = ( Base ` A )
5 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
6 5 5 jca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ N e. Fin ) )
7 6 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) -> ( N e. Fin /\ N e. Fin ) )
8 mpoexga 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( i m j ) ) ) e. _V )
9 7 8 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) -> ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( i m j ) ) ) e. _V )
10 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
11 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
12 2 3 4 10 11 mat2pmatfval 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T = ( m e. B |-> ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( i m j ) ) ) ) )
13 1 2 3 4 m2cpm 
 |-  ( ( N e. Fin /\ R e. Ring /\ b e. B ) -> ( T ` b ) e. S )
14 13 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) -> ( T ` b ) e. S )
15 9 12 14 fmpt2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> S )