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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
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	1 2 3 4	m2cpmf1o	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –1-1-onto→ 𝑆 )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12	1 5 6 11	cpmatpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑚 ∈ 𝑆 ) → 𝑚 ∈ ( Base ‘ 𝐶 ) )
13	12	3expia	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑚 ∈ 𝑆 → 𝑚 ∈ ( Base ‘ 𝐶 ) ) )
14	13	ssrdv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
15	7 11	ressbas2	⊢ ( 𝑆 ⊆ ( Base ‘ 𝐶 ) → 𝑆 = ( Base ‘ 𝑈 ) )
16	14 15	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = ( Base ‘ 𝑈 ) )
17	16	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑈 ) = 𝑆 )
18	17	f1oeq3d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) ↔ 𝑇 : 𝐾 –1-1-onto→ 𝑆 ) )
19	10 18	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) )
20	9 19	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) )
21		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
22	4 21	isrim	⊢ ( 𝑇 ∈ ( 𝐴 RingIso 𝑈 ) ↔ ( 𝑇 ∈ ( 𝐴 RingHom 𝑈 ) ∧ 𝑇 : 𝐾 –1-1-onto→ ( Base ‘ 𝑈 ) ) )
23	8 20 22	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingIso 𝑈 ) )

Metamath Proof Explorer

Theorem m2cpmrngiso

Proof