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 = N matToPolyMat R
mat2pmatbas.a ⊢ A = N Mat R
mat2pmatbas.b ⊢ B = Base A
mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
mat2pmatbas.c ⊢ C = N Mat P
mat2pmatbas0.h ⊢ H = Base C
Assertion mat2pmatmhm ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ mulGrp A MndHom mulGrp C

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t ⊢ T = N matToPolyMat R
2 mat2pmatbas.a ⊢ A = N Mat R
3 mat2pmatbas.b ⊢ B = Base A
4 mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
5 mat2pmatbas.c ⊢ C = N Mat P
6 mat2pmatbas0.h ⊢ H = Base C
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 ⊢ mulGrp A = mulGrp A
11 10 ringmgp ⊢ A ∈ Ring → mulGrp A ∈ Mnd
12 9 11 syl ⊢ N ∈ Fin ∧ R ∈ CRing → mulGrp A ∈ 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 ⊢ mulGrp C = mulGrp C
18 17 ringmgp ⊢ C ∈ Ring → mulGrp C ∈ Mnd
19 16 18 syl ⊢ N ∈ Fin ∧ R ∈ CRing → mulGrp C ∈ 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 ∈ B T ⁡ x ⋅ A y = T ⁡ x ⋅ C T ⁡ y
23 1 2 3 4 5 6 mat2pmat1 ⊢ N ∈ Fin ∧ R ∈ Ring → T ⁡ 1 A = 1 C
24 7 23 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → T ⁡ 1 A = 1 C
25 21 22 24 3jca ⊢ N ∈ Fin ∧ R ∈ CRing → T : B ⟶ H ∧ ∀ x ∈ B ∀ y ∈ B T ⁡ x ⋅ A y = T ⁡ x ⋅ C T ⁡ y ∧ T ⁡ 1 A = 1 C
26 10 3 mgpbas ⊢ B = Base mulGrp A
27 17 6 mgpbas ⊢ H = Base mulGrp C
28 eqid ⊢ ⋅ A = ⋅ A
29 10 28 mgpplusg ⊢ ⋅ A = + mulGrp A
30 eqid ⊢ ⋅ C = ⋅ C
31 17 30 mgpplusg ⊢ ⋅ C = + mulGrp C
32 eqid ⊢ 1 A = 1 A
33 10 32 ringidval ⊢ 1 A = 0 mulGrp A
34 eqid ⊢ 1 C = 1 C
35 17 34 ringidval ⊢ 1 C = 0 mulGrp C
36 26 27 29 31 33 35 ismhm ⊢ T ∈ mulGrp A MndHom mulGrp C ↔ mulGrp A ∈ Mnd ∧ mulGrp C ∈ Mnd ∧ T : B ⟶ H ∧ ∀ x ∈ B ∀ y ∈ B T ⁡ x ⋅ A y = T ⁡ x ⋅ C T ⁡ y ∧ T ⁡ 1 A = 1 C
37 12 19 25 36 syl21anbrc ⊢ N ∈ Fin ∧ R ∈ CRing → T ∈ mulGrp A MndHom mulGrp C