Theorem pm2mpmhm

Description: The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpmhm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpmhm.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpmhm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpmhm.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	pm2mpmhm.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion	pm2mpmhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐶 ) MndHom ( mulGrp ‘ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpmhm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpmhm.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpmhm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		pm2mpmhm.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
5		pm2mpmhm.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
6	1 2	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
7		eqid	⊢ ( mulGrp ‘ 𝐶 ) = ( mulGrp ‘ 𝐶 )
8	7	ringmgp	⊢ ( 𝐶 ∈ Ring → ( mulGrp ‘ 𝐶 ) ∈ Mnd )
9	6 8	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( mulGrp ‘ 𝐶 ) ∈ Mnd )
10	3	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
11	4	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
12		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
13	12	ringmgp	⊢ ( 𝑄 ∈ Ring → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
14	10 11 13	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
15		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
16	7 15	mgpbas	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( mulGrp ‘ 𝐶 ) )
17	16	eqcomi	⊢ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) = ( Base ‘ 𝐶 )
18		eqid	⊢ ( ·𝑠 ‘ 𝑄 ) = ( ·𝑠 ‘ 𝑄 )
19		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑄 ) ) = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
20		eqid	⊢ ( var1 ‘ 𝐴 ) = ( var1 ‘ 𝐴 )
21		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
22	12 21	mgpbas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
23	22	eqcomi	⊢ ( Base ‘ ( mulGrp ‘ 𝑄 ) ) = ( Base ‘ 𝑄 )
24	1 2 17 18 19 20 3 4 5 23	pm2mpf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ⟶ ( Base ‘ ( mulGrp ‘ 𝑄 ) ) )
25	1 2 3 4 5 17	pm2mpmhmlem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ∀ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝑇 ‘ 𝑦 ) ) )
26	1 2 15 18 19 20 3 4 5	idpm2idmp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ 𝐶 ) ) = ( 1r ‘ 𝑄 ) )
27	24 25 26	3jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 : ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ⟶ ( Base ‘ ( mulGrp ‘ 𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ∀ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝑇 ‘ 𝑦 ) ) ∧ ( 𝑇 ‘ ( 1r ‘ 𝐶 ) ) = ( 1r ‘ 𝑄 ) ) )
28		eqid	⊢ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) = ( Base ‘ ( mulGrp ‘ 𝐶 ) )
29		eqid	⊢ ( Base ‘ ( mulGrp ‘ 𝑄 ) ) = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
30		eqid	⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
31	7 30	mgpplusg	⊢ ( .r ‘ 𝐶 ) = ( +g ‘ ( mulGrp ‘ 𝐶 ) )
32		eqid	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
33	12 32	mgpplusg	⊢ ( .r ‘ 𝑄 ) = ( +g ‘ ( mulGrp ‘ 𝑄 ) )
34		eqid	⊢ ( 1r ‘ 𝐶 ) = ( 1r ‘ 𝐶 )
35	7 34	ringidval	⊢ ( 1r ‘ 𝐶 ) = ( 0g ‘ ( mulGrp ‘ 𝐶 ) )
36		eqid	⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
37	12 36	ringidval	⊢ ( 1r ‘ 𝑄 ) = ( 0g ‘ ( mulGrp ‘ 𝑄 ) )
38	28 29 31 33 35 37	ismhm	⊢ ( 𝑇 ∈ ( ( mulGrp ‘ 𝐶 ) MndHom ( mulGrp ‘ 𝑄 ) ) ↔ ( ( ( mulGrp ‘ 𝐶 ) ∈ Mnd ∧ ( mulGrp ‘ 𝑄 ) ∈ Mnd ) ∧ ( 𝑇 : ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ⟶ ( Base ‘ ( mulGrp ‘ 𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ∀ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝐶 ) ) ( 𝑇 ‘ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝑇 ‘ 𝑦 ) ) ∧ ( 𝑇 ‘ ( 1r ‘ 𝐶 ) ) = ( 1r ‘ 𝑄 ) ) ) )
39	9 14 27 38	syl21anbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐶 ) MndHom ( mulGrp ‘ 𝑄 ) ) )