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 = Poly 1 ⁡ R
m2cpmghm.c ⊢ C = N Mat P
m2cpmghm.u ⊢ U = C ↾ 𝑠 S
Assertion m2cpmghm ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ 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 = Poly 1 ⁡ R
6 m2cpmghm.c ⊢ C = N Mat P
7 m2cpmghm.u ⊢ U = C ↾ 𝑠 S
8 eqid ⊢ Base C = Base C
9 2 3 4 5 6 8 mat2pmatghm ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ A GrpHom C
10 1 5 6 cpmatsubgpmat ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ C
11 1 2 3 4 m2cpmf ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ S
12 11 frnd ⊢ N ∈ Fin ∧ R ∈ Ring → ran ⁡ T ⊆ S
13 7 resghm2b ⊢ S ∈ SubGrp ⁡ C ∧ ran ⁡ T ⊆ S → T ∈ A GrpHom C ↔ T ∈ A GrpHom U
14 13 bicomd ⊢ S ∈ SubGrp ⁡ C ∧ ran ⁡ T ⊆ S → T ∈ A GrpHom U ↔ T ∈ A GrpHom C
15 10 12 14 syl2anc ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ A GrpHom U ↔ T ∈ A GrpHom C
16 9 15 mpbird ⊢ N ∈ Fin ∧ R ∈ Ring → T ∈ A GrpHom U