Theorem m2cpmf1

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

	Ref	Expression
Hypotheses	m2cpm.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	m2cpm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	m2cpm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2cpm.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	m2cpmf1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		m2cpm.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		m2cpm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3		m2cpm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		m2cpm.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
5		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
6		eqid	⊢ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
7		eqid	⊢ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
8	2 3 4 5 6 7	mat2pmatf1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
9	1 2 3 4	m2cpmf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝑆 )
10	9	frnd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ran 𝑇 ⊆ 𝑆 )
11		f1ssr	⊢ ( ( 𝑇 : 𝐵 –1-1→ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ∧ ran 𝑇 ⊆ 𝑆 ) → 𝑇 : 𝐵 –1-1→ 𝑆 )
12	8 10 11	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝑆 )