pmatcoe1fsupp

Description: For a polynomial matrix there is an upper bound for the coefficients of all the polynomials being not 0. (Contributed by AV, 3-Oct-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	pmatcoe1fsupp.p	$⊢ P = {Poly}_{1} (R)$
	pmatcoe1fsupp.c	$⊢ C = N Mat P$
	pmatcoe1fsupp.b	$⊢ B = {Base}_{C}$
	pmatcoe1fsupp.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	pmatcoe1fsupp	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		pmatcoe1fsupp.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcoe1fsupp.c	$⊢ C = N Mat P$
3		pmatcoe1fsupp.b	$⊢ B = {Base}_{C}$
4		pmatcoe1fsupp.0	$⊢ \underset{˙}{0} = 0_{R}$
5		ssrab2	$⊢ \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}}$
6	5	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}}$
7	6	olcd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \subseteq {Base}_{R}^{ℕ_{0}} \lor \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}})$
8		inss	$⊢ (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \subseteq {Base}_{R}^{ℕ_{0}} \lor \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}}) \to ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}}$
9	7 8	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}}$
10		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
11	10	anidms	$⊢ N \in Fin \to N \times N \in Fin$
12		snfi	$⊢ \{{coe}_{1} (M (u))\} \in Fin$
13	12	a1i	$⊢ (N \in Fin \land u \in (N \times N)) \to \{{coe}_{1} (M (u))\} \in Fin$
14	13	ralrimiva	$⊢ N \in Fin \to \forall u \in (N \times N) \{{coe}_{1} (M (u))\} \in Fin$
15	11 14	jca	$⊢ N \in Fin \to (N \times N \in Fin \land \forall u \in (N \times N) \{{coe}_{1} (M (u))\} \in Fin)$
16	15	3ad2ant1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N \times N \in Fin \land \forall u \in (N \times N) \{{coe}_{1} (M (u))\} \in Fin)$
17		iunfi	$⊢ (N \times N \in Fin \land \forall u \in (N \times N) \{{coe}_{1} (M (u))\} \in Fin) \to ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \in Fin$
18		infi	$⊢ ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \in Fin \to ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \in Fin$
19	16 17 18	3syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \in Fin$
20		fvex	$⊢ 0_{R} \in V$
21	4 20	eqeltri	$⊢ \underset{˙}{0} \in V$
22	21	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{˙}{0} \in V$
23		elin	$⊢ w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \leftrightarrow (w \in ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \land w \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\})$
24		breq1	$⊢ v = w \to ({finSupp}_{\underset{˙}{0}} (v) \leftrightarrow {finSupp}_{\underset{˙}{0}} (w))$
25	24	elrab	$⊢ w \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \leftrightarrow (w \in ({Base}_{R}^{ℕ_{0}}) \land {finSupp}_{\underset{˙}{0}} (w))$
26	25	simprbi	$⊢ w \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \to {finSupp}_{\underset{˙}{0}} (w)$
27	23 26	simplbiim	$⊢ w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \to {finSupp}_{\underset{˙}{0}} (w)$
28	27	rgen	$⊢ \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) {finSupp}_{\underset{˙}{0}} (w)$
29	28	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) {finSupp}_{\underset{˙}{0}} (w)$
30		fsuppmapnn0fiub0	$⊢ (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}} \land ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \in Fin \land \underset{˙}{0} \in V) \to (\forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) {finSupp}_{\underset{˙}{0}} (w) \to \exists s \in ℕ_{0} \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0}))$
31	30	imp	$⊢ ((⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \subseteq {Base}_{R}^{ℕ_{0}} \land ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \in Fin \land \underset{˙}{0} \in V) \land \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) {finSupp}_{\underset{˙}{0}} (w)) \to \exists s \in ℕ_{0} \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0})$
32	9 19 22 29 31	syl31anc	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0})$
33		opelxpi	$⊢ (i \in N \land j \in N) \to ⟨i, j⟩ \in (N \times N)$
34		df-ov	$⊢ i M j = M (⟨i, j⟩)$
35	34	fveq2i	$⊢ {coe}_{1} (i M j) = {coe}_{1} (M (⟨i, j⟩))$
36		fvex	$⊢ {coe}_{1} (M (⟨i, j⟩)) \in V$
37	36	snid	$⊢ {coe}_{1} (M (⟨i, j⟩)) \in \{{coe}_{1} (M (⟨i, j⟩))\}$
38	35 37	eqeltri	$⊢ {coe}_{1} (i M j) \in \{{coe}_{1} (M (⟨i, j⟩))\}$
39	38	a1i	$⊢ (i \in N \land j \in N) \to {coe}_{1} (i M j) \in \{{coe}_{1} (M (⟨i, j⟩))\}$
40		2fveq3	$⊢ u = ⟨i, j⟩ \to {coe}_{1} (M (u)) = {coe}_{1} (M (⟨i, j⟩))$
41	40	sneqd	$⊢ u = ⟨i, j⟩ \to \{{coe}_{1} (M (u))\} = \{{coe}_{1} (M (⟨i, j⟩))\}$
42	41	eliuni	$⊢ (⟨i, j⟩ \in (N \times N) \land {coe}_{1} (i M j) \in \{{coe}_{1} (M (⟨i, j⟩))\}) \to {coe}_{1} (i M j) \in ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\}$
43	33 39 42	syl2anc	$⊢ (i \in N \land j \in N) \to {coe}_{1} (i M j) \in ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\}$
44	43	adantl	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to {coe}_{1} (i M j) \in ⋃_{u \in N \times N} \{{coe}_{1} (M (u))\}$
45		eqid	$⊢ {Base}_{P} = {Base}_{P}$
46		simprl	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to i \in N$
47		simprr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to j \in N$
48	3	eleq2i	$⊢ M \in B \leftrightarrow M \in {Base}_{C}$
49	48	biimpi	$⊢ M \in B \to M \in {Base}_{C}$
50	49	3ad2ant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to M \in {Base}_{C}$
51	50	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to M \in {Base}_{C}$
52	51 3	eleqtrrdi	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to M \in B$
53	2 45 3 46 47 52	matecld	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to i M j \in {Base}_{P}$
54		eqid	$⊢ {coe}_{1} (i M j) = {coe}_{1} (i M j)$
55		eqid	$⊢ 0_{R} = 0_{R}$
56		eqid	$⊢ {Base}_{R} = {Base}_{R}$
57	54 45 1 55 56	coe1fsupp	$⊢ i M j \in {Base}_{P} \to {coe}_{1} (i M j) \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{0_{R}} (v)\}$
58	53 57	syl	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to {coe}_{1} (i M j) \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{0_{R}} (v)\}$
59	4	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{˙}{0} = 0_{R}$
60	59	breq2d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ({finSupp}_{\underset{˙}{0}} (v) \leftrightarrow {finSupp}_{0_{R}} (v))$
61	60	rabbidv	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} = \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{0_{R}} (v)\}$
62	61	eleq2d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ({coe}_{1} (i M j) \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \leftrightarrow {coe}_{1} (i M j) \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{0_{R}} (v)\})$
63	62	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to ({coe}_{1} (i M j) \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\} \leftrightarrow {coe}_{1} (i M j) \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{0_{R}} (v)\})$
64	58 63	mpbird	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to {coe}_{1} (i M j) \in \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}$
65	44 64	elind	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to {coe}_{1} (i M j) \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\})$
66		simplr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to x \in ℕ_{0}$
67		fveq1	$⊢ w = {coe}_{1} (i M j) \to w (z) = {coe}_{1} (i M j) (z)$
68	67	eqeq1d	$⊢ w = {coe}_{1} (i M j) \to (w (z) = \underset{˙}{0} \leftrightarrow {coe}_{1} (i M j) (z) = \underset{˙}{0})$
69	68	imbi2d	$⊢ w = {coe}_{1} (i M j) \to ((s < z \to w (z) = \underset{˙}{0}) \leftrightarrow (s < z \to {coe}_{1} (i M j) (z) = \underset{˙}{0}))$
70		breq2	$⊢ z = x \to (s < z \leftrightarrow s < x)$
71		fveqeq2	$⊢ z = x \to ({coe}_{1} (i M j) (z) = \underset{˙}{0} \leftrightarrow {coe}_{1} (i M j) (x) = \underset{˙}{0})$
72	70 71	imbi12d	$⊢ z = x \to ((s < z \to {coe}_{1} (i M j) (z) = \underset{˙}{0}) \leftrightarrow (s < x \to {coe}_{1} (i M j) (x) = \underset{˙}{0}))$
73	69 72	rspc2v	$⊢ ({coe}_{1} (i M j) \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \land x \in ℕ_{0}) \to (\forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0}) \to (s < x \to {coe}_{1} (i M j) (x) = \underset{˙}{0}))$
74	65 66 73	syl2anc	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to (\forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0}) \to (s < x \to {coe}_{1} (i M j) (x) = \underset{˙}{0}))$
75	74	ex	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to ((i \in N \land j \in N) \to (\forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0}) \to (s < x \to {coe}_{1} (i M j) (x) = \underset{˙}{0})))$
76	75	com23	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to (\forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0}) \to ((i \in N \land j \in N) \to (s < x \to {coe}_{1} (i M j) (x) = \underset{˙}{0})))$
77	76	impancom	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0})) \to (x \in ℕ_{0} \to ((i \in N \land j \in N) \to (s < x \to {coe}_{1} (i M j) (x) = \underset{˙}{0})))$
78	77	imp	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0})) \land x \in ℕ_{0}) \to ((i \in N \land j \in N) \to (s < x \to {coe}_{1} (i M j) (x) = \underset{˙}{0}))$
79	78	com23	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0})) \land x \in ℕ_{0}) \to (s < x \to ((i \in N \land j \in N) \to {coe}_{1} (i M j) (x) = \underset{˙}{0}))$
80	79	ralrimdvv	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0})) \land x \in ℕ_{0}) \to (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = \underset{˙}{0})$
81	80	ralrimiva	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \land \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0})) \to \forall x \in ℕ_{0} (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = \underset{˙}{0})$
82	81	ex	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land s \in ℕ_{0}) \to (\forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0}) \to \forall x \in ℕ_{0} (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = \underset{˙}{0}))$
83	82	reximdva	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\exists s \in ℕ_{0} \forall w \in (⋃_{u \in N \times N} \{{coe}_{1} (M (u))\} \cap \{v \in ({Base}_{R}^{ℕ_{0}}) \| {finSupp}_{\underset{˙}{0}} (v)\}) \forall z \in ℕ_{0} (s < z \to w (z) = \underset{˙}{0}) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = \underset{˙}{0}))$
84	32 83	mpd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem pmatcoe1fsupp

Proof