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 𝐴 = ( 𝑁 Mat 𝑅 )
m2cpminv0.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
m2cpminv0.p 𝑃 = ( Poly1𝑅 )
m2cpminv0.c 𝐶 = ( 𝑁 Mat 𝑃 )
m2cpminv0.0 0 = ( 0g𝐴 )
m2cpminv0.z 𝑍 = ( 0g𝐶 )
Assertion m2cpminv0 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼𝑍 ) = 0 )

Proof

Step Hyp Ref Expression
1 m2cpminv0.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 m2cpminv0.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
3 m2cpminv0.p 𝑃 = ( Poly1𝑅 )
4 m2cpminv0.c 𝐶 = ( 𝑁 Mat 𝑃 )
5 m2cpminv0.0 0 = ( 0g𝐴 )
6 m2cpminv0.z 𝑍 = ( 0g𝐶 )
7 eqid ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑁 matToPolyMat 𝑅 )
8 1 fveq2i ( 0g𝐴 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) )
9 5 8 eqtri 0 = ( 0g ‘ ( 𝑁 Mat 𝑅 ) )
10 4 fveq2i ( 0g𝐶 ) = ( 0g ‘ ( 𝑁 Mat 𝑃 ) )
11 6 10 eqtri 𝑍 = ( 0g ‘ ( 𝑁 Mat 𝑃 ) )
12 7 3 9 11 0mat2pmat ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 0 ) = 𝑍 )
13 12 ancoms ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 0 ) = 𝑍 )
14 13 eqcomd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑍 = ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 0 ) )
15 14 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼𝑍 ) = ( 𝐼 ‘ ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 0 ) ) )
16 1 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
17 eqid ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
18 17 5 ring0cl ( 𝐴 ∈ Ring → 0 ∈ ( Base ‘ 𝐴 ) )
19 16 18 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 0 ∈ ( Base ‘ 𝐴 ) )
20 2 1 17 7 m2cpminvid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 0 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 ‘ ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 0 ) ) = 0 )
21 19 20 mpd3an3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼 ‘ ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 0 ) ) = 0 )
22 15 21 eqtrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐼𝑍 ) = 0 )