Theorem m2cpmghm

Description: The transformation of matrices into constant polynomial matrices is an additive group homomorphism. (Contributed by AV, 18-Nov-2019)

	Ref	Expression
Hypotheses	m2cpm.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	m2cpm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	m2cpm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2cpm.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	m2cpmghm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	m2cpmghm.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	m2cpmghm.u	⊢ 𝑈 = ( 𝐶 ↾s 𝑆 )
Assertion	m2cpmghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		m2cpm.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		m2cpm.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3		m2cpm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		m2cpm.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
5		m2cpmghm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
6		m2cpmghm.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
7		m2cpmghm.u	⊢ 𝑈 = ( 𝐶 ↾s 𝑆 )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9	2 3 4 5 6 8	mat2pmatghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
10	1 5 6	cpmatsubgpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )
11	1 2 3 4	m2cpmf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝑆 )
12	11	frnd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ran 𝑇 ⊆ 𝑆 )
13	7	resghm2b	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ∧ ran 𝑇 ⊆ 𝑆 ) → ( 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ↔ 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) ) )
14	13	bicomd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ∧ ran 𝑇 ⊆ 𝑆 ) → ( 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) ↔ 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ) )
15	10 12 14	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) ↔ 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ) )
16	9 15	mpbird	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝑈 ) )