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 )