Theorem m2cpmf1o

Description: The matrix transformation is a 1-1 function from the matrices onto the constant polynomial matrices. (Contributed by AV, 19-Nov-2019)

	Ref	Expression
Hypotheses	m2cpmfo.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	m2cpmfo.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	m2cpmfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2cpmfo.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
Assertion	m2cpmf1o	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –1-1-onto→ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		m2cpmfo.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		m2cpmfo.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3		m2cpmfo.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		m2cpmfo.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
5	1 2 3 4	m2cpmf1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –1-1→ 𝑆 )
6	1 2 3 4	m2cpmfo	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –onto→ 𝑆 )
7		df-f1o	⊢ ( 𝑇 : 𝐾 –1-1-onto→ 𝑆 ↔ ( 𝑇 : 𝐾 –1-1→ 𝑆 ∧ 𝑇 : 𝐾 –onto→ 𝑆 ) )
8	5 6 7	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐾 –1-1-onto→ 𝑆 )