pmatcollpw3lem

Description: Lemma for pmatcollpw3 and pmatcollpw3fi : Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpw.c	$⊢ C = N Mat P$
	pmatcollpw.b	$⊢ B = {Base}_{C}$
	pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
	pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpw.x	$⊢ X = {var}_{1} (R)$
	pmatcollpw.t	$⊢ T = N matToPolyMat R$
	pmatcollpw3.a	$⊢ A = N Mat R$
	pmatcollpw3.d	$⊢ D = {Base}_{A}$
Assertion	pmatcollpw3lem	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to (M = \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)) \to \exists f \in (D^{I}) M = \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (f (n))))$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpw.c	$⊢ C = N Mat P$
3		pmatcollpw.b	$⊢ B = {Base}_{C}$
4		pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
5		pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpw.x	$⊢ X = {var}_{1} (R)$
7		pmatcollpw.t	$⊢ T = N matToPolyMat R$
8		pmatcollpw3.a	$⊢ A = N Mat R$
9		pmatcollpw3.d	$⊢ D = {Base}_{A}$
10		dmeq	$⊢ x = y \to dom x = dom y$
11	10	dmeqd	$⊢ x = y \to dom dom x = dom dom y$
12		oveq	$⊢ x = y \to i x j = i y j$
13	12	fveq2d	$⊢ x = y \to {coe}_{1} (i x j) = {coe}_{1} (i y j)$
14	13	fveq1d	$⊢ x = y \to {coe}_{1} (i x j) (k) = {coe}_{1} (i y j) (k)$
15	11 11 14	mpoeq123dv	$⊢ x = y \to (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) = (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k))$
16		fveq2	$⊢ k = l \to {coe}_{1} (i y j) (k) = {coe}_{1} (i y j) (l)$
17	16	mpoeq3dv	$⊢ k = l \to (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k)) = (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l))$
18	15 17	cbvmpov	$⊢ (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) = (y \in B, l \in I ⟼ (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)))$
19		dmexg	$⊢ y \in B \to dom y \in V$
20	19	dmexd	$⊢ y \in B \to dom dom y \in V$
21	20 20	jca	$⊢ y \in B \to (dom dom y \in V \land dom dom y \in V)$
22	21	ad2antrl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land (y \in B \land l \in I)) \to (dom dom y \in V \land dom dom y \in V)$
23		mpoexga	$⊢ (dom dom y \in V \land dom dom y \in V) \to (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)) \in V$
24	22 23	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land (y \in B \land l \in I)) \to (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)) \in V$
25	24	ralrimivva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to \forall y \in B \forall l \in I (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)) \in V$
26		simprr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to I \neq \emptyset$
27		nn0ex	$⊢ ℕ_{0} \in V$
28	27	ssex	$⊢ I \subseteq ℕ_{0} \to I \in V$
29	28	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to I \in V$
30		simp3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to M \in B$
31	30	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to M \in B$
32	18 25 26 29 31	mpocurryvald	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) = (l \in I ⟼ ⦋ M / y ⦌ (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)))$
33		fveq2	$⊢ l = k \to {coe}_{1} (i y j) (l) = {coe}_{1} (i y j) (k)$
34	33	mpoeq3dv	$⊢ l = k \to (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)) = (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k))$
35	34	csbeq2dv	$⊢ l = k \to ⦋ M / y ⦌ (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)) = ⦋ M / y ⦌ (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k))$
36		eqcom	$⊢ x = y \leftrightarrow y = x$
37		eqcom	$⊢ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) = (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k)) \leftrightarrow (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k)) = (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))$
38	15 36 37	3imtr3i	$⊢ y = x \to (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k)) = (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))$
39	38	cbvcsbv	$⊢ ⦋ M / y ⦌ (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (k)) = ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))$
40	35 39	eqtrdi	$⊢ l = k \to ⦋ M / y ⦌ (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l)) = ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))$
41	40	cbvmptv	$⊢ (l \in I ⟼ ⦋ M / y ⦌ (i \in dom dom y, j \in dom dom y ⟼ {coe}_{1} (i y j) (l))) = (k \in I ⟼ ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)))$
42	32 41	eqtrdi	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) = (k \in I ⟼ ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)))$
43		dmeq	$⊢ x = M \to dom x = dom M$
44	43	dmeqd	$⊢ x = M \to dom dom x = dom dom M$
45		oveq	$⊢ x = M \to i x j = i M j$
46	45	fveq2d	$⊢ x = M \to {coe}_{1} (i x j) = {coe}_{1} (i M j)$
47	46	fveq1d	$⊢ x = M \to {coe}_{1} (i x j) (k) = {coe}_{1} (i M j) (k)$
48	44 44 47	mpoeq123dv	$⊢ x = M \to (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (k))$
49	48	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land x = M) \to (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (k))$
50	30 49	csbied	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (k))$
51		eqid	$⊢ {Base}_{P} = {Base}_{P}$
52	2 51 3	matbas2i	$⊢ M \in B \to M \in ({Base}_{P}^{(N \times N)})$
53		elmapi	$⊢ M \in ({Base}_{P}^{(N \times N)}) \to M : N \times N ⟶ {Base}_{P}$
54		fdm	$⊢ M : N \times N ⟶ {Base}_{P} \to dom M = N \times N$
55	54	dmeqd	$⊢ M : N \times N ⟶ {Base}_{P} \to dom dom M = dom (N \times N)$
56		dmxpid	$⊢ dom (N \times N) = N$
57	55 56	eqtr2di	$⊢ M : N \times N ⟶ {Base}_{P} \to N = dom dom M$
58	52 53 57	3syl	$⊢ M \in B \to N = dom dom M$
59	58	3ad2ant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to N = dom dom M$
60	59	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to N = dom dom M$
61		simpr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to m = M$
62	61	oveqd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to i m j = i M j$
63	62	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to {coe}_{1} (i m j) = {coe}_{1} (i M j)$
64	63	fveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to {coe}_{1} (i m j) (k) = {coe}_{1} (i M j) (k)$
65	60 60 64	mpoeq123dv	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)) = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (k))$
66	30 65	csbied	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)) = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (k))$
67	50 66	eqtr4d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) = ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))$
68	67	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) = ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))$
69	68	mpteq2dv	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to (k \in I ⟼ ⦋ M / x ⦌ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) = (k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)))$
70	42 69	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) = (k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)))$
71		oveq	$⊢ m = M \to i m j = i M j$
72	71	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to i m j = i M j$
73	72	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to {coe}_{1} (i m j) = {coe}_{1} (i M j)$
74	73	fveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to {coe}_{1} (i m j) (k) = {coe}_{1} (i M j) (k)$
75	74	mpoeq3dv	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land m = M) \to (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (k))$
76	30 75	csbied	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (k))$
77	76	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \to ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)) = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (k))$
78		eqid	$⊢ {Base}_{R} = {Base}_{R}$
79		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \to N \in Fin$
80		simpll2	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \to R \in CRing$
81		simp2	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \land i \in N \land j \in N) \to i \in N$
82		simp3	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \land i \in N \land j \in N) \to j \in N$
83	31	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \to M \in B$
84	83	3ad2ant1	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \land i \in N \land j \in N) \to M \in B$
85	2 51 3 81 82 84	matecld	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \land i \in N \land j \in N) \to i M j \in {Base}_{P}$
86		ssel	$⊢ I \subseteq ℕ_{0} \to (k \in I \to k \in ℕ_{0})$
87	86	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to (k \in I \to k \in ℕ_{0})$
88	87	imp	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \to k \in ℕ_{0}$
89	88	3ad2ant1	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \land i \in N \land j \in N) \to k \in ℕ_{0}$
90		eqid	$⊢ {coe}_{1} (i M j) = {coe}_{1} (i M j)$
91	90 51 1 78	coe1fvalcl	$⊢ (i M j \in {Base}_{P} \land k \in ℕ_{0}) \to {coe}_{1} (i M j) (k) \in {Base}_{R}$
92	85 89 91	syl2anc	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \land i \in N \land j \in N) \to {coe}_{1} (i M j) (k) \in {Base}_{R}$
93	8 78 9 79 80 92	matbas2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \to (i \in N, j \in N ⟼ {coe}_{1} (i M j) (k)) \in D$
94	77 93	eqeltrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land k \in I) \to ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k)) \in D$
95	94	fmpttd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to (k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))) : I ⟶ D$
96	9	fvexi	$⊢ D \in V$
97	96	a1i	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to D \in V$
98	28	adantr	$⊢ (I \subseteq ℕ_{0} \land I \neq \emptyset) \to I \in V$
99		elmapg	$⊢ (D \in V \land I \in V) \to ((k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))) \in (D^{I}) \leftrightarrow (k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))) : I ⟶ D)$
100	97 98 99	syl2an	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to ((k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))) \in (D^{I}) \leftrightarrow (k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))) : I ⟶ D)$
101	95 100	mpbird	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to (k \in I ⟼ ⦋ M / m ⦌ (i \in N, j \in N ⟼ {coe}_{1} (i m j) (k))) \in (D^{I})$
102	70 101	eqeltrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) \in (D^{I})$
103		fveq1	$⊢ f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) \to f (n) = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) (n)$
104	103	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \to f (n) = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) (n)$
105	104	adantr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to f (n) = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) (n)$
106		eqid	$⊢ (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) = (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)))$
107		dmexg	$⊢ x \in B \to dom x \in V$
108	107	dmexd	$⊢ x \in B \to dom dom x \in V$
109	108 108	jca	$⊢ x \in B \to (dom dom x \in V \land dom dom x \in V)$
110	109	ad2antrl	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \land (x \in B \land k \in I)) \to (dom dom x \in V \land dom dom x \in V)$
111		mpoexga	$⊢ (dom dom x \in V \land dom dom x \in V) \to (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) \in V$
112	110 111	syl	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \land (x \in B \land k \in I)) \to (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) \in V$
113	112	ralrimivva	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to \forall x \in B \forall k \in I (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)) \in V$
114	29	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to I \in V$
115	31	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to M \in B$
116		simpr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to n \in I$
117	106 113 114 115 116	fvmpocurryd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) (n) = M (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) n$
118		df-decpmat	$⊢ decompPMat = (x \in V, k \in ℕ_{0} ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)))$
119	118	reseq1i	$⊢ {decompPMat ↾}_{(B \times I)} = {(x \in V, k \in ℕ_{0} ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) ↾}_{(B \times I)}$
120		ssv	$⊢ B \subseteq V$
121	120	a1i	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to B \subseteq V$
122		simpl	$⊢ (I \subseteq ℕ_{0} \land I \neq \emptyset) \to I \subseteq ℕ_{0}$
123	121 122	anim12i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to (B \subseteq V \land I \subseteq ℕ_{0})$
124	123	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to (B \subseteq V \land I \subseteq ℕ_{0})$
125		resmpo	$⊢ (B \subseteq V \land I \subseteq ℕ_{0}) \to {(x \in V, k \in ℕ_{0} ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) ↾}_{(B \times I)} = (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)))$
126	124 125	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to {(x \in V, k \in ℕ_{0} ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) ↾}_{(B \times I)} = (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k)))$
127	119 126	eqtr2id	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) = {decompPMat ↾}_{(B \times I)}$
128	127	oveqd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to M (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) n = M ({decompPMat ↾}_{(B \times I)}) n$
129	117 128	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land n \in I) \to curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) (n) = M ({decompPMat ↾}_{(B \times I)}) n$
130	129	adantlr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M) (n) = M ({decompPMat ↾}_{(B \times I)}) n$
131	105 130	eqtrd	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to f (n) = M ({decompPMat ↾}_{(B \times I)}) n$
132	131	fveq2d	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to T (f (n)) = T (M ({decompPMat ↾}_{(B \times I)}) n)$
133	30	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \to M \in B$
134		ovres	$⊢ (M \in B \land n \in I) \to M ({decompPMat ↾}_{(B \times I)}) n = M decompPMat n$
135	133 134	sylan	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to M ({decompPMat ↾}_{(B \times I)}) n = M decompPMat n$
136	135	fveq2d	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to T (M ({decompPMat ↾}_{(B \times I)}) n) = T (M decompPMat n)$
137	132 136	eqtrd	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to T (f (n)) = T (M decompPMat n)$
138	137	oveq2d	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \land n \in I) \to (n \underset{˙}{\times} X) \underset{˙}{} T (f (n)) = (n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)$
139	138	mpteq2dva	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \to (n \in I ⟼ (n \underset{˙}{\times} X) \underset{˙}{} T (f (n))) = (n \in I ⟼ (n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n))$
140	139	oveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \to \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (f (n))) = \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n))$
141	140	eqeq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \land f = curry (x \in B, k \in I ⟼ (i \in dom dom x, j \in dom dom x ⟼ {coe}_{1} (i x j) (k))) (M)) \to (M = \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (f (n))) \leftrightarrow M = \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)))$
142	102 141	rspcedv	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (I \subseteq ℕ_{0} \land I \neq \emptyset)) \to (M = \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)) \to \exists f \in (D^{I}) M = \underset{n \in I}{\sum_{C}} ((n \underset{˙}{\times} X) \underset{˙}{} T (f (n))))$

Metamath Proof Explorer

Theorem pmatcollpw3lem

Proof