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 \in Fin \land R \in Ring) \to (I : S \underset{1-1 onto}{⟶} K \land I^{-1} = 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 \in Fin \land R \in Ring) \to I : S ⟶ K$
7	3 5 1 2	m2cpmf	$⊢ (N \in Fin \land R \in Ring) \to T : K ⟶ S$
8	3 4 5	m2cpminvid2	$⊢ (N \in Fin \land R \in Ring \land s \in S) \to T (I (s)) = s$
9	8	3expa	$⊢ ((N \in Fin \land R \in Ring) \land s \in S) \to T (I (s)) = s$
10	9	ralrimiva	$⊢ (N \in Fin \land R \in Ring) \to \forall s \in S T (I (s)) = s$
11	4 1 2 5	m2cpminvid	$⊢ (N \in Fin \land R \in Ring \land k \in K) \to I (T (k)) = k$
12	11	3expa	$⊢ ((N \in Fin \land R \in Ring) \land k \in K) \to I (T (k)) = k$
13	12	ralrimiva	$⊢ (N \in Fin \land R \in Ring) \to \forall k \in K I (T (k)) = k$
14	6 7 10 13	2fvidf1od	$⊢ (N \in Fin \land R \in Ring) \to I : S \underset{1-1 onto}{⟶} K$
15	6 7 10 13	2fvidinvd	$⊢ (N \in Fin \land R \in Ring) \to I^{-1} = T$
16	14 15	jca	$⊢ (N \in Fin \land R \in Ring) \to (I : S \underset{1-1 onto}{⟶} K \land I^{-1} = T)$