Metamath Proof Explorer


Theorem cpm2mf

Description: The inverse matrix transformation is a function from the constant polynomial matrices to the matrices over the base ring of the polynomials. (Contributed by AV, 24-Nov-2019) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses cpm2mf.a 𝐴 = ( 𝑁 Mat 𝑅 )
cpm2mf.k 𝐾 = ( Base ‘ 𝐴 )
cpm2mf.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpm2mf.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
Assertion cpm2mf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆𝐾 )

Proof

Step Hyp Ref Expression
1 cpm2mf.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 cpm2mf.k 𝐾 = ( Base ‘ 𝐴 )
3 cpm2mf.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
4 cpm2mf.i 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
5 4 3 cpm2mfval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 = ( 𝑚𝑆 ↦ ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
6 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 simpll ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) → 𝑁 ∈ Fin )
8 simplr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) → 𝑅 ∈ Ring )
9 eqid ( 𝑁 Mat ( Poly1𝑅 ) ) = ( 𝑁 Mat ( Poly1𝑅 ) )
10 eqid ( Base ‘ ( Poly1𝑅 ) ) = ( Base ‘ ( Poly1𝑅 ) )
11 eqid ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) )
12 simp2 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) ∧ 𝑥𝑁𝑦𝑁 ) → 𝑥𝑁 )
13 simp3 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) ∧ 𝑥𝑁𝑦𝑁 ) → 𝑦𝑁 )
14 eqid ( Poly1𝑅 ) = ( Poly1𝑅 )
15 3 14 9 11 cpmatpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑚𝑆 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) )
16 15 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) )
17 16 3ad2ant1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) ∧ 𝑥𝑁𝑦𝑁 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) )
18 9 10 11 12 13 17 matecld ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) ∧ 𝑥𝑁𝑦𝑁 ) → ( 𝑥 𝑚 𝑦 ) ∈ ( Base ‘ ( Poly1𝑅 ) ) )
19 0nn0 0 ∈ ℕ0
20 eqid ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) = ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) )
21 20 10 14 6 coe1fvalcl ( ( ( 𝑥 𝑚 𝑦 ) ∈ ( Base ‘ ( Poly1𝑅 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
22 18 19 21 sylancl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) ∧ 𝑥𝑁𝑦𝑁 ) → ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
23 1 6 2 7 8 22 matbas2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚𝑆 ) → ( 𝑥𝑁 , 𝑦𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ∈ 𝐾 )
24 5 23 fmpt3d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆𝐾 )