Metamath Proof Explorer


Theorem m2cpminvid

Description: The inverse transformation applied to the transformation of a matrix over a ring R results in the matrix itself. (Contributed by AV, 12-Nov-2019) (Revised by AV, 13-Dec-2019)

Ref Expression
Hypotheses m2cpminvid.i I=NcPolyMatToMatR
m2cpminvid.a A=NMatR
m2cpminvid.k K=BaseA
m2cpminvid.t T=NmatToPolyMatR
Assertion m2cpminvid NFinRRingMKITM=M

Proof

Step Hyp Ref Expression
1 m2cpminvid.i I=NcPolyMatToMatR
2 m2cpminvid.a A=NMatR
3 m2cpminvid.k K=BaseA
4 m2cpminvid.t T=NmatToPolyMatR
5 eqid NConstPolyMatR=NConstPolyMatR
6 5 4 2 3 m2cpm NFinRRingMKTMNConstPolyMatR
7 1 5 cpm2mval NFinRRingTMNConstPolyMatRITM=xN,yNcoe1xTMy0
8 6 7 syld3an3 NFinRRingMKITM=xN,yNcoe1xTMy0
9 eqid Poly1R=Poly1R
10 eqid algScPoly1R=algScPoly1R
11 4 2 3 9 10 mat2pmatvalel NFinRRingMKxNyNxTMy=algScPoly1RxMy
12 11 3impb NFinRRingMKxNyNxTMy=algScPoly1RxMy
13 12 fveq2d NFinRRingMKxNyNcoe1xTMy=coe1algScPoly1RxMy
14 13 fveq1d NFinRRingMKxNyNcoe1xTMy0=coe1algScPoly1RxMy0
15 simp12 NFinRRingMKxNyNRRing
16 eqid BaseR=BaseR
17 simp2 NFinRRingMKxNyNxN
18 simp3 NFinRRingMKxNyNyN
19 simp13 NFinRRingMKxNyNMK
20 2 16 3 17 18 19 matecld NFinRRingMKxNyNxMyBaseR
21 9 10 16 ply1sclid RRingxMyBaseRxMy=coe1algScPoly1RxMy0
22 15 20 21 syl2anc NFinRRingMKxNyNxMy=coe1algScPoly1RxMy0
23 14 22 eqtr4d NFinRRingMKxNyNcoe1xTMy0=xMy
24 23 mpoeq3dva NFinRRingMKxN,yNcoe1xTMy0=xN,yNxMy
25 eqidd NFinRRingMKiNjNxN,yNxMy=xN,yNxMy
26 oveq12 x=iy=jxMy=iMj
27 26 adantl NFinRRingMKiNjNx=iy=jxMy=iMj
28 simprl NFinRRingMKiNjNiN
29 simprr NFinRRingMKiNjNjN
30 ovexd NFinRRingMKiNjNiMjV
31 25 27 28 29 30 ovmpod NFinRRingMKiNjNixN,yNxMyj=iMj
32 31 ralrimivva NFinRRingMKiNjNixN,yNxMyj=iMj
33 simp1 NFinRRingMKNFin
34 simp2 NFinRRingMKRRing
35 2 16 3 33 34 20 matbas2d NFinRRingMKxN,yNxMyK
36 simp3 NFinRRingMKMK
37 2 3 eqmat xN,yNxMyKMKxN,yNxMy=MiNjNixN,yNxMyj=iMj
38 35 36 37 syl2anc NFinRRingMKxN,yNxMy=MiNjNixN,yNxMyj=iMj
39 32 38 mpbird NFinRRingMKxN,yNxMy=M
40 8 24 39 3eqtrd NFinRRingMKITM=M