pm2mpmhmlem1

Description: Lemma 1 for pm2mpmhm . (Contributed by AV, 21-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	pm2mpmhmlem1	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{0_{Q}} ((l \in ℕ_{0} ⟼ ({\sum_{A}}_{k = 0}^{l}, ((x decompPMat k) \cdot_{A} (y decompPMat (l - k)))) \underset{˙}{*} (l \underset{˙}{\times} X)))$

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		fvexd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to 0_{Q} \in V$
12		ovexd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land l \in ℕ_{0}) \to ({\sum_{A}}_{k = 0}^{l}, ((x decompPMat k) \cdot_{A} (y decompPMat (l - k)))) \underset{˙}{*} (l \underset{˙}{\times} X) \in V$
13		oveq2	$⊢ l = n \to (0 \dots l) = (0 \dots n)$
14		oveq1	$⊢ l = n \to l - k = n - k$
15	14	oveq2d	$⊢ l = n \to y decompPMat (l - k) = y decompPMat (n - k)$
16	15	oveq2d	$⊢ l = n \to (x decompPMat k) \cdot_{A} (y decompPMat (l - k)) = (x decompPMat k) \cdot_{A} (y decompPMat (n - k))$
17	13 16	mpteq12dv	$⊢ l = n \to (k \in (0 \dots l) ⟼ (x decompPMat k) \cdot_{A} (y decompPMat (l - k))) = (k \in (0 \dots n) ⟼ (x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
18	17	oveq2d	$⊢ l = n \to {\sum_{A}}_{k = 0}^{l} ((x decompPMat k) \cdot_{A} (y decompPMat (l - k))) = {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
19		oveq1	$⊢ l = n \to l \underset{˙}{\times} X = n \underset{˙}{\times} X$
20	18 19	oveq12d	$⊢ l = n \to ({\sum_{A}}_{k = 0}^{l}, ((x decompPMat k) \cdot_{A} (y decompPMat (l - k)))) \underset{˙}{} (l \underset{˙}{\times} X) = ({\sum_{A}}_{k = 0}^{n}, ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))) \underset{˙}{} (n \underset{˙}{\times} X)$
21		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to N \in Fin$
22		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to R \in Ring$
23	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
24	23	anim1i	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (C \in Ring \land (x \in B \land y \in B))$
25		3anass	$⊢ (C \in Ring \land x \in B \land y \in B) \leftrightarrow (C \in Ring \land (x \in B \land y \in B))$
26	24 25	sylibr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (C \in Ring \land x \in B \land y \in B)$
27		eqid	$⊢ \cdot_{C} = \cdot_{C}$
28	3 27	ringcl	$⊢ (C \in Ring \land x \in B \land y \in B) \to x \cdot_{C} y \in B$
29	26 28	syl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to x \cdot_{C} y \in B$
30		eqid	$⊢ 0_{R} = 0_{R}$
31	1 2 3 30	pmatcoe1fsupp	$⊢ (N \in Fin \land R \in Ring \land x \cdot_{C} y \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R})$
32	21 22 29 31	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R})$
33		fvoveq1	$⊢ a = i \to {coe}_{1} (a (x \cdot_{C} y) b) = {coe}_{1} (i (x \cdot_{C} y) b)$
34	33	fveq1d	$⊢ a = i \to {coe}_{1} (a (x \cdot_{C} y) b) (n) = {coe}_{1} (i (x \cdot_{C} y) b) (n)$
35	34	eqeq1d	$⊢ a = i \to ({coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R} \leftrightarrow {coe}_{1} (i (x \cdot_{C} y) b) (n) = 0_{R})$
36		oveq2	$⊢ b = j \to i (x \cdot_{C} y) b = i (x \cdot_{C} y) j$
37	36	fveq2d	$⊢ b = j \to {coe}_{1} (i (x \cdot_{C} y) b) = {coe}_{1} (i (x \cdot_{C} y) j)$
38	37	fveq1d	$⊢ b = j \to {coe}_{1} (i (x \cdot_{C} y) b) (n) = {coe}_{1} (i (x \cdot_{C} y) j) (n)$
39	38	eqeq1d	$⊢ b = j \to ({coe}_{1} (i (x \cdot_{C} y) b) (n) = 0_{R} \leftrightarrow {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R})$
40	35 39	rspc2va	$⊢ ((i \in N \land j \in N) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R}$
41	40	expcom	$⊢ \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R} \to ((i \in N \land j \in N) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R})$
42	41	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to ((i \in N \land j \in N) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R})$
43	42	3impib	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \land i \in N \land j \in N) \to {coe}_{1} (i (x \cdot_{C} y) j) (n) = 0_{R}$
44	43	mpoeq3dva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = (i \in N, j \in N ⟼ 0_{R})$
45	7 30	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
46	45	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
47	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
48	8	ply1sca	$⊢ A \in Ring \to A = Scalar (Q)$
49	47 48	syl	$⊢ (N \in Fin \land R \in Ring) \to A = Scalar (Q)$
50	49	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to A = Scalar (Q)$
51	50	fveq2d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to 0_{A} = 0_{Scalar (Q)}$
52	44 46 51	3eqtr2d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) = 0_{Scalar (Q)}$
53	52	oveq1d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Scalar (Q)} \underset{˙}{} (n \underset{˙}{\times} X)$
54	8	ply1lmod	$⊢ A \in Ring \to Q \in LMod$
55	47 54	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in LMod$
56	55	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to Q \in LMod$
57	47	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to A \in Ring$
58		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
59	8 6 58 5 9	ply1moncl	$⊢ (A \in Ring \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in L$
60	57 59	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in L$
61		eqid	$⊢ Scalar (Q) = Scalar (Q)$
62		eqid	$⊢ 0_{Scalar (Q)} = 0_{Scalar (Q)}$
63		eqid	$⊢ 0_{Q} = 0_{Q}$
64	9 61 4 62 63	lmod0vs	$⊢ (Q \in LMod \land n \underset{˙}{\times} X \in L) \to 0_{Scalar (Q)} \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q}$
65	56 60 64	syl2an2r	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to 0_{Scalar (Q)} \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q}$
66	65	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to 0_{Scalar (Q)} \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q}$
67	53 66	eqtrd	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \land \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q}$
68	67	ex	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (\forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R} \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q})$
69	68	imim2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ((s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q}))$
70	69	ralimdva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q}))$
71	70	reximdv	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to \forall a \in N \forall b \in N {coe}_{1} (a (x \cdot_{C} y) b) (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q}))$
72	32 71	mpd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q})$
73	2 3	decpmatval	$⊢ (x \cdot_{C} y \in B \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n))$
74	29 73	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n))$
75	74	oveq1d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{} (n \underset{˙}{\times} X)$
76	75	eqeq1d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q} \leftrightarrow (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q})$
77	76	imbi2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ((s < n \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}) \leftrightarrow (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}))$
78	77	ralbidva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\forall n \in ℕ_{0} (s < n \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}) \leftrightarrow \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}))$
79	78	rexbidv	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}) \leftrightarrow \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (i \in N, j \in N ⟼ {coe}_{1} (i (x \cdot_{C} y) j) (n)) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}))$
80	72 79	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q})$
81	1 2 3 7	decpmatmul	$⊢ (R \in Ring \land (x \in B \land y \in B) \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
82	81	ad4ant234	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (x \cdot_{C} y) decompPMat n = {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))$
83	82	eqcomd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to {\sum_{A}}_{k = 0}^{n} ((x decompPMat k) \cdot_{A} (y decompPMat (n - k))) = (x \cdot_{C} y) decompPMat n$
84	83	oveq1d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ({\sum_{A}}_{k = 0}^{n}, ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))) \underset{˙}{} (n \underset{˙}{\times} X) = ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X)$
85	84	eqeq1d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to (({\sum_{A}}_{k = 0}^{n}, ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q} \leftrightarrow ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q})$
86	85	imbi2d	$⊢ (((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \land n \in ℕ_{0}) \to ((s < n \to ({\sum_{A}}_{k = 0}^{n}, ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}) \leftrightarrow (s < n \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}))$
87	86	ralbidva	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\forall n \in ℕ_{0} (s < n \to ({\sum_{A}}_{k = 0}^{n}, ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}) \leftrightarrow \forall n \in ℕ_{0} (s < n \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}))$
88	87	rexbidv	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to (\exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to ({\sum_{A}}_{k = 0}^{n}, ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}) \leftrightarrow \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to ((x \cdot_{C} y) decompPMat n) \underset{˙}{} (n \underset{˙}{\times} X) = 0_{Q}))$
89	80 88	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to ({\sum_{A}}_{k = 0}^{n}, ((x decompPMat k) \cdot_{A} (y decompPMat (n - k)))) \underset{˙}{*} (n \underset{˙}{\times} X) = 0_{Q})$
90	11 12 20 89	mptnn0fsuppd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in B \land y \in B)) \to {finSupp}_{0_{Q}} ((l \in ℕ_{0} ⟼ ({\sum_{A}}_{k = 0}^{l}, ((x decompPMat k) \cdot_{A} (y decompPMat (l - k)))) \underset{˙}{*} (l \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem pm2mpmhmlem1

Proof