pm2mpmhmlem2

Description: Lemma 2 for pm2mpmhm . (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpmhm.p	$⊢ P = {Poly}_{1} (R)$
	pm2mpmhm.c	$⊢ C = N Mat P$
	pm2mpmhm.a	$⊢ A = N Mat R$
	pm2mpmhm.q	$⊢ Q = {Poly}_{1} (A)$
	pm2mpmhm.t	$⊢ T = N pMatToMatPoly R$
	pm2mpmhm.b	$⊢ B = {Base}_{C}$
Assertion	pm2mpmhmlem2	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in B \forall y \in B T (x \cdot_{C} y) = T (x) \cdot_{Q} T (y)$

Proof

Step	Hyp	Ref	Expression
1		pm2mpmhm.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpmhm.c	$⊢ C = N Mat P$
3		pm2mpmhm.a	$⊢ A = N Mat R$
4		pm2mpmhm.q	$⊢ Q = {Poly}_{1} (A)$
5		pm2mpmhm.t	$⊢ T = N pMatToMatPoly R$
6		pm2mpmhm.b	$⊢ B = {Base}_{C}$
7		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to N \in Fin$
8		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to R \in Ring$
9	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
10	9	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to C \in Ring$
11		simpl	$⊢ (x \in B \land y \in B) \to x \in B$
12	11	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to x \in B$
13		simpr	$⊢ (x \in B \land y \in B) \to y \in B$
14	13	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to y \in B$
15		eqid	$⊢ \cdot_{C} = \cdot_{C}$
16	6 15	ringcl	$⊢ (C \in Ring \land x \in B \land y \in B) \to x \cdot_{C} y \in B$
17	10 12 14 16	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to x \cdot_{C} y \in B$
18		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
19		eqid	$⊢ \cdot_{{mulGrp}_{Q}} = \cdot_{{mulGrp}_{Q}}$
20		eqid	$⊢ {var}_{1} (A) = {var}_{1} (A)$
21	1 2 6 18 19 20 3 4 5	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land x \cdot_{C} y \in B) \to T (x \cdot_{C} y) = \underset{k \in ℕ_{0}}{\sum_{Q}} (((x \cdot_{C} y) decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
22	7 8 17 21	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x \cdot_{C} y) = \underset{k \in ℕ_{0}}{\sum_{Q}} (((x \cdot_{C} y) decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
23	1 2 6 3	decpmatmul	$⊢ (R \in Ring \land (x \in B \land y \in B) \land k \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat k = {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))$
24	23	ad4ant234	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat k = {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))$
25	24	oveq1d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to ((x \cdot_{C} y) decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) = ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))$
26	25	mpteq2dva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (k \in ℕ_{0} ⟼ ((x \cdot_{C} y) decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = (k \in ℕ_{0} ⟼ ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
27	26	oveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (((x \cdot_{C} y) decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = \underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
28		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
29	3	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
30	29	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to A \in Ring$
31		eqid	$⊢ {Base}_{A} = {Base}_{A}$
32		eqid	$⊢ 0_{A} = 0_{A}$
33		ringcmn	$⊢ A \in Ring \to A \in CMnd$
34	29 33	syl	$⊢ (N \in Fin \land R \in Ring) \to A \in CMnd$
35	34	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to A \in CMnd$
36		fzfid	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to (0 \dots k) \in Fin$
37	30	ad2antrr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to A \in Ring$
38		simp-5r	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to R \in Ring$
39	12	ad3antrrr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to x \in B$
40		elfznn0	$⊢ z \in (0 \dots k) \to z \in ℕ_{0}$
41	40	adantl	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to z \in ℕ_{0}$
42	1 2 6 3 31	decpmatcl	$⊢ (R \in Ring \land x \in B \land z \in ℕ_{0}) \to x decompPMat z \in {Base}_{A}$
43	38 39 41 42	syl3anc	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to x decompPMat z \in {Base}_{A}$
44	14	ad3antrrr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to y \in B$
45		fznn0sub	$⊢ z \in (0 \dots k) \to k - z \in ℕ_{0}$
46	45	adantl	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to k - z \in ℕ_{0}$
47	1 2 6 3 31	decpmatcl	$⊢ (R \in Ring \land y \in B \land k - z \in ℕ_{0}) \to y decompPMat (k - z) \in {Base}_{A}$
48	38 44 46 47	syl3anc	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to y decompPMat (k - z) \in {Base}_{A}$
49		eqid	$⊢ \cdot_{A} = \cdot_{A}$
50	31 49	ringcl	$⊢ (A \in Ring \land x decompPMat z \in {Base}_{A} \land y decompPMat (k - z) \in {Base}_{A}) \to (x decompPMat z) \cdot_{A} (y decompPMat (k - z)) \in {Base}_{A}$
51	37 43 48 50	syl3anc	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to (x decompPMat z) \cdot_{A} (y decompPMat (k - z)) \in {Base}_{A}$
52	51	ralrimiva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to \forall z \in (0 \dots k) (x decompPMat z) \cdot_{A} (y decompPMat (k - z)) \in {Base}_{A}$
53	31 35 36 52	gsummptcl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z))) \in {Base}_{A}$
54	53	ralrimiva	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to \forall k \in ℕ_{0} {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z))) \in {Base}_{A}$
55	1 2 6 3 49 32	decpmatmulsumfsupp	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))))$
56	55	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))))$
57		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
58	4 28 20 19 30 31 18 32 54 56 57	gsummoncoe1	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n) = ⦋ n / k ⦌ ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z))))$
59		csbov2g	$⊢ n \in ℕ_{0} \to ⦋ n / k ⦌ ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) = \sum_{A} ⦋ n / k ⦌ (z \in (0 \dots k) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (k - z)))$
60		id	$⊢ n \in ℕ_{0} \to n \in ℕ_{0}$
61		oveq2	$⊢ k = n \to (0 \dots k) = (0 \dots n)$
62		oveq1	$⊢ k = n \to k - z = n - z$
63	62	oveq2d	$⊢ k = n \to y decompPMat (k - z) = y decompPMat (n - z)$
64	63	oveq2d	$⊢ k = n \to (x decompPMat z) \cdot_{A} (y decompPMat (k - z)) = (x decompPMat z) \cdot_{A} (y decompPMat (n - z))$
65	61 64	mpteq12dv	$⊢ k = n \to (z \in (0 \dots k) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (k - z))) = (z \in (0 \dots n) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (n - z)))$
66	65	adantl	$⊢ (n \in ℕ_{0} \land k = n) \to (z \in (0 \dots k) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (k - z))) = (z \in (0 \dots n) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (n - z)))$
67	60 66	csbied	$⊢ n \in ℕ_{0} \to ⦋ n / k ⦌ (z \in (0 \dots k) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (k - z))) = (z \in (0 \dots n) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (n - z)))$
68	67	oveq2d	$⊢ n \in ℕ_{0} \to \sum_{A} ⦋ n / k ⦌ (z \in (0 \dots k) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (k - z))) = {\sum_{A}}_{z = 0}^{n} ((x decompPMat z) \cdot_{A} (y decompPMat (n - z)))$
69	59 68	eqtrd	$⊢ n \in ℕ_{0} \to ⦋ n / k ⦌ ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) = {\sum_{A}}_{z = 0}^{n} ((x decompPMat z) \cdot_{A} (y decompPMat (n - z)))$
70	69	adantl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ⦋ n / k ⦌ ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) = {\sum_{A}}_{z = 0}^{n} ((x decompPMat z) \cdot_{A} (y decompPMat (n - z)))$
71		eqidd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (r \in ℕ_{0} ⟼ {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l))) = (r \in ℕ_{0} ⟼ {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l)))$
72		oveq2	$⊢ r = n \to (0 \dots r) = (0 \dots n)$
73		fvoveq1	$⊢ r = n \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l)$
74	73	oveq2d	$⊢ r = n \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l)$
75	72 74	mpteq12dv	$⊢ r = n \to (l \in (0 \dots r) ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l)) = (l \in (0 \dots n) ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l))$
76	75	oveq2d	$⊢ r = n \to {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l)) = {\sum_{A}}_{l = 0}^{n} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l))$
77	76	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land r = n) \to {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l)) = {\sum_{A}}_{l = 0}^{n} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l))$
78		ovexd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {\sum_{A}}_{l = 0}^{n} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l)) \in V$
79	71 77 57 78	fvmptd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (r \in ℕ_{0} ⟼ {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l))) (n) = {\sum_{A}}_{l = 0}^{n} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l))$
80		eqid	$⊢ 0_{Q} = 0_{Q}$
81	4	ply1ring	$⊢ A \in Ring \to Q \in Ring$
82	29 81	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Ring$
83		ringcmn	$⊢ Q \in Ring \to Q \in CMnd$
84	82 83	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in CMnd$
85	84	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to Q \in CMnd$
86		nn0ex	$⊢ ℕ_{0} \in V$
87	86	a1i	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ℕ_{0} \in V$
88	11	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)$
89		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)$
90	88 89	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)$
91	90	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (N \in Fin \land R \in Ring \land x \in B)$
92	1 2 6 18 19 20 3 4 28	pm2mpghmlem1	$⊢ ((N \in Fin \land R \in Ring \land x \in B) \land k \in ℕ_{0}) \to (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
93	91 92	sylan	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
94	93	fmpttd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) : ℕ_{0} ⟶ {Base}_{Q}$
95	1 2 6 18 19 20 3 4	pm2mpghmlem2	$⊢ (N \in Fin \land R \in Ring \land x \in B) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
96	91 95	syl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
97	28 80 85 87 94 96	gsumcl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}$
98	13	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)$
99		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)$
100	98 99	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)$
101	100	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (N \in Fin \land R \in Ring \land y \in B)$
102	1 2 6 18 19 20 3 4 28	pm2mpghmlem1	$⊢ ((N \in Fin \land R \in Ring \land y \in B) \land k \in ℕ_{0}) \to (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
103	101 102	sylan	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
104	103	fmpttd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) : ℕ_{0} ⟶ {Base}_{Q}$
105	7 8 14	3jca	$⊢ ((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)$
106	105	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (N \in Fin \land R \in Ring \land y \in B)$
107	1 2 6 18 19 20 3 4	pm2mpghmlem2	$⊢ (N \in Fin \land R \in Ring \land y \in B) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
108	106 107	syl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
109	28 80 85 87 104 108	gsumcl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}$
110		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
111	4 110 49 28	coe1mul	$⊢ (A \in Ring \land \underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q} \land \underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}) \to {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) = (r \in ℕ_{0} ⟼ {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l)))$
112	111	fveq1d	$⊢ (A \in Ring \land \underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q} \land \underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}) \to {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) (n) = (r \in ℕ_{0} ⟼ {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l))) (n)$
113	30 97 109 112	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) (n) = (r \in ℕ_{0} ⟼ {\sum_{A}}_{l = 0}^{r} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (r - l))) (n)$
114		oveq2	$⊢ z = l \to x decompPMat z = x decompPMat l$
115		oveq2	$⊢ z = l \to n - z = n - l$
116	115	oveq2d	$⊢ z = l \to y decompPMat (n - z) = y decompPMat (n - l)$
117	114 116	oveq12d	$⊢ z = l \to (x decompPMat z) \cdot_{A} (y decompPMat (n - z)) = (x decompPMat l) \cdot_{A} (y decompPMat (n - l))$
118	117	cbvmptv	$⊢ (z \in (0 \dots n) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (n - z))) = (l \in (0 \dots n) ⟼ (x decompPMat l) \cdot_{A} (y decompPMat (n - l)))$
119	29	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to A \in Ring$
120		simp-5r	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land k \in ℕ_{0}) \to R \in Ring$
121	12	ad3antrrr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land k \in ℕ_{0}) \to x \in B$
122		simpr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
123	1 2 6 3 31	decpmatcl	$⊢ (R \in Ring \land x \in B \land k \in ℕ_{0}) \to x decompPMat k \in {Base}_{A}$
124	120 121 122 123	syl3anc	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land k \in ℕ_{0}) \to x decompPMat k \in {Base}_{A}$
125	124	ralrimiva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to \forall k \in ℕ_{0} x decompPMat k \in {Base}_{A}$
126	8 12	jca	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (R \in Ring \land x \in B)$
127	126	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (R \in Ring \land x \in B)$
128	1 2 6 3 32	decpmatfsupp	$⊢ (R \in Ring \land x \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ x decompPMat k))$
129	127 128	syl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ x decompPMat k))$
130		elfznn0	$⊢ l \in (0 \dots n) \to l \in ℕ_{0}$
131	130	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to l \in ℕ_{0}$
132	4 28 20 19 119 31 18 32 125 129 131	gsummoncoe1	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) = ⦋ l / k ⦌ (x decompPMat k)$
133		csbov2g	$⊢ l \in (0 \dots n) \to ⦋ l / k ⦌ (x decompPMat k) = x decompPMat ⦋ l / k ⦌ k$
134		csbvarg	$⊢ l \in (0 \dots n) \to ⦋ l / k ⦌ k = l$
135	134	oveq2d	$⊢ l \in (0 \dots n) \to x decompPMat ⦋ l / k ⦌ k = x decompPMat l$
136	133 135	eqtrd	$⊢ l \in (0 \dots n) \to ⦋ l / k ⦌ (x decompPMat k) = x decompPMat l$
137	136	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to ⦋ l / k ⦌ (x decompPMat k) = x decompPMat l$
138	132 137	eqtr2d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to x decompPMat l = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l)$
139	14	ad3antrrr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land k \in ℕ_{0}) \to y \in B$
140	1 2 6 3 31	decpmatcl	$⊢ (R \in Ring \land y \in B \land k \in ℕ_{0}) \to y decompPMat k \in {Base}_{A}$
141	120 139 122 140	syl3anc	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \land k \in ℕ_{0}) \to y decompPMat k \in {Base}_{A}$
142	141	ralrimiva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to \forall k \in ℕ_{0} y decompPMat k \in {Base}_{A}$
143	8 14	jca	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (R \in Ring \land y \in B)$
144	143	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (R \in Ring \land y \in B)$
145	1 2 6 3 32	decpmatfsupp	$⊢ (R \in Ring \land y \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ y decompPMat k))$
146	144 145	syl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ y decompPMat k))$
147		fznn0sub	$⊢ l \in (0 \dots n) \to n - l \in ℕ_{0}$
148	147	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to n - l \in ℕ_{0}$
149	4 28 20 19 119 31 18 32 142 146 148	gsummoncoe1	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l) = ⦋ (n - l) / k ⦌ (y decompPMat k)$
150		ovex	$⊢ n - l \in V$
151		csbov2g	$⊢ n - l \in V \to ⦋ (n - l) / k ⦌ (y decompPMat k) = y decompPMat ⦋ (n - l) / k ⦌ k$
152	150 151	mp1i	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to ⦋ (n - l) / k ⦌ (y decompPMat k) = y decompPMat ⦋ (n - l) / k ⦌ k$
153		csbvarg	$⊢ n - l \in V \to ⦋ (n - l) / k ⦌ k = n - l$
154	150 153	mp1i	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to ⦋ (n - l) / k ⦌ k = n - l$
155	154	oveq2d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to y decompPMat ⦋ (n - l) / k ⦌ k = y decompPMat (n - l)$
156	149 152 155	3eqtrrd	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to y decompPMat (n - l) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l)$
157	138 156	oveq12d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land l \in (0 \dots n)) \to (x decompPMat l) \cdot_{A} (y decompPMat (n - l)) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l)$
158	157	mpteq2dva	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (l \in (0 \dots n) ⟼ (x decompPMat l) \cdot_{A} (y decompPMat (n - l))) = (l \in (0 \dots n) ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l))$
159	118 158	syl5eq	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (z \in (0 \dots n) ⟼ (x decompPMat z) \cdot_{A} (y decompPMat (n - z))) = (l \in (0 \dots n) ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l))$
160	159	oveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {\sum_{A}}_{z = 0}^{n} ((x decompPMat z) \cdot_{A} (y decompPMat (n - z))) = {\sum_{A}}_{l = 0}^{n} ({coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (l) \cdot_{A} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n - l))$
161	79 113 160	3eqtr4rd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {\sum_{A}}_{z = 0}^{n} ((x decompPMat z) \cdot_{A} (y decompPMat (n - z))) = {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) (n)$
162	58 70 161	3eqtrd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n) = {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) (n)$
163	162	ralrimiva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \forall n \in ℕ_{0} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n) = {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) (n)$
164	29	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to A \in Ring$
165	84	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to Q \in CMnd$
166	86	a1i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to ℕ_{0} \in V$
167	4	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
168	29 167	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in LMod$
169	168	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to Q \in LMod$
170	34	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to A \in CMnd$
171		fzfid	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to (0 \dots k) \in Fin$
172	29	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to A \in Ring$
173		simp-4r	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to R \in Ring$
174		simplrl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to x \in B$
175	174	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to x \in B$
176	40	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to z \in ℕ_{0}$
177	173 175 176 42	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to x decompPMat z \in {Base}_{A}$
178		simplrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to y \in B$
179	178	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to y \in B$
180	45	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to k - z \in ℕ_{0}$
181	173 179 180 47	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to y decompPMat (k - z) \in {Base}_{A}$
182	172 177 181 50	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \land z \in (0 \dots k)) \to (x decompPMat z) \cdot_{A} (y decompPMat (k - z)) \in {Base}_{A}$
183	182	ralrimiva	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to \forall z \in (0 \dots k) (x decompPMat z) \cdot_{A} (y decompPMat (k - z)) \in {Base}_{A}$
184	31 170 171 183	gsummptcl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z))) \in {Base}_{A}$
185	29	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to A \in Ring$
186	4	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
187	185 186	syl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to A = Scalar (Q)$
188	187	eqcomd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to Scalar (Q) = A$
189	188	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to {Base}_{Scalar (Q)} = {Base}_{A}$
190	184 189	eleqtrrd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z))) \in {Base}_{Scalar (Q)}$
191		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
192	4 20 191 19 28	ply1moncl	$⊢ (A \in Ring \land k \in ℕ_{0}) \to k \cdot_{{mulGrp}_{Q}} {var}_{1} (A) \in {Base}_{Q}$
193	185 192	sylancom	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to k \cdot_{{mulGrp}_{Q}} {var}_{1} (A) \in {Base}_{Q}$
194		eqid	$⊢ Scalar (Q) = Scalar (Q)$
195		eqid	$⊢ {Base}_{Scalar (Q)} = {Base}_{Scalar (Q)}$
196	28 194 18 195	lmodvscl	$⊢ (Q \in LMod \land {\sum_{A}}_{z = 0}^{k} ((x decompPMat z) \cdot_{A} (y decompPMat (k - z))) \in {Base}_{Scalar (Q)} \land k \cdot_{{mulGrp}_{Q}} {var}_{1} (A) \in {Base}_{Q}) \to ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
197	169 190 193 196	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
198	197	fmpttd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (k \in ℕ_{0} ⟼ ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) : ℕ_{0} ⟶ {Base}_{Q}$
199	1 2 6 18 19 20 3 4 28 5	pm2mpmhmlem1	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ ({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
200	28 80 165 166 198 199	gsumcl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}$
201	82	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to Q \in Ring$
202	90 92	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
203	202	fmpttd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (k \in ℕ_{0} ⟼ (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) : ℕ_{0} ⟶ {Base}_{Q}$
204	90 95	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
205	28 80 165 166 203 204	gsumcl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}$
206	100 102	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land k \in ℕ_{0}) \to (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)) \in {Base}_{Q}$
207	206	fmpttd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (k \in ℕ_{0} ⟼ (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) : ℕ_{0} ⟶ {Base}_{Q}$
208	7 8 14 107	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{0_{Q}} ((k \in ℕ_{0} ⟼ (y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
209	28 80 165 166 207 208	gsumcl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}$
210	28 110	ringcl	$⊢ (Q \in Ring \land \underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q} \land \underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q}) \to (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \in {Base}_{Q}$
211	201 205 209 210	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \in {Base}_{Q}$
212		eqid	$⊢ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
213		eqid	$⊢ {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) = {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))))$
214	4 28 212 213	ply1coe1eq	$⊢ (A \in Ring \land \underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) \in {Base}_{Q} \land (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \in {Base}_{Q}) \to (\forall n \in ℕ_{0} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n) = {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) (n) \leftrightarrow \underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))))$
215	164 200 211 214	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\forall n \in ℕ_{0} {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) (n) = {coe}_{1} ((\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))) (n) \leftrightarrow \underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))))$
216	163 215	mpbid	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \underset{k \in ℕ_{0}}{\sum_{Q}} (({\sum_{A}}_{z = 0}^{k}, ((x decompPMat z) \cdot_{A} (y decompPMat (k - z)))) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
217	22 27 216	3eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x \cdot_{C} y) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
218	1 2 6 18 19 20 3 4 5	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land x \in B) \to T (x) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
219	7 8 12 218	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
220	1 2 6 18 19 20 3 4 5	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land y \in B) \to T (y) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
221	7 8 14 220	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (y) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))$
222	219 221	oveq12d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x) \cdot_{Q} T (y) = (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((x decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A)))) \cdot_{Q} (\underset{k \in ℕ_{0}}{\sum_{Q}}, ((y decompPMat k) \cdot_{Q} (k \cdot_{{mulGrp}_{Q}} {var}_{1} (A))))$
223	217 222	eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to T (x \cdot_{C} y) = T (x) \cdot_{Q} T (y)$
224	223	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in B \forall y \in B T (x \cdot_{C} y) = T (x) \cdot_{Q} T (y)$

Metamath Proof Explorer

Theorem pm2mpmhmlem2

Proof