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 ) → 𝐼 : 𝑆 ⟶ 𝐾 )