mat2pmatghm

Description: The transformation of matrices into polynomial matrices is an additive group homomorphism. (Contributed by AV, 28-Oct-2019) (Proof shortened by AV, 28-Nov-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	mat2pmatghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom 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		eqid	$⊢ +_{A} = +_{A}$
8		eqid	$⊢ +_{C} = +_{C}$
9	2	matgrp	$⊢ (N \in Fin \land R \in Ring) \to A \in Grp$
10	4 5	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
11		ringgrp	$⊢ C \in Ring \to C \in Grp$
12	10 11	syl	$⊢ (N \in Fin \land R \in Ring) \to C \in Grp$
13	1 2 3 4 5 6	mat2pmatf	$⊢ (N \in Fin \land R \in Ring) \to T : B ⟶ H$
14		eqid	$⊢ {Base}_{P} = {Base}_{P}$
15		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
16	15	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to N \in Fin$
17	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
18	17	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to P \in Ring$
19		simp1lr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to R \in Ring$
20		eqid	$⊢ {Base}_{R} = {Base}_{R}$
21		simp2	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i \in N$
22		simp3	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to j \in N$
23		simp1rl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to x \in B$
24	2 20 3 21 22 23	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i x j \in {Base}_{R}$
25		eqid	$⊢ algSc (P) = algSc (P)$
26	4 25 20 14	ply1sclcl	$⊢ (R \in Ring \land i x j \in {Base}_{R}) \to algSc (P) (i x j) \in {Base}_{P}$
27	19 24 26	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i x j) \in {Base}_{P}$
28	5 14 6 16 18 27	matbas2d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i x j)) \in H$
29		simp1rr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to y \in B$
30	2 20 3 21 22 29	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i y j \in {Base}_{R}$
31	4 25 20 14	ply1sclcl	$⊢ (R \in Ring \land i y j \in {Base}_{R}) \to algSc (P) (i y j) \in {Base}_{P}$
32	19 30 31	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i y j) \in {Base}_{P}$
33	5 14 6 16 18 32	matbas2d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i y j)) \in H$
34		eqid	$⊢ +_{P} = +_{P}$
35	5 6 8 34	matplusg2	$⊢ ((i \in N, j \in N ⟼ algSc (P) (i x j)) \in H \land (i \in N, j \in N ⟼ algSc (P) (i y j)) \in H) \to (i \in N, j \in N ⟼ algSc (P) (i x j)) +_{C} (i \in N, j \in N ⟼ algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i x j)) {+_{P}}_{f} (i \in N, j \in N ⟼ algSc (P) (i y j))$
36	28 33 35	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i x j)) +_{C} (i \in N, j \in N ⟼ algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i x j)) {+_{P}}_{f} (i \in N, j \in N ⟼ algSc (P) (i y j))$
37		fvexd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i x j) \in V$
38		fvexd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i y j) \in V$
39		eqidd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i x j)) = (i \in N, j \in N ⟼ algSc (P) (i x j))$
40		eqidd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i y j))$
41	16 16 37 38 39 40	offval22	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i x j)) {+_{P}}_{f} (i \in N, j \in N ⟼ algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i x j) +_{P} algSc (P) (i y j))$
42		simpr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (x \in B \land y \in B)$
43	42	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to (x \in B \land y \in B)$
44		3simpc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to (i \in N \land j \in N)$
45		eqid	$⊢ +_{R} = +_{R}$
46	2 3 7 45	matplusgcell	$⊢ ((x \in B \land y \in B) \land (i \in N \land j \in N)) \to i (x +_{A} y) j = (i x j) +_{R} (i y j)$
47	43 44 46	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i (x +_{A} y) j = (i x j) +_{R} (i y j)$
48	4	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
49	48	adantl	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (P)$
50	49	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to +_{R} = +_{Scalar (P)}$
51	50	oveqd	$⊢ (N \in Fin \land R \in Ring) \to (i x j) +_{R} (i y j) = (i x j) +_{Scalar (P)} (i y j)$
52	51	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i x j) +_{R} (i y j) = (i x j) +_{Scalar (P)} (i y j)$
53	52	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to (i x j) +_{R} (i y j) = (i x j) +_{Scalar (P)} (i y j)$
54	47 53	eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i (x +_{A} y) j = (i x j) +_{Scalar (P)} (i y j)$
55	54	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i (x +_{A} y) j) = algSc (P) ((i x j) +_{Scalar (P)} (i y j))$
56		eqid	$⊢ Scalar (P) = Scalar (P)$
57	18	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to P \in Ring$
58	4	ply1lmod	$⊢ R \in Ring \to P \in LMod$
59	58	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to P \in LMod$
60	59	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to P \in LMod$
61	25 56 57 60	asclghm	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) \in (Scalar (P) GrpHom P)$
62	49	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to Scalar (P) = R$
63	62	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{Scalar (P)} = {Base}_{R}$
64	63	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (i x j \in {Base}_{Scalar (P)} \leftrightarrow i x j \in {Base}_{R})$
65	64	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i x j \in {Base}_{Scalar (P)} \leftrightarrow i x j \in {Base}_{R})$
66	65	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to (i x j \in {Base}_{Scalar (P)} \leftrightarrow i x j \in {Base}_{R})$
67	24 66	mpbird	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i x j \in {Base}_{Scalar (P)}$
68	63	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (i y j \in {Base}_{Scalar (P)} \leftrightarrow i y j \in {Base}_{R})$
69	68	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i y j \in {Base}_{Scalar (P)} \leftrightarrow i y j \in {Base}_{R})$
70	69	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to (i y j \in {Base}_{Scalar (P)} \leftrightarrow i y j \in {Base}_{R})$
71	30 70	mpbird	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i y j \in {Base}_{Scalar (P)}$
72		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
73		eqid	$⊢ +_{Scalar (P)} = +_{Scalar (P)}$
74	72 73 34	ghmlin	$⊢ (algSc (P) \in (Scalar (P) GrpHom P) \land i x j \in {Base}_{Scalar (P)} \land i y j \in {Base}_{Scalar (P)}) \to algSc (P) ((i x j) +_{Scalar (P)} (i y j)) = algSc (P) (i x j) +_{P} algSc (P) (i y j)$
75	61 67 71 74	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) ((i x j) +_{Scalar (P)} (i y j)) = algSc (P) (i x j) +_{P} algSc (P) (i y j)$
76	55 75	eqtr2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i x j) +_{P} algSc (P) (i y j) = algSc (P) (i (x +_{A} y) j)$
77	76	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i x j) +_{P} algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i (x +_{A} y) j))$
78	41 77	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i x j)) {+_{P}}_{f} (i \in N, j \in N ⟼ algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i (x +_{A} y) j))$
79	36 78	eqtr2d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i (x +_{A} y) j)) = (i \in N, j \in N ⟼ algSc (P) (i x j)) +_{C} (i \in N, j \in N ⟼ algSc (P) (i y j))$
80		simpl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in Ring)$
81	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
82		ringmnd	$⊢ A \in Ring \to A \in Mnd$
83	81 82	syl	$⊢ (N \in Fin \land R \in Ring) \to A \in Mnd$
84	83	anim1i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (A \in Mnd \land (x \in B \land y \in B))$
85		3anass	$⊢ (A \in Mnd \land x \in B \land y \in B) \leftrightarrow (A \in Mnd \land (x \in B \land y \in B))$
86	84 85	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (A \in Mnd \land x \in B \land y \in B)$
87	3 7	mndcl	$⊢ (A \in Mnd \land x \in B \land y \in B) \to x +_{A} y \in B$
88	86 87	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to x +_{A} y \in B$
89		df-3an	$⊢ (N \in Fin \land R \in Ring \land x +_{A} y \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land x +_{A} y \in B)$
90	80 88 89	sylanbrc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in Ring \land x +_{A} y \in B)$
91	1 2 3 4 25	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land x +_{A} y \in B) \to T (x +_{A} y) = (i \in N, j \in N ⟼ algSc (P) (i (x +_{A} y) j))$
92	90 91	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x +_{A} y) = (i \in N, j \in N ⟼ algSc (P) (i (x +_{A} y) j))$
93		simpl	$⊢ (x \in B \land y \in B) \to x \in B$
94	93	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to ((N \in Fin \land R \in Ring) \land x \in B)$
95		df-3an	$⊢ (N \in Fin \land R \in Ring \land x \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land x \in B)$
96	94 95	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in Ring \land x \in B)$
97	1 2 3 4 25	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land x \in B) \to T (x) = (i \in N, j \in N ⟼ algSc (P) (i x j))$
98	96 97	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x) = (i \in N, j \in N ⟼ algSc (P) (i x j))$
99		simpr	$⊢ (x \in B \land y \in B) \to y \in B$
100	99	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to ((N \in Fin \land R \in Ring) \land y \in B)$
101		df-3an	$⊢ (N \in Fin \land R \in Ring \land y \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land y \in B)$
102	100 101	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in Ring \land y \in B)$
103	1 2 3 4 25	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land y \in B) \to T (y) = (i \in N, j \in N ⟼ algSc (P) (i y j))$
104	102 103	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (y) = (i \in N, j \in N ⟼ algSc (P) (i y j))$
105	98 104	oveq12d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x) +_{C} T (y) = (i \in N, j \in N ⟼ algSc (P) (i x j)) +_{C} (i \in N, j \in N ⟼ algSc (P) (i y j))$
106	79 92 105	3eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x +_{A} y) = T (x) +_{C} T (y)$
107	3 6 7 8 9 12 13 106	isghmd	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom C)$

Metamath Proof Explorer

Theorem mat2pmatghm

Proof