pmatcollpw1lem1

Description: Lemma 1 for pmatcollpw1 . (Contributed by AV, 28-Sep-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw1.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpw1.c	$⊢ C = N Mat P$
	pmatcollpw1.b	$⊢ B = {Base}_{C}$
	pmatcollpw1.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
	pmatcollpw1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpw1.x	$⊢ X = {var}_{1} (R)$
Assertion	pmatcollpw1lem1	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to {finSupp}_{0_{P}} ((n \in ℕ_{0} ⟼ (I (M decompPMat n) J) \underset{˙}{\times} (n \underset{˙}{\times} X)))$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw1.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpw1.c	$⊢ C = N Mat P$
3		pmatcollpw1.b	$⊢ B = {Base}_{C}$
4		pmatcollpw1.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
5		pmatcollpw1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpw1.x	$⊢ X = {var}_{1} (R)$
7		fvexd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to 0_{P} \in V$
8		ovexd	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land n \in ℕ_{0}) \to (I (M decompPMat n) J) \underset{˙}{\times} (n \underset{˙}{\times} X) \in V$
9		oveq2	$⊢ n = x \to M decompPMat n = M decompPMat x$
10	9	oveqd	$⊢ n = x \to I (M decompPMat n) J = I (M decompPMat x) J$
11		oveq1	$⊢ n = x \to n \underset{˙}{\times} X = x \underset{˙}{\times} X$
12	10 11	oveq12d	$⊢ n = x \to (I (M decompPMat n) J) \underset{˙}{\times} (n \underset{˙}{\times} X) = (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X)$
13		eqid	$⊢ {Base}_{P} = {Base}_{P}$
14		simp2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to I \in N$
15		simp3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to J \in N$
16		simp13	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to M \in B$
17	2 13 3 14 15 16	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to I M J \in {Base}_{P}$
18		eqid	$⊢ {coe}_{1} (I M J) = {coe}_{1} (I M J)$
19		eqid	$⊢ 0_{R} = 0_{R}$
20	18 13 1 19	coe1ae0	$⊢ I M J \in {Base}_{P} \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (I M J) (x) = 0_{R})$
21	17 20	syl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (I M J) (x) = 0_{R})$
22		simpl12	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to R \in Ring$
23	16	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to M \in B$
24		simpr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to x \in ℕ_{0}$
25		3simpc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to (I \in N \land J \in N)$
26	25	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to (I \in N \land J \in N)$
27	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)$
28	22 23 24 26 27	syl31anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to I (M decompPMat x) J = {coe}_{1} (I M J) (x)$
29	28	adantr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \land {coe}_{1} (I M J) (x) = 0_{R}) \to I (M decompPMat x) J = {coe}_{1} (I M J) (x)$
30		simpr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \land {coe}_{1} (I M J) (x) = 0_{R}) \to {coe}_{1} (I M J) (x) = 0_{R}$
31	29 30	eqtrd	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \land {coe}_{1} (I M J) (x) = 0_{R}) \to I (M decompPMat x) J = 0_{R}$
32	31	oveq1d	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \land {coe}_{1} (I M J) (x) = 0_{R}) \to (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X)$
33		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
34	1 6 33 5 13	ply1moncl	$⊢ (R \in Ring \land x \in ℕ_{0}) \to x \underset{˙}{\times} X \in {Base}_{P}$
35	22 24 34	syl2anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to x \underset{˙}{\times} X \in {Base}_{P}$
36	1 13 4 19	ply10s0	$⊢ (R \in Ring \land x \underset{˙}{\times} X \in {Base}_{P}) \to 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
37	22 35 36	syl2anc	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
38	37	adantr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \land {coe}_{1} (I M J) (x) = 0_{R}) \to 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
39	32 38	eqtrd	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \land {coe}_{1} (I M J) (x) = 0_{R}) \to (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
40	39	ex	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to ({coe}_{1} (I M J) (x) = 0_{R} \to (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
41	40	imim2d	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \land x \in ℕ_{0}) \to ((s < x \to {coe}_{1} (I M J) (x) = 0_{R}) \to (s < x \to (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
42	41	ralimdva	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (I M J) (x) = 0_{R}) \to \forall x \in ℕ_{0} (s < x \to (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
43	42	reximdv	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to (\exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (I M J) (x) = 0_{R}) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
44	21 43	mpd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to (I (M decompPMat x) J) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
45	7 8 12 44	mptnn0fsuppd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land I \in N \land J \in N) \to {finSupp}_{0_{P}} ((n \in ℕ_{0} ⟼ (I (M decompPMat n) J) \underset{˙}{\times} (n \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem pmatcollpw1lem1

Proof