pm2mpghm

Description: The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019) (Revised by AV, 6-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpfo.p	$⊢ P = {Poly}_{1} (R)$
	pm2mpfo.c	$⊢ C = N Mat P$
	pm2mpfo.b	$⊢ B = {Base}_{C}$
	pm2mpfo.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	pm2mpfo.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	pm2mpfo.x	$⊢ X = {var}_{1} (A)$
	pm2mpfo.a	$⊢ A = N Mat R$
	pm2mpfo.q	$⊢ Q = {Poly}_{1} (A)$
	pm2mpfo.l	$⊢ L = {Base}_{Q}$
	pm2mpfo.t	$⊢ T = N pMatToMatPoly R$
Assertion	pm2mpghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (C GrpHom Q)$

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpfo.c	$⊢ C = N Mat P$
3		pm2mpfo.b	$⊢ B = {Base}_{C}$
4		pm2mpfo.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		pm2mpfo.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		pm2mpfo.x	$⊢ X = {var}_{1} (A)$
7		pm2mpfo.a	$⊢ A = N Mat R$
8		pm2mpfo.q	$⊢ Q = {Poly}_{1} (A)$
9		pm2mpfo.l	$⊢ L = {Base}_{Q}$
10		pm2mpfo.t	$⊢ T = N pMatToMatPoly R$
11		eqid	$⊢ +_{C} = +_{C}$
12		eqid	$⊢ +_{Q} = +_{Q}$
13	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
14		ringgrp	$⊢ C \in Ring \to C \in Grp$
15	13 14	syl	$⊢ (N \in Fin \land R \in Ring) \to C \in Grp$
16	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
17	8	ply1ring	$⊢ A \in Ring \to Q \in Ring$
18	16 17	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Ring$
19		ringgrp	$⊢ Q \in Ring \to Q \in Grp$
20	18 19	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Grp$
21	1 2 3 4 5 6 7 8 10 9	pm2mpf	$⊢ (N \in Fin \land R \in Ring) \to T : B ⟶ L$
22		ringmnd	$⊢ C \in Ring \to C \in Mnd$
23	13 22	syl	$⊢ (N \in Fin \land R \in Ring) \to C \in Mnd$
24	23	anim1i	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to (C \in Mnd \land (a \in B \land b \in B))$
25		3anass	$⊢ (C \in Mnd \land a \in B \land b \in B) \leftrightarrow (C \in Mnd \land (a \in B \land b \in B))$
26	24 25	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to (C \in Mnd \land a \in B \land b \in B)$
27	3 11	mndcl	$⊢ (C \in Mnd \land a \in B \land b \in B) \to a +_{C} b \in B$
28	26 27	syl	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to a +_{C} b \in B$
29	2 3	decpmatval	$⊢ (a +_{C} b \in B \land k \in ℕ_{0}) \to (a +_{C} b) decompPMat k = (i \in N, j \in N ⟼ {coe}_{1} (i (a +_{C} b) j) (k))$
30	28 29	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (a +_{C} b) decompPMat k = (i \in N, j \in N ⟼ {coe}_{1} (i (a +_{C} b) j) (k))$
31		simplll	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to N \in Fin$
32		fvexd	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i a j) (k) \in V$
33		fvexd	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i b j) (k) \in V$
34		eqidd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k))$
35		eqidd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k))$
36	31 31 32 33 34 35	offval22	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) {+_{R}}_{f} (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k) +_{R} {coe}_{1} (i b j) (k))$
37		eqid	$⊢ {Base}_{R} = {Base}_{R}$
38		eqid	$⊢ {Base}_{A} = {Base}_{A}$
39		simpllr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to R \in Ring$
40		simprl	$⊢ (((N \in Fin \land R \in Ring) \land a \in B) \land (i \in N \land j \in N)) \to i \in N$
41		simprr	$⊢ (((N \in Fin \land R \in Ring) \land a \in B) \land (i \in N \land j \in N)) \to j \in N$
42	3	eleq2i	$⊢ a \in B \leftrightarrow a \in {Base}_{C}$
43	42	biimpi	$⊢ a \in B \to a \in {Base}_{C}$
44	43	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land a \in B) \land (i \in N \land j \in N)) \to a \in {Base}_{C}$
45		eqid	$⊢ {Base}_{P} = {Base}_{P}$
46	2 45	matecl	$⊢ (i \in N \land j \in N \land a \in {Base}_{C}) \to i a j \in {Base}_{P}$
47	40 41 44 46	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land a \in B) \land (i \in N \land j \in N)) \to i a j \in {Base}_{P}$
48	47	ex	$⊢ ((N \in Fin \land R \in Ring) \land a \in B) \to ((i \in N \land j \in N) \to i a j \in {Base}_{P})$
49	48	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to ((i \in N \land j \in N) \to i a j \in {Base}_{P})$
50	49	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to ((i \in N \land j \in N) \to i a j \in {Base}_{P})$
51	50	3impib	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to i a j \in {Base}_{P}$
52		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
53	52	3ad2ant1	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to k \in ℕ_{0}$
54		eqid	$⊢ {coe}_{1} (i a j) = {coe}_{1} (i a j)$
55	54 45 1 37	coe1fvalcl	$⊢ (i a j \in {Base}_{P} \land k \in ℕ_{0}) \to {coe}_{1} (i a j) (k) \in {Base}_{R}$
56	51 53 55	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i a j) (k) \in {Base}_{R}$
57	7 37 38 31 39 56	matbas2d	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) \in {Base}_{A}$
58		simprl	$⊢ (((N \in Fin \land R \in Ring) \land b \in B) \land (i \in N \land j \in N)) \to i \in N$
59		simprr	$⊢ (((N \in Fin \land R \in Ring) \land b \in B) \land (i \in N \land j \in N)) \to j \in N$
60	3	eleq2i	$⊢ b \in B \leftrightarrow b \in {Base}_{C}$
61	60	biimpi	$⊢ b \in B \to b \in {Base}_{C}$
62	61	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land b \in B) \land (i \in N \land j \in N)) \to b \in {Base}_{C}$
63	2 45	matecl	$⊢ (i \in N \land j \in N \land b \in {Base}_{C}) \to i b j \in {Base}_{P}$
64	58 59 62 63	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land b \in B) \land (i \in N \land j \in N)) \to i b j \in {Base}_{P}$
65	64	ex	$⊢ ((N \in Fin \land R \in Ring) \land b \in B) \to ((i \in N \land j \in N) \to i b j \in {Base}_{P})$
66	65	adantrl	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to ((i \in N \land j \in N) \to i b j \in {Base}_{P})$
67	66	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to ((i \in N \land j \in N) \to i b j \in {Base}_{P})$
68	67	3impib	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to i b j \in {Base}_{P}$
69		eqid	$⊢ {coe}_{1} (i b j) = {coe}_{1} (i b j)$
70	69 45 1 37	coe1fvalcl	$⊢ (i b j \in {Base}_{P} \land k \in ℕ_{0}) \to {coe}_{1} (i b j) (k) \in {Base}_{R}$
71	68 53 70	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i b j) (k) \in {Base}_{R}$
72	7 37 38 31 39 71	matbas2d	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) \in {Base}_{A}$
73		eqid	$⊢ +_{A} = +_{A}$
74		eqid	$⊢ +_{R} = +_{R}$
75	7 38 73 74	matplusg2	$⊢ ((i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) \in {Base}_{A} \land (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) \in {Base}_{A}) \to (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) +_{A} (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) {+_{R}}_{f} (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k))$
76	57 72 75	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) +_{A} (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) {+_{R}}_{f} (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k))$
77		simplr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (a \in B \land b \in B)$
78	77	anim1i	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land (i \in N \land j \in N)) \to ((a \in B \land b \in B) \land (i \in N \land j \in N))$
79	78	3impb	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to ((a \in B \land b \in B) \land (i \in N \land j \in N))$
80		eqid	$⊢ +_{P} = +_{P}$
81	2 3 11 80	matplusgcell	$⊢ ((a \in B \land b \in B) \land (i \in N \land j \in N)) \to i (a +_{C} b) j = (i a j) +_{P} (i b j)$
82	79 81	syl	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to i (a +_{C} b) j = (i a j) +_{P} (i b j)$
83	82	fveq2d	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i (a +_{C} b) j) = {coe}_{1} ((i a j) +_{P} (i b j))$
84	83	fveq1d	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i (a +_{C} b) j) (k) = {coe}_{1} ((i a j) +_{P} (i b j)) (k)$
85	39	3ad2ant1	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to R \in Ring$
86	1 45 80 74	coe1addfv	$⊢ ((R \in Ring \land i a j \in {Base}_{P} \land i b j \in {Base}_{P}) \land k \in ℕ_{0}) \to {coe}_{1} ((i a j) +_{P} (i b j)) (k) = {coe}_{1} (i a j) (k) +_{R} {coe}_{1} (i b j) (k)$
87	85 51 68 53 86	syl31anc	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} ((i a j) +_{P} (i b j)) (k) = {coe}_{1} (i a j) (k) +_{R} {coe}_{1} (i b j) (k)$
88	84 87	eqtrd	$⊢ ((((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i (a +_{C} b) j) (k) = {coe}_{1} (i a j) (k) +_{R} {coe}_{1} (i b j) (k)$
89	88	mpoeq3dva	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (a +_{C} b) j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k) +_{R} {coe}_{1} (i b j) (k))$
90	36 76 89	3eqtr4rd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (a +_{C} b) j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) +_{A} (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k))$
91	8	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
92	16 91	syl	$⊢ (N \in Fin \land R \in Ring) \to A = Scalar (Q)$
93	92	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to A = Scalar (Q)$
94	93	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to +_{A} = +_{Scalar (Q)}$
95		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to a \in B$
96	2 3	decpmatval	$⊢ (a \in B \land k \in ℕ_{0}) \to a decompPMat k = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k))$
97	95 96	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to a decompPMat k = (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k))$
98	97	eqcomd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) = a decompPMat k$
99		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to b \in B$
100	2 3	decpmatval	$⊢ (b \in B \land k \in ℕ_{0}) \to b decompPMat k = (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k))$
101	99 100	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to b decompPMat k = (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k))$
102	101	eqcomd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) = b decompPMat k$
103	94 98 102	oveq123d	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i a j) (k)) +_{A} (i \in N, j \in N ⟼ {coe}_{1} (i b j) (k)) = (a decompPMat k) +_{Scalar (Q)} (b decompPMat k)$
104	30 90 103	3eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (a +_{C} b) decompPMat k = (a decompPMat k) +_{Scalar (Q)} (b decompPMat k)$
105	104	oveq1d	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to ((a +_{C} b) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X) = ((a decompPMat k) +_{Scalar (Q)} (b decompPMat k)) \underset{˙}{} (k \underset{˙}{\times} X)$
106	8	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
107	16 106	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in LMod$
108	107	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to Q \in LMod$
109		simpl	$⊢ (a \in B \land b \in B) \to a \in B$
110	109	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to a \in B$
111	1 2 3 7 38	decpmatcl	$⊢ (R \in Ring \land a \in B \land k \in ℕ_{0}) \to a decompPMat k \in {Base}_{A}$
112	39 110 52 111	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to a decompPMat k \in {Base}_{A}$
113	92	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to Scalar (Q) = A$
114	113	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to Scalar (Q) = A$
115	114	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to {Base}_{Scalar (Q)} = {Base}_{A}$
116	112 115	eleqtrrd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to a decompPMat k \in {Base}_{Scalar (Q)}$
117		simpr	$⊢ (a \in B \land b \in B) \to b \in B$
118	117	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to b \in B$
119	1 2 3 7 38	decpmatcl	$⊢ (R \in Ring \land b \in B \land k \in ℕ_{0}) \to b decompPMat k \in {Base}_{A}$
120	39 118 52 119	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to b decompPMat k \in {Base}_{A}$
121	120 115	eleqtrrd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to b decompPMat k \in {Base}_{Scalar (Q)}$
122		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
123	122 9	mgpbas	$⊢ L = {Base}_{{mulGrp}_{Q}}$
124	122	ringmgp	$⊢ Q \in Ring \to {mulGrp}_{Q} \in Mnd$
125	18 124	syl	$⊢ (N \in Fin \land R \in Ring) \to {mulGrp}_{Q} \in Mnd$
126	125	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to {mulGrp}_{Q} \in Mnd$
127	6 8 9	vr1cl	$⊢ A \in Ring \to X \in L$
128	16 127	syl	$⊢ (N \in Fin \land R \in Ring) \to X \in L$
129	128	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to X \in L$
130	123 5 126 52 129	mulgnn0cld	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in L$
131		eqid	$⊢ Scalar (Q) = Scalar (Q)$
132		eqid	$⊢ {Base}_{Scalar (Q)} = {Base}_{Scalar (Q)}$
133		eqid	$⊢ +_{Scalar (Q)} = +_{Scalar (Q)}$
134	9 12 131 4 132 133	lmodvsdir	$⊢ (Q \in LMod \land (a decompPMat k \in {Base}_{Scalar (Q)} \land b decompPMat k \in {Base}_{Scalar (Q)} \land k \underset{˙}{\times} X \in L)) \to ((a decompPMat k) +_{Scalar (Q)} (b decompPMat k)) \underset{˙}{} (k \underset{˙}{\times} X) = ((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) +_{Q} ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
135	108 116 121 130 134	syl13anc	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to ((a decompPMat k) +_{Scalar (Q)} (b decompPMat k)) \underset{˙}{} (k \underset{˙}{\times} X) = ((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) +_{Q} ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
136	105 135	eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to ((a +_{C} b) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X) = ((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) +_{Q} ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
137	136	mpteq2dva	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to (k \in ℕ_{0} ⟼ ((a +_{C} b) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = (k \in ℕ_{0} ⟼ ((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) +_{Q} ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
138	137	oveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (((a +_{C} b) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = \underset{k \in ℕ_{0}}{\sum_{Q}} (((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) +_{Q} ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
139		eqid	$⊢ 0_{Q} = 0_{Q}$
140		ringcmn	$⊢ Q \in Ring \to Q \in CMnd$
141	18 140	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in CMnd$
142	141	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to Q \in CMnd$
143		nn0ex	$⊢ ℕ_{0} \in V$
144	143	a1i	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to ℕ_{0} \in V$
145	109	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to ((N \in Fin \land R \in Ring) \land a \in B)$
146		df-3an	$⊢ (N \in Fin \land R \in Ring \land a \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land a \in B)$
147	145 146	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to (N \in Fin \land R \in Ring \land a \in B)$
148	1 2 3 4 5 6 7 8 9	pm2mpghmlem1	$⊢ ((N \in Fin \land R \in Ring \land a \in B) \land k \in ℕ_{0}) \to (a decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X) \in L$
149	147 148	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (a decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X) \in L$
150	117	anim2i	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to ((N \in Fin \land R \in Ring) \land b \in B)$
151		df-3an	$⊢ (N \in Fin \land R \in Ring \land b \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land b \in B)$
152	150 151	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to (N \in Fin \land R \in Ring \land b \in B)$
153	1 2 3 4 5 6 7 8 9	pm2mpghmlem1	$⊢ ((N \in Fin \land R \in Ring \land b \in B) \land k \in ℕ_{0}) \to (b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X) \in L$
154	152 153	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \land k \in ℕ_{0}) \to (b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X) \in L$
155		eqidd	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to (k \in ℕ_{0} ⟼ (a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = (k \in ℕ_{0} ⟼ (a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X))$
156		eqidd	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to (k \in ℕ_{0} ⟼ (b decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = (k \in ℕ_{0} ⟼ (b decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X))$
157	1 2 3 4 5 6 7 8	pm2mpghmlem2	$⊢ (N \in Fin \land R \in Ring \land a \in B) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (a decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
158	147 157	syl	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (a decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
159	1 2 3 4 5 6 7 8	pm2mpghmlem2	$⊢ (N \in Fin \land R \in Ring \land b \in B) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
160	152 159	syl	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
161	9 139 12 142 144 149 154 155 156 158 160	gsummptfsadd	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) +_{Q} ((b decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X))) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X))) +_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((b decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)))$
162	138 161	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (((a +_{C} b) decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X))) +_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
163		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to N \in Fin$
164		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to R \in Ring$
165	1 2 3 4 5 6 7 8 10	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land a +_{C} b \in B) \to T (a +_{C} b) = \underset{k \in ℕ_{0}}{\sum_{Q}} (((a +_{C} b) decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
166	163 164 28 165	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to T (a +_{C} b) = \underset{k \in ℕ_{0}}{\sum_{Q}} (((a +_{C} b) decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
167	1 2 3 4 5 6 7 8 10	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land a \in B) \to T (a) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((a decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
168	163 164 95 167	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to T (a) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((a decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
169	1 2 3 4 5 6 7 8 10	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land b \in B) \to T (b) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
170	163 164 99 169	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to T (b) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((b decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
171	168 170	oveq12d	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to T (a) +_{Q} T (b) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((a decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X))) +_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((b decompPMat k) \underset{˙}{} (k \underset{˙}{\times} X)))$
172	162 166 171	3eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (a \in B \land b \in B)) \to T (a +_{C} b) = T (a) +_{Q} T (b)$
173	3 9 11 12 15 20 21 172	isghmd	$⊢ (N \in Fin \land R \in Ring) \to T \in (C GrpHom Q)$

Metamath Proof Explorer

Theorem pm2mpghm

Proof