decpmataa0

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is 0 for almost all powers. (Contributed by AV, 3-Nov-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	decpmate.p	$⊢ P = {Poly}_{1} (R)$
	decpmate.c	$⊢ C = N Mat P$
	decpmate.b	$⊢ B = {Base}_{C}$
	decpmatcl.a	$⊢ A = N Mat R$
	decpmatfsupp.0	$⊢ \underset{˙}{0} = 0_{A}$
Assertion	decpmataa0	$⊢ (R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to M decompPMat x = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		decpmate.p	$⊢ P = {Poly}_{1} (R)$
2		decpmate.c	$⊢ C = N Mat P$
3		decpmate.b	$⊢ B = {Base}_{C}$
4		decpmatcl.a	$⊢ A = N Mat R$
5		decpmatfsupp.0	$⊢ \underset{˙}{0} = 0_{A}$
6	2 3	matrcl	$⊢ M \in B \to (N \in Fin \land P \in V)$
7	6	simpld	$⊢ M \in B \to N \in Fin$
8	7	adantl	$⊢ (R \in Ring \land M \in B) \to N \in Fin$
9		simpl	$⊢ (R \in Ring \land M \in B) \to R \in Ring$
10		simpr	$⊢ (R \in Ring \land M \in B) \to M \in B$
11		eqid	$⊢ 0_{R} = 0_{R}$
12	1 2 3 11	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) = 0_{R})$
13	8 9 10 12	syl3anc	$⊢ (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) = 0_{R})$
14		eqid	$⊢ {Base}_{A} = {Base}_{A}$
15	1 2 3 4 14	decpmatcl	$⊢ (R \in Ring \land M \in B \land x \in ℕ_{0}) \to M decompPMat x \in {Base}_{A}$
16	15	3expa	$⊢ ((R \in Ring \land M \in B) \land x \in ℕ_{0}) \to M decompPMat x \in {Base}_{A}$
17	8 9	jca	$⊢ (R \in Ring \land M \in B) \to (N \in Fin \land R \in Ring)$
18	4	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
19	14 5	ring0cl	$⊢ A \in Ring \to \underset{˙}{0} \in {Base}_{A}$
20	17 18 19	3syl	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{0} \in {Base}_{A}$
21	20	adantr	$⊢ ((R \in Ring \land M \in B) \land x \in ℕ_{0}) \to \underset{˙}{0} \in {Base}_{A}$
22	4 14	eqmat	$⊢ (M decompPMat x \in {Base}_{A} \land \underset{˙}{0} \in {Base}_{A}) \to (M decompPMat x = \underset{˙}{0} \leftrightarrow \forall i \in N \forall j \in N i (M decompPMat x) j = i \underset{˙}{0} j)$
23	16 21 22	syl2anc	$⊢ ((R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (M decompPMat x = \underset{˙}{0} \leftrightarrow \forall i \in N \forall j \in N i (M decompPMat x) j = i \underset{˙}{0} j)$
24		df-3an	$⊢ (R \in Ring \land M \in B \land x \in ℕ_{0}) \leftrightarrow ((R \in Ring \land M \in B) \land x \in ℕ_{0})$
25	1 2 3	decpmate	$⊢ ((R \in Ring \land M \in B \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to i (M decompPMat x) j = {coe}_{1} (i M j) (x)$
26	24 25	sylanbr	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to i (M decompPMat x) j = {coe}_{1} (i M j) (x)$
27	17	adantr	$⊢ ((R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (N \in Fin \land R \in Ring)$
28	27	adantr	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to (N \in Fin \land R \in Ring)$
29	4 11	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (a \in N, b \in N ⟼ 0_{R})$
30	5 29	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} = (a \in N, b \in N ⟼ 0_{R})$
31	28 30	syl	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to \underset{˙}{0} = (a \in N, b \in N ⟼ 0_{R})$
32		eqidd	$⊢ ((((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \land (a = i \land b = j)) \to 0_{R} = 0_{R}$
33		simpl	$⊢ (i \in N \land j \in N) \to i \in N$
34	33	adantl	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to i \in N$
35		simpr	$⊢ (i \in N \land j \in N) \to j \in N$
36	35	adantl	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to j \in N$
37		fvexd	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to 0_{R} \in V$
38	31 32 34 36 37	ovmpod	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to i \underset{˙}{0} j = 0_{R}$
39	26 38	eqeq12d	$⊢ (((R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to (i (M decompPMat x) j = i \underset{˙}{0} j \leftrightarrow {coe}_{1} (i M j) (x) = 0_{R})$
40	39	2ralbidva	$⊢ ((R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (\forall i \in N \forall j \in N i (M decompPMat x) j = i \underset{˙}{0} j \leftrightarrow \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R})$
41	23 40	bitrd	$⊢ ((R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (M decompPMat x = \underset{˙}{0} \leftrightarrow \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R})$
42	41	imbi2d	$⊢ ((R \in Ring \land M \in B) \land x \in ℕ_{0}) \to ((s < x \to M decompPMat x = \underset{˙}{0}) \leftrightarrow (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R}))$
43	42	ralbidva	$⊢ (R \in Ring \land M \in B) \to (\forall x \in ℕ_{0} (s < x \to M decompPMat x = \underset{˙}{0}) \leftrightarrow \forall x \in ℕ_{0} (s < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R}))$
44	43	rexbidv	$⊢ (R \in Ring \land M \in B) \to (\exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to M decompPMat x = \underset{˙}{0}) \leftrightarrow \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) = 0_{R}))$
45	13 44	mpbird	$⊢ (R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to M decompPMat x = \underset{˙}{0})$

Metamath Proof Explorer

Theorem decpmataa0

Proof