Metamath Proof Explorer


Theorem m2cpminv

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

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

Proof

Step Hyp Ref Expression
1 m2cpminv.a
 |-  A = ( N Mat R )
2 m2cpminv.k
 |-  K = ( Base ` A )
3 m2cpminv.s
 |-  S = ( N ConstPolyMat R )
4 m2cpminv.i
 |-  I = ( N cPolyMatToMat R )
5 m2cpminv.t
 |-  T = ( N matToPolyMat R )
6 1 2 3 4 cpm2mf
 |-  ( ( N e. Fin /\ R e. Ring ) -> I : S --> K )
7 3 5 1 2 m2cpmf
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : K --> S )
8 3 4 5 m2cpminvid2
 |-  ( ( N e. Fin /\ R e. Ring /\ s e. S ) -> ( T ` ( I ` s ) ) = s )
9 8 3expa
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ s e. S ) -> ( T ` ( I ` s ) ) = s )
10 9 ralrimiva
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. s e. S ( T ` ( I ` s ) ) = s )
11 4 1 2 5 m2cpminvid
 |-  ( ( N e. Fin /\ R e. Ring /\ k e. K ) -> ( I ` ( T ` k ) ) = k )
12 11 3expa
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ k e. K ) -> ( I ` ( T ` k ) ) = k )
13 12 ralrimiva
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. k e. K ( I ` ( T ` k ) ) = k )
14 6 7 10 13 2fvidf1od
 |-  ( ( N e. Fin /\ R e. Ring ) -> I : S -1-1-onto-> K )
15 6 7 10 13 2fvidinvd
 |-  ( ( N e. Fin /\ R e. Ring ) -> `' I = T )
16 14 15 jca
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( I : S -1-1-onto-> K /\ `' I = T ) )