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 𝐴 = ( 𝑁 Mat 𝑅 )
m2cpminv.k 𝐾 = ( Base ‘ 𝐴 )
m2cpminv.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
m2cpminv.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
m2cpminv.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion m2cpminv ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼 : 𝑆1-1-onto𝐾 𝐼 = 𝑇 ) )

Proof

Step Hyp Ref Expression
1 m2cpminv.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 m2cpminv.k 𝐾 = ( Base ‘ 𝐴 )
3 m2cpminv.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
4 m2cpminv.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
5 m2cpminv.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6 1 2 3 4 cpm2mf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆𝐾 )
7 3 5 1 2 m2cpmf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾𝑆 )
8 3 4 5 m2cpminvid2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠𝑆 ) → ( 𝑇 ‘ ( 𝐼𝑠 ) ) = 𝑠 )
9 8 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠𝑆 ) → ( 𝑇 ‘ ( 𝐼𝑠 ) ) = 𝑠 )
10 9 ralrimiva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑠𝑆 ( 𝑇 ‘ ( 𝐼𝑠 ) ) = 𝑠 )
11 4 1 2 5 m2cpminvid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑘𝐾 ) → ( 𝐼 ‘ ( 𝑇𝑘 ) ) = 𝑘 )
12 11 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑘𝐾 ) → ( 𝐼 ‘ ( 𝑇𝑘 ) ) = 𝑘 )
13 12 ralrimiva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑘𝐾 ( 𝐼 ‘ ( 𝑇𝑘 ) ) = 𝑘 )
14 6 7 10 13 2fvidf1od ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆1-1-onto𝐾 )
15 6 7 10 13 2fvidinvd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 = 𝑇 )
16 14 15 jca ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼 : 𝑆1-1-onto𝐾 𝐼 = 𝑇 ) )