Metamath Proof Explorer

Theorem cpm2mf

Description: The inverse matrix transformation is a function from the constant polynomial matrices to the matrices over the base ring of the polynomials. (Contributed by AV, 24-Nov-2019) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses cpm2mf.a 
|- A = ( N Mat R )
cpm2mf.k 
|- K = ( Base ` A )
cpm2mf.s 
|- S = ( N ConstPolyMat R )
cpm2mf.i 
|- I = ( N cPolyMatToMat R )
Assertion cpm2mf 
|- ( ( N e. Fin /\ R e. Ring ) -> I : S --> K )

Proof

Step Hyp Ref Expression
1 cpm2mf.a 
 |-  A = ( N Mat R )
2 cpm2mf.k 
 |-  K = ( Base ` A )
3 cpm2mf.s 
 |-  S = ( N ConstPolyMat R )
4 cpm2mf.i 
 |-  I = ( N cPolyMatToMat R )
5 4 3 cpm2mfval 
 |-  ( ( N e. Fin /\ R e. Ring ) -> I = ( m e. S |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> N e. Fin )
8 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> R e. Ring )
9 eqid 
 |-  ( N Mat ( Poly1 ` R ) ) = ( N Mat ( Poly1 ` R ) )
10 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
11 eqid 
 |-  ( Base ` ( N Mat ( Poly1 ` R ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
12 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> x e. N )
13 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> y e. N )
14 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
15 3 14 9 11 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ m e. S ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
16 15 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
17 16 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
18 9 10 11 12 13 17 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> ( x m y ) e. ( Base ` ( Poly1 ` R ) ) )
19 0nn0 
 |-  0 e. NN0
20 eqid 
 |-  ( coe1 ` ( x m y ) ) = ( coe1 ` ( x m y ) )
21 20 10 14 6 coe1fvalcl 
 |-  ( ( ( x m y ) e. ( Base ` ( Poly1 ` R ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( x m y ) ) ` 0 ) e. ( Base ` R ) )
22 18 19 21 sylancl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> ( ( coe1 ` ( x m y ) ) ` 0 ) e. ( Base ` R ) )
23 1 6 2 7 8 22 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) e. K )
24 5 23 fmpt3d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> I : S --> K )