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 ∈ Fin ∧ R ∈ Ring → I : S ⟶ 1-1 onto K ∧ 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 ∈ Fin ∧ R ∈ Ring → I : S ⟶ K
7 3 5 1 2 m2cpmf ⊢ N ∈ Fin ∧ R ∈ Ring → T : K ⟶ S
8 3 4 5 m2cpminvid2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ s ∈ S → T ⁡ I ⁡ s = s
9 8 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ s ∈ S → T ⁡ I ⁡ s = s
10 9 ralrimiva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ s ∈ S T ⁡ I ⁡ s = s
11 4 1 2 5 m2cpminvid ⊢ N ∈ Fin ∧ R ∈ Ring ∧ k ∈ K → I ⁡ T ⁡ k = k
12 11 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ k ∈ K → I ⁡ T ⁡ k = k
13 12 ralrimiva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ k ∈ K I ⁡ T ⁡ k = k
14 6 7 10 13 2fvidf1od ⊢ N ∈ Fin ∧ R ∈ Ring → I : S ⟶ 1-1 onto K
15 6 7 10 13 2fvidinvd ⊢ N ∈ Fin ∧ R ∈ Ring → I -1 = T
16 14 15 jca ⊢ N ∈ Fin ∧ R ∈ Ring → I : S ⟶ 1-1 onto K ∧ I -1 = T