Metamath Proof Explorer


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 𝑈 ) )