Metamath Proof Explorer

Theorem m2cpmrngiso

Description: The transformation of matrices into constant polynomial matrices is a ring isomorphism. (Contributed by AV, 19-Nov-2019)

Ref Expression
Hypotheses m2cpmfo.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
m2cpmfo.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
m2cpmfo.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
m2cpmfo.k ⊢ 𝐾 = ( Base ‘ 𝐴 )
m2cpmrngiso.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
m2cpmrngiso.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
m2cpmrngiso.u ⊢ 𝑈 = ( 𝐶 ↾s 𝑆 )
Assertion m2cpmrngiso ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingIso 𝑈 ) )

Proof

Step Hyp Ref Expression
1 m2cpmfo.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 m2cpmfo.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3 m2cpmfo.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 m2cpmfo.k ⊢ 𝐾 = ( Base ‘ 𝐴 )
5 m2cpmrngiso.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
6 m2cpmrngiso.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
7 m2cpmrngiso.u ⊢ 𝑈 = ( 𝐶 ↾s 𝑆 )
8 1 2 3 4 5 6 7 m2cpmrhm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝑈 ) )
9 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10 9 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
11 1 2 3 4 m2cpmf1o ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –1-1-onto→ 𝑆 )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 1 5 6 12 cpmatpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑚 ∈ 𝑆 ) → 𝑚 ∈ ( Base ‘ 𝐶 ) )
14 13 3expia ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑚 ∈ 𝑆 → 𝑚 ∈ ( Base ‘ 𝐶 ) ) )
15 14 ssrdv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
16 7 12 ressbas2 ⊢ ( 𝑆 ⊆ ( Base ‘ 𝐶 ) → 𝑆 = ( Base ‘ 𝑈 ) )
17 15 16 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = ( Base ‘ 𝑈 ) )
18 17 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑈 ) = 𝑆 )
19 18 f1oeq3d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) ↔ 𝑇 : 𝐾 –1-1-onto→ 𝑆 ) )
20 11 19 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) )
21 10 20 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) )
22 3 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
23 10 22 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
24 1 5 6 cpmatsubgpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )
25 7 subggrp ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) → 𝑈 ∈ Grp )
26 10 24 25 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ Grp )
27 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
28 4 27 isrim ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑈 ∈ Grp ) → ( 𝑇 ∈ ( 𝐴 RingIso 𝑈 ) ↔ ( 𝑇 ∈ ( 𝐴 RingHom 𝑈 ) ∧ 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) ) ) )
29 23 26 28 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑇 ∈ ( 𝐴 RingIso 𝑈 ) ↔ ( 𝑇 ∈ ( 𝐴 RingHom 𝑈 ) ∧ 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) ) ) )
30 8 21 29 mpbir2and ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingIso 𝑈 ) )