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	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
Assertion	mat2pmatmhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2		mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
6		mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
7		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
8	2	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
9	7 8	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
10		eqid	⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
11	10	ringmgp	⊢ ( 𝐴 ∈ Ring → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
12	9 11	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
13	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
14	7 13	syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
15	5	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐶 ∈ Ring )
16	14 15	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ Ring )
17		eqid	⊢ ( mulGrp ‘ 𝐶 ) = ( mulGrp ‘ 𝐶 )
18	17	ringmgp	⊢ ( 𝐶 ∈ Ring → ( mulGrp ‘ 𝐶 ) ∈ Mnd )
19	16 18	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( mulGrp ‘ 𝐶 ) ∈ Mnd )
20	1 2 3 4 5 6	mat2pmatf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐻 )
21	7 20	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 : 𝐵 ⟶ 𝐻 )
22	1 2 3 4 5 6	mat2pmatmul	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) )
23	1 2 3 4 5 6	mat2pmat1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) )
24	7 23	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) )
25	21 22 24	3jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑇 : 𝐵 ⟶ 𝐻 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) ∧ ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) ) )
26	10 3	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐴 ) )
27	17 6	mgpbas	⊢ 𝐻 = ( Base ‘ ( mulGrp ‘ 𝐶 ) )
28		eqid	⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
29	10 28	mgpplusg	⊢ ( .r ‘ 𝐴 ) = ( +g ‘ ( mulGrp ‘ 𝐴 ) )
30		eqid	⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
31	17 30	mgpplusg	⊢ ( .r ‘ 𝐶 ) = ( +g ‘ ( mulGrp ‘ 𝐶 ) )
32		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
33	10 32	ringidval	⊢ ( 1r ‘ 𝐴 ) = ( 0g ‘ ( mulGrp ‘ 𝐴 ) )
34		eqid	⊢ ( 1r ‘ 𝐶 ) = ( 1r ‘ 𝐶 )
35	17 34	ringidval	⊢ ( 1r ‘ 𝐶 ) = ( 0g ‘ ( mulGrp ‘ 𝐶 ) )
36	26 27 29 31 33 35	ismhm	⊢ ( 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) ↔ ( ( ( mulGrp ‘ 𝐴 ) ∈ Mnd ∧ ( mulGrp ‘ 𝐶 ) ∈ Mnd ) ∧ ( 𝑇 : 𝐵 ⟶ 𝐻 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) ∧ ( 𝑇 ‘ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐶 ) ) ) )
37	12 19 25 36	syl21anbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) )