monmatcollpw

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix having scaled monomials with the same power as entries is the matrix of the coefficients of the monomials or a zero matrix. Generalization of decpmatid (but requires R to be commutative!). (Contributed by AV, 11-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	monmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
	monmatcollpw.c	$⊢ C = N Mat P$
	monmatcollpw.a	$⊢ A = N Mat R$
	monmatcollpw.k	$⊢ K = {Base}_{A}$
	monmatcollpw.0	$⊢ \underset{˙}{0} = 0_{A}$
	monmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	monmatcollpw.x	$⊢ X = {var}_{1} (R)$
	monmatcollpw.m	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
	monmatcollpw.t	$⊢ T = N matToPolyMat R$
Assertion	monmatcollpw	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) decompPMat I = if (I = L, M, \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		monmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
2		monmatcollpw.c	$⊢ C = N Mat P$
3		monmatcollpw.a	$⊢ A = N Mat R$
4		monmatcollpw.k	$⊢ K = {Base}_{A}$
5		monmatcollpw.0	$⊢ \underset{˙}{0} = 0_{A}$
6		monmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
7		monmatcollpw.x	$⊢ X = {var}_{1} (R)$
8		monmatcollpw.m	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
9		monmatcollpw.t	$⊢ T = N matToPolyMat R$
10		simpll	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to N \in Fin$
11		crngring	$⊢ R \in CRing \to R \in Ring$
12	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
13	11 12	syl	$⊢ R \in CRing \to P \in Ring$
14	13	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to P \in Ring$
15	11	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
16		simp2	$⊢ (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0}) \to L \in ℕ_{0}$
17		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
18		eqid	$⊢ {Base}_{P} = {Base}_{P}$
19	1 7 17 6 18	ply1moncl	$⊢ (R \in Ring \land L \in ℕ_{0}) \to L \underset{˙}{\times} X \in {Base}_{P}$
20	15 16 19	syl2an	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to L \underset{˙}{\times} X \in {Base}_{P}$
21	11	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
22		simp1	$⊢ (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0}) \to M \in K$
23	21 22	anim12i	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to ((N \in Fin \land R \in Ring) \land M \in K)$
24		df-3an	$⊢ (N \in Fin \land R \in Ring \land M \in K) \leftrightarrow ((N \in Fin \land R \in Ring) \land M \in K)$
25	23 24	sylibr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (N \in Fin \land R \in Ring \land M \in K)$
26	9 3 4 1 2	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in K) \to T (M) \in {Base}_{C}$
27	25 26	syl	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to T (M) \in {Base}_{C}$
28	20 27	jca	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (L \underset{˙}{\times} X \in {Base}_{P} \land T (M) \in {Base}_{C})$
29		eqid	$⊢ {Base}_{C} = {Base}_{C}$
30	18 2 29 8	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (L \underset{˙}{\times} X \in {Base}_{P} \land T (M) \in {Base}_{C})) \to (L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M) \in {Base}_{C}$
31	10 14 28 30	syl21anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M) \in {Base}_{C}$
32		simpr3	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to I \in ℕ_{0}$
33	2 29	decpmatval	$⊢ ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M) \in {Base}_{C} \land I \in ℕ_{0}) \to ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) decompPMat I = (i \in N, j \in N ⟼ {coe}_{1} (i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j) (I))$
34	31 32 33	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) decompPMat I = (i \in N, j \in N ⟼ {coe}_{1} (i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j) (I))$
35	14	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to P \in Ring$
36	28	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (L \underset{˙}{\times} X \in {Base}_{P} \land T (M) \in {Base}_{C})$
37		3simpc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (i \in N \land j \in N)$
38		eqid	$⊢ \cdot_{P} = \cdot_{P}$
39	2 29 18 8 38	matvscacell	$⊢ (P \in Ring \land (L \underset{˙}{\times} X \in {Base}_{P} \land T (M) \in {Base}_{C}) \land (i \in N \land j \in N)) \to i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j = (L \underset{˙}{\times} X) \cdot_{P} (i T (M) j)$
40	35 36 37 39	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j = (L \underset{˙}{\times} X) \cdot_{P} (i T (M) j)$
41	40	fveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {coe}_{1} (i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j) = {coe}_{1} ((L \underset{˙}{\times} X) \cdot_{P} (i T (M) j))$
42	41	fveq1d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {coe}_{1} (i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j) (I) = {coe}_{1} ((L \underset{˙}{\times} X) \cdot_{P} (i T (M) j)) (I)$
43	22	anim2i	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to ((N \in Fin \land R \in CRing) \land M \in K)$
44		df-3an	$⊢ (N \in Fin \land R \in CRing \land M \in K) \leftrightarrow ((N \in Fin \land R \in CRing) \land M \in K)$
45	43 44	sylibr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (N \in Fin \land R \in CRing \land M \in K)$
46	45	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (N \in Fin \land R \in CRing \land M \in K)$
47		eqid	$⊢ algSc (P) = algSc (P)$
48	9 3 4 1 47	mat2pmatvalel	$⊢ ((N \in Fin \land R \in CRing \land M \in K) \land (i \in N \land j \in N)) \to i T (M) j = algSc (P) (i M j)$
49	46 37 48	syl2anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to i T (M) j = algSc (P) (i M j)$
50	49	oveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (L \underset{˙}{\times} X) \cdot_{P} (i T (M) j) = (L \underset{˙}{\times} X) \cdot_{P} algSc (P) (i M j)$
51	1	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
52	51	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to P \in AssAlg$
53	52	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to P \in AssAlg$
54		eqid	$⊢ {Base}_{R} = {Base}_{R}$
55		eqid	$⊢ {Base}_{A} = {Base}_{A}$
56		simp2	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to i \in N$
57		simp3	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to j \in N$
58	4	eleq2i	$⊢ M \in K \leftrightarrow M \in {Base}_{A}$
59	58	biimpi	$⊢ M \in K \to M \in {Base}_{A}$
60	59	3ad2ant1	$⊢ (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0}) \to M \in {Base}_{A}$
61	60	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to M \in {Base}_{A}$
62	61	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to M \in {Base}_{A}$
63	3 54 55 56 57 62	matecld	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to i M j \in {Base}_{R}$
64	1	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
65	64	adantl	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (P)$
66	65	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to Scalar (P) = R$
67	66	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{Scalar (P)} = {Base}_{R}$
68	67	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to {Base}_{Scalar (P)} = {Base}_{R}$
69	68	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {Base}_{Scalar (P)} = {Base}_{R}$
70	63 69	eleqtrrd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to i M j \in {Base}_{Scalar (P)}$
71	20	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to L \underset{˙}{\times} X \in {Base}_{P}$
72		eqid	$⊢ Scalar (P) = Scalar (P)$
73		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
74		eqid	$⊢ \cdot_{P} = \cdot_{P}$
75	47 72 73 18 38 74	asclmul2	$⊢ (P \in AssAlg \land i M j \in {Base}_{Scalar (P)} \land L \underset{˙}{\times} X \in {Base}_{P}) \to (L \underset{˙}{\times} X) \cdot_{P} algSc (P) (i M j) = (i M j) \cdot_{P} (L \underset{˙}{\times} X)$
76	53 70 71 75	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (L \underset{˙}{\times} X) \cdot_{P} algSc (P) (i M j) = (i M j) \cdot_{P} (L \underset{˙}{\times} X)$
77	50 76	eqtrd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (L \underset{˙}{\times} X) \cdot_{P} (i T (M) j) = (i M j) \cdot_{P} (L \underset{˙}{\times} X)$
78	77	fveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {coe}_{1} ((L \underset{˙}{\times} X) \cdot_{P} (i T (M) j)) = {coe}_{1} ((i M j) \cdot_{P} (L \underset{˙}{\times} X))$
79	78	fveq1d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {coe}_{1} ((L \underset{˙}{\times} X) \cdot_{P} (i T (M) j)) (I) = {coe}_{1} ((i M j) \cdot_{P} (L \underset{˙}{\times} X)) (I)$
80	11	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to R \in Ring$
81	80	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to R \in Ring$
82		simp1r2	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to L \in ℕ_{0}$
83		eqid	$⊢ 0_{R} = 0_{R}$
84	83 54 1 7 74 17 6	coe1tm	$⊢ (R \in Ring \land i M j \in {Base}_{R} \land L \in ℕ_{0}) \to {coe}_{1} ((i M j) \cdot_{P} (L \underset{˙}{\times} X)) = (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R}))$
85	81 63 82 84	syl3anc	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {coe}_{1} ((i M j) \cdot_{P} (L \underset{˙}{\times} X)) = (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R}))$
86	85	fveq1d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {coe}_{1} ((i M j) \cdot_{P} (L \underset{˙}{\times} X)) (I) = (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)$
87	42 79 86	3eqtrd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to {coe}_{1} (i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j) (I) = (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)$
88	87	mpoeq3dva	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (i \in N, j \in N ⟼ {coe}_{1} (i ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) j) (I)) = (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I))$
89	21	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (N \in Fin \land R \in Ring)$
90	89	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to (N \in Fin \land R \in Ring)$
91	3 83	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (z \in N, w \in N ⟼ 0_{R})$
92	90 91	syl	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to 0_{A} = (z \in N, w \in N ⟼ 0_{R})$
93	5 92	syl5eq	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to \underset{˙}{0} = (z \in N, w \in N ⟼ 0_{R})$
94		eqidd	$⊢ ((((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \land (z = x \land w = y)) \to 0_{R} = 0_{R}$
95		simprl	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to x \in N$
96		simprr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to y \in N$
97		fvexd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to 0_{R} \in V$
98	93 94 95 96 97	ovmpod	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to x \underset{˙}{0} y = 0_{R}$
99	98	eqcomd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to 0_{R} = x \underset{˙}{0} y$
100	99	ifeq2d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to if (I = L, x M y, 0_{R}) = if (I = L, x M y, x \underset{˙}{0} y)$
101		eqidd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) = (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I))$
102		oveq12	$⊢ (i = x \land j = y) \to i M j = x M y$
103	102	ifeq1d	$⊢ (i = x \land j = y) \to if (l = L, i M j, 0_{R}) = if (l = L, x M y, 0_{R})$
104	103	mpteq2dv	$⊢ (i = x \land j = y) \to (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) = (l \in ℕ_{0} ⟼ if (l = L, x M y, 0_{R}))$
105	104	fveq1d	$⊢ (i = x \land j = y) \to (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I) = (l \in ℕ_{0} ⟼ if (l = L, x M y, 0_{R})) (I)$
106		eqidd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to (l \in ℕ_{0} ⟼ if (l = L, x M y, 0_{R})) = (l \in ℕ_{0} ⟼ if (l = L, x M y, 0_{R}))$
107		eqeq1	$⊢ l = I \to (l = L \leftrightarrow I = L)$
108	107	ifbid	$⊢ l = I \to if (l = L, x M y, 0_{R}) = if (I = L, x M y, 0_{R})$
109	108	adantl	$⊢ ((((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \land l = I) \to if (l = L, x M y, 0_{R}) = if (I = L, x M y, 0_{R})$
110	32	adantr	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to I \in ℕ_{0}$
111		ovex	$⊢ x M y \in V$
112		fvex	$⊢ 0_{R} \in V$
113	111 112	ifex	$⊢ if (I = L, x M y, 0_{R}) \in V$
114	113	a1i	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to if (I = L, x M y, 0_{R}) \in V$
115	106 109 110 114	fvmptd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to (l \in ℕ_{0} ⟼ if (l = L, x M y, 0_{R})) (I) = if (I = L, x M y, 0_{R})$
116	105 115	sylan9eqr	$⊢ ((((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \land (i = x \land j = y)) \to (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I) = if (I = L, x M y, 0_{R})$
117	101 116 95 96 114	ovmpod	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to x (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) y = if (I = L, x M y, 0_{R})$
118		ifov	$⊢ x if (I = L, M, \underset{˙}{0}) y = if (I = L, x M y, x \underset{˙}{0} y)$
119	118	a1i	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to x if (I = L, M, \underset{˙}{0}) y = if (I = L, x M y, x \underset{˙}{0} y)$
120	100 117 119	3eqtr4d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land (x \in N \land y \in N)) \to x (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) y = x if (I = L, M, \underset{˙}{0}) y$
121	120	ralrimivva	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) y = x if (I = L, M, \underset{˙}{0}) y$
122		simplr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to R \in CRing$
123		eqidd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) = (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R}))$
124	107	ifbid	$⊢ l = I \to if (l = L, i M j, 0_{R}) = if (I = L, i M j, 0_{R})$
125	124	adantl	$⊢ ((((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \land l = I) \to if (l = L, i M j, 0_{R}) = if (I = L, i M j, 0_{R})$
126	32	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to I \in ℕ_{0}$
127	54 83	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
128	15 127	syl	$⊢ (N \in Fin \land R \in CRing) \to 0_{R} \in {Base}_{R}$
129	128	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to 0_{R} \in {Base}_{R}$
130	129	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to 0_{R} \in {Base}_{R}$
131	63 130	ifcld	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to if (I = L, i M j, 0_{R}) \in {Base}_{R}$
132	123 125 126 131	fvmptd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I) = if (I = L, i M j, 0_{R})$
133	132 131	eqeltrd	$⊢ (((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \land i \in N \land j \in N) \to (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I) \in {Base}_{R}$
134	3 54 4 10 122 133	matbas2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) \in K$
135	61 58	sylibr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to M \in K$
136	3	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
137	4 5	ring0cl	$⊢ A \in Ring \to \underset{˙}{0} \in K$
138	21 136 137	3syl	$⊢ (N \in Fin \land R \in CRing) \to \underset{˙}{0} \in K$
139	138	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to \underset{˙}{0} \in K$
140	135 139	ifcld	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to if (I = L, M, \underset{˙}{0}) \in K$
141	3 4	eqmat	$⊢ ((i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) \in K \land if (I = L, M, \underset{˙}{0}) \in K) \to ((i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) = if (I = L, M, \underset{˙}{0}) \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) y = x if (I = L, M, \underset{˙}{0}) y)$
142	134 140 141	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to ((i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) = if (I = L, M, \underset{˙}{0}) \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) y = x if (I = L, M, \underset{˙}{0}) y)$
143	121 142	mpbird	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to (i \in N, j \in N ⟼ (l \in ℕ_{0} ⟼ if (l = L, i M j, 0_{R})) (I)) = if (I = L, M, \underset{˙}{0})$
144	34 88 143	3eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in K \land L \in ℕ_{0} \land I \in ℕ_{0})) \to ((L \underset{˙}{\times} X) \underset{˙}{\cdot} T (M)) decompPMat I = if (I = L, M, \underset{˙}{0})$

Metamath Proof Explorer

Theorem monmatcollpw

Proof