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 ) )