mptcoe1matfsupp

Description: The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019) (Proof shortened by AV, 23-Dec-2019)

	Ref	Expression
Hypotheses	mptcoe1matfsupp.a	$⊢ A = N Mat R$
	mptcoe1matfsupp.q	$⊢ Q = {Poly}_{1} (A)$
	mptcoe1matfsupp.l	$⊢ L = {Base}_{Q}$
Assertion	mptcoe1matfsupp	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {finSupp}_{0_{R}} ((k \in ℕ_{0} ⟼ I {coe}_{1} (O) (k) J))$

Proof

Step	Hyp	Ref	Expression
1		mptcoe1matfsupp.a	$⊢ A = N Mat R$
2		mptcoe1matfsupp.q	$⊢ Q = {Poly}_{1} (A)$
3		mptcoe1matfsupp.l	$⊢ L = {Base}_{Q}$
4		fvexd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to 0_{R} \in V$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ {Base}_{A} = {Base}_{A}$
7		simp2	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to I \in N$
8	7	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to I \in N$
9		simp3	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to J \in N$
10	9	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to J \in N$
11		simp3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to O \in L$
12	11	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to O \in L$
13		eqid	$⊢ {coe}_{1} (O) = {coe}_{1} (O)$
14	13 3 2 6	coe1fvalcl	$⊢ (O \in L \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
15	12 14	sylan	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
16	1 5 6 8 10 15	matecld	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to I {coe}_{1} (O) (k) J \in {Base}_{R}$
17		eqid	$⊢ 0_{A} = 0_{A}$
18	13 3 2 17 6	coe1fsupp	$⊢ O \in L \to {coe}_{1} (O) \in \{c \in ({Base}_{A}^{ℕ_{0}}) \| {finSupp}_{0_{A}} (c)\}$
19		elrabi	$⊢ {coe}_{1} (O) \in \{c \in ({Base}_{A}^{ℕ_{0}}) \| {finSupp}_{0_{A}} (c)\} \to {coe}_{1} (O) \in ({Base}_{A}^{ℕ_{0}})$
20	12 18 19	3syl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {coe}_{1} (O) \in ({Base}_{A}^{ℕ_{0}})$
21		fvex	$⊢ 0_{A} \in V$
22	20 21	jctir	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to ({coe}_{1} (O) \in ({Base}_{A}^{ℕ_{0}}) \land 0_{A} \in V)$
23	13 3 2 17	coe1sfi	$⊢ O \in L \to {finSupp}_{0_{A}} ({coe}_{1} (O))$
24	12 23	syl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {finSupp}_{0_{A}} ({coe}_{1} (O))$
25		fsuppmapnn0ub	$⊢ ({coe}_{1} (O) \in ({Base}_{A}^{ℕ_{0}}) \land 0_{A} \in V) \to ({finSupp}_{0_{A}} ({coe}_{1} (O)) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))$
26	22 24 25	sylc	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})$
27		csbov	$⊢ ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = I ⦋ x / k ⦌ {coe}_{1} (O) (k) J$
28		csbfv	$⊢ ⦋ x / k ⦌ {coe}_{1} (O) (k) = {coe}_{1} (O) (x)$
29	28	oveqi	$⊢ I ⦋ x / k ⦌ {coe}_{1} (O) (k) J = I {coe}_{1} (O) (x) J$
30	27 29	eqtri	$⊢ ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = I {coe}_{1} (O) (x) J$
31	30	a1i	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land s < x) \land {coe}_{1} (O) (x) = 0_{A}) \to ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = I {coe}_{1} (O) (x) J$
32		oveq	$⊢ {coe}_{1} (O) (x) = 0_{A} \to I {coe}_{1} (O) (x) J = I 0_{A} J$
33	32	adantl	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land s < x) \land {coe}_{1} (O) (x) = 0_{A}) \to I {coe}_{1} (O) (x) J = I 0_{A} J$
34		eqid	$⊢ 0_{R} = 0_{R}$
35	1 34	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
36	35	3adant3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
37	36	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
38		eqidd	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land (i = I \land j = J)) \to 0_{R} = 0_{R}$
39	37 38 7 9 4	ovmpod	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to I 0_{A} J = 0_{R}$
40	39	ad4antr	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land s < x) \land {coe}_{1} (O) (x) = 0_{A}) \to I 0_{A} J = 0_{R}$
41	31 33 40	3eqtrd	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \land s < x) \land {coe}_{1} (O) (x) = 0_{A}) \to ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = 0_{R}$
42	41	exp31	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to (s < x \to ({coe}_{1} (O) (x) = 0_{A} \to ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = 0_{R}))$
43	42	a2d	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land s \in ℕ_{0}) \land x \in ℕ_{0}) \to ((s < x \to {coe}_{1} (O) (x) = 0_{A}) \to (s < x \to ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = 0_{R}))$
44	43	ralimdva	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land s \in ℕ_{0}) \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}) \to \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = 0_{R}))$
45	44	reximdva	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to (\exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = 0_{R}))$
46	26 45	mpd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to ⦋ x / k ⦌ (I {coe}_{1} (O) (k) J) = 0_{R})$
47	4 16 46	mptnn0fsupp	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {finSupp}_{0_{R}} ((k \in ℕ_{0} ⟼ I {coe}_{1} (O) (k) J))$

Metamath Proof Explorer

Theorem mptcoe1matfsupp

Proof