Metamath Proof Explorer

Theorem m2cpmmhm

Description: The transformation of matrices into constant polynomial matrices is a homomorphism of multiplicative monoids. (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 m2cpmmhm ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ mulGrp A MndHom mulGrp 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 mat2pmatmhm ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ mulGrp A MndHom mulGrp C
10 crngring ⊢ R ∈ CRing → R ∈ Ring
11 10 anim2i ⊢ N ∈ Fin ∧ R ∈ CRing → N ∈ Fin ∧ R ∈ Ring
12 1 5 6 cpmatsrgpmat ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ C
13 eqid ⊢ mulGrp C = mulGrp C
14 13 subrgsubm ⊢ S ∈ SubRing ⁡ C → S ∈ SubMnd ⁡ mulGrp C
15 11 12 14 3syl ⊢ N ∈ Fin ∧ R ∈ CRing → S ∈ SubMnd ⁡ mulGrp C
16 1 2 3 4 m2cpmf ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ S
17 frn ⊢ T : B ⟶ S → ran ⁡ T ⊆ S
18 11 16 17 3syl ⊢ N ∈ Fin ∧ R ∈ CRing → ran ⁡ T ⊆ S
19 6 ovexi ⊢ C ∈ V
20 1 ovexi ⊢ S ∈ V
21 7 13 mgpress ⊢ C ∈ V ∧ S ∈ V → mulGrp C ↾ 𝑠 S = mulGrp U
22 19 20 21 mp2an ⊢ mulGrp C ↾ 𝑠 S = mulGrp U
23 22 eqcomi ⊢ mulGrp U = mulGrp C ↾ 𝑠 S
24 23 resmhm2b ⊢ S ∈ SubMnd ⁡ mulGrp C ∧ ran ⁡ T ⊆ S → T ∈ mulGrp A MndHom mulGrp C ↔ T ∈ mulGrp A MndHom mulGrp U
25 15 18 24 syl2anc ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ mulGrp A MndHom mulGrp C ↔ T ∈ mulGrp A MndHom mulGrp U
26 9 25 mpbid ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ mulGrp A MndHom mulGrp U