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
|- S = ( N ConstPolyMat R )
m2cpm.t
|- T = ( N matToPolyMat R )
m2cpm.a
|- A = ( N Mat R )
m2cpm.b
|- B = ( Base ` A )
m2cpmghm.p
|- P = ( Poly1 ` R )
m2cpmghm.c
|- C = ( N Mat P )
m2cpmghm.u
|- U = ( C |`s S )
Assertion m2cpmghm
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom U ) )

Proof

Step Hyp Ref Expression
1 m2cpm.s
 |-  S = ( N ConstPolyMat R )
2 m2cpm.t
 |-  T = ( N matToPolyMat R )
3 m2cpm.a
 |-  A = ( N Mat R )
4 m2cpm.b
 |-  B = ( Base ` A )
5 m2cpmghm.p
 |-  P = ( Poly1 ` R )
6 m2cpmghm.c
 |-  C = ( N Mat P )
7 m2cpmghm.u
 |-  U = ( C |`s S )
8 eqid
 |-  ( Base ` C ) = ( Base ` C )
9 2 3 4 5 6 8 mat2pmatghm
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) )
10 1 5 6 cpmatsubgpmat
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )
11 1 2 3 4 m2cpmf
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> S )
12 11 frnd
 |-  ( ( N e. Fin /\ R e. Ring ) -> ran T C_ S )
13 7 resghm2b
 |-  ( ( S e. ( SubGrp ` C ) /\ ran T C_ S ) -> ( T e. ( A GrpHom C ) <-> T e. ( A GrpHom U ) ) )
14 13 bicomd
 |-  ( ( S e. ( SubGrp ` C ) /\ ran T C_ S ) -> ( T e. ( A GrpHom U ) <-> T e. ( A GrpHom C ) ) )
15 10 12 14 syl2anc
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T e. ( A GrpHom U ) <-> T e. ( A GrpHom C ) ) )
16 9 15 mpbird
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom U ) )