Metamath Proof Explorer

Theorem mat2pmatmhm

Description: The transformation of matrices into polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 29-Oct-2019)

Ref Expression
Hypotheses mat2pmatbas.t ⊢T=NmatToPolyMatR
mat2pmatbas.a ⊢A=NMatR
mat2pmatbas.b ⊢B=BaseA
mat2pmatbas.p ⊢P=Poly1⁡R
mat2pmatbas.c ⊢C=NMatP
mat2pmatbas0.h ⊢H=BaseC
Assertion mat2pmatmhm ⊢N∈Fin∧R∈CRing→T∈mulGrpAMndHommulGrpC

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t ⊢T=NmatToPolyMatR
2 mat2pmatbas.a ⊢A=NMatR
3 mat2pmatbas.b ⊢B=BaseA
4 mat2pmatbas.p ⊢P=Poly1⁡R
5 mat2pmatbas.c ⊢C=NMatP
6 mat2pmatbas0.h ⊢H=BaseC
7 crngring ⊢R∈CRing→R∈Ring
8 2 matring ⊢N∈Fin∧R∈Ring→A∈Ring
9 7 8 sylan2 ⊢N∈Fin∧R∈CRing→A∈Ring
10 eqid ⊢mulGrpA=mulGrpA
11 10 ringmgp ⊢A∈Ring→mulGrpA∈Mnd
12 9 11 syl ⊢N∈Fin∧R∈CRing→mulGrpA∈Mnd
13 4 ply1ring ⊢R∈Ring→P∈Ring
14 7 13 syl ⊢R∈CRing→P∈Ring
15 5 matring ⊢N∈Fin∧P∈Ring→C∈Ring
16 14 15 sylan2 ⊢N∈Fin∧R∈CRing→C∈Ring
17 eqid ⊢mulGrpC=mulGrpC
18 17 ringmgp ⊢C∈Ring→mulGrpC∈Mnd
19 16 18 syl ⊢N∈Fin∧R∈CRing→mulGrpC∈Mnd
20 1 2 3 4 5 6 mat2pmatf ⊢N∈Fin∧R∈Ring→T:B⟶H
21 7 20 sylan2 ⊢N∈Fin∧R∈CRing→T:B⟶H
22 1 2 3 4 5 6 mat2pmatmul ⊢N∈Fin∧R∈CRing→∀x∈B∀y∈BT⁡x⋅Ay=T⁡x⋅CT⁡y
23 1 2 3 4 5 6 mat2pmat1 ⊢N∈Fin∧R∈Ring→T⁡1A=1C
24 7 23 sylan2 ⊢N∈Fin∧R∈CRing→T⁡1A=1C
25 21 22 24 3jca ⊢N∈Fin∧R∈CRing→T:B⟶H∧∀x∈B∀y∈BT⁡x⋅Ay=T⁡x⋅CT⁡y∧T⁡1A=1C
26 10 3 mgpbas ⊢B=BasemulGrpA
27 17 6 mgpbas ⊢H=BasemulGrpC
28 eqid ⊢⋅A=⋅A
29 10 28 mgpplusg ⊢⋅A=+mulGrpA
30 eqid ⊢⋅C=⋅C
31 17 30 mgpplusg ⊢⋅C=+mulGrpC
32 eqid ⊢1A=1A
33 10 32 ringidval ⊢1A=0mulGrpA
34 eqid ⊢1C=1C
35 17 34 ringidval ⊢1C=0mulGrpC
36 26 27 29 31 33 35 ismhm ⊢T∈mulGrpAMndHommulGrpC↔mulGrpA∈Mnd∧mulGrpC∈Mnd∧T:B⟶H∧∀x∈B∀y∈BT⁡x⋅Ay=T⁡x⋅CT⁡y∧T⁡1A=1C
37 12 19 25 36 syl21anbrc ⊢N∈Fin∧R∈CRing→T∈mulGrpAMndHommulGrpC