Metamath Proof Explorer

Theorem m2cpminv0

Description: The inverse matrix transformation applied to the zero polynomial matrix results in the zero of the matrices over the base ring of the polynomials. (Contributed by AV, 24-Nov-2019) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses m2cpminv0.a 
|- A = ( N Mat R )
m2cpminv0.i 
|- I = ( N cPolyMatToMat R )
m2cpminv0.p 
|- P = ( Poly1 ` R )
m2cpminv0.c 
|- C = ( N Mat P )
m2cpminv0.0 
|- .0. = ( 0g ` A )
m2cpminv0.z 
|- Z = ( 0g ` C )
Assertion m2cpminv0 
|- ( ( N e. Fin /\ R e. Ring ) -> ( I ` Z ) = .0. )

Proof

Step Hyp Ref Expression
1 m2cpminv0.a 
 |-  A = ( N Mat R )
2 m2cpminv0.i 
 |-  I = ( N cPolyMatToMat R )
3 m2cpminv0.p 
 |-  P = ( Poly1 ` R )
4 m2cpminv0.c 
 |-  C = ( N Mat P )
5 m2cpminv0.0 
 |-  .0. = ( 0g ` A )
6 m2cpminv0.z 
 |-  Z = ( 0g ` C )
7 eqid 
 |-  ( N matToPolyMat R ) = ( N matToPolyMat R )
8 1 fveq2i 
 |-  ( 0g ` A ) = ( 0g ` ( N Mat R ) )
9 5 8 eqtri 
 |-  .0. = ( 0g ` ( N Mat R ) )
10 4 fveq2i 
 |-  ( 0g ` C ) = ( 0g ` ( N Mat P ) )
11 6 10 eqtri 
 |-  Z = ( 0g ` ( N Mat P ) )
12 7 3 9 11 0mat2pmat 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( N matToPolyMat R ) ` .0. ) = Z )
13 12 ancoms 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( N matToPolyMat R ) ` .0. ) = Z )
14 13 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Z = ( ( N matToPolyMat R ) ` .0. ) )
15 14 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( I ` Z ) = ( I ` ( ( N matToPolyMat R ) ` .0. ) ) )
16 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
17 eqid 
 |-  ( Base ` A ) = ( Base ` A )
18 17 5 ring0cl 
 |-  ( A e. Ring -> .0. e. ( Base ` A ) )
19 16 18 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. e. ( Base ` A ) )
20 2 1 17 7 m2cpminvid 
 |-  ( ( N e. Fin /\ R e. Ring /\ .0. e. ( Base ` A ) ) -> ( I ` ( ( N matToPolyMat R ) ` .0. ) ) = .0. )
21 19 20 mpd3an3 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( I ` ( ( N matToPolyMat R ) ` .0. ) ) = .0. )
22 15 21 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( I ` Z ) = .0. )