pmatcollpw2lem

Description: Lemma for pmatcollpw2 . (Contributed by AV, 3-Oct-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	pmatcollpw2lem	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{C}} ((n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (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		simp1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to N \in Fin$
8		mpoexga	$⊢ (N \in Fin \land N \in Fin) \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) \in V$
9	7 7 8	syl2anc	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) \in V$
10	9	ralrimivw	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \forall n \in ℕ_{0} (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) \in V$
11		eqid	$⊢ (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) = (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
12	11	fnmpt	$⊢ \forall n \in ℕ_{0} (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) \in V \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) Fn ℕ_{0}$
13	10 12	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) Fn ℕ_{0}$
14		nn0ex	$⊢ ℕ_{0} \in V$
15	14	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ℕ_{0} \in V$
16		fvexd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to 0_{C} \in V$
17		suppvalfn	$⊢ ((n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) Fn ℕ_{0} \land ℕ_{0} \in V \land 0_{C} \in V) \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) supp 0_{C} = \{x \in ℕ_{0} \| (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C}\}$
18	13 15 16 17	syl3anc	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) supp 0_{C} = \{x \in ℕ_{0} \| (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C}\}$
19		eqid	$⊢ 0_{R} = 0_{R}$
20	1 2 3 19	pmatcoe1fsupp	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R})$
21		oveq1	$⊢ {coe}_{1} (i M j) (x) = 0_{R} \to {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X)$
22	4	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{˙}{\times} = \cdot_{P}$
23	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
24	23	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to R = Scalar (P)$
25	24	fveq2d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to 0_{R} = 0_{Scalar (P)}$
26		eqidd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to x \underset{˙}{\times} X = x \underset{˙}{\times} X$
27	22 25 26	oveq123d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{Scalar (P)} \cdot_{P} (x \underset{˙}{\times} X)$
28	27	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{Scalar (P)} \cdot_{P} (x \underset{˙}{\times} X)$
29	24	eqcomd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Scalar (P) = R$
30	29	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to Scalar (P) = R$
31	30	fveq2d	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to 0_{Scalar (P)} = 0_{R}$
32	31	oveq1d	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to 0_{Scalar (P)} \cdot_{P} (x \underset{˙}{\times} X) = 0_{R} \cdot_{P} (x \underset{˙}{\times} X)$
33		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to R \in Ring$
34		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
35		eqid	$⊢ {Base}_{P} = {Base}_{P}$
36	1 6 34 5 35	ply1moncl	$⊢ (R \in Ring \land x \in ℕ_{0}) \to x \underset{˙}{\times} X \in {Base}_{P}$
37	36	3ad2antl2	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to x \underset{˙}{\times} X \in {Base}_{P}$
38	33 37	jca	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (R \in Ring \land x \underset{˙}{\times} X \in {Base}_{P})$
39	38	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \to (R \in Ring \land x \underset{˙}{\times} X \in {Base}_{P})$
40	39	adantr	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to (R \in Ring \land x \underset{˙}{\times} X \in {Base}_{P})$
41		eqid	$⊢ \cdot_{P} = \cdot_{P}$
42	1 35 41 19	ply10s0	$⊢ (R \in Ring \land x \underset{˙}{\times} X \in {Base}_{P}) \to 0_{R} \cdot_{P} (x \underset{˙}{\times} X) = 0_{P}$
43	40 42	syl	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to 0_{R} \cdot_{P} (x \underset{˙}{\times} X) = 0_{P}$
44	28 32 43	3eqtrd	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to 0_{R} \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
45	21 44	sylan9eqr	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \land {coe}_{1} (i M j) (x) = 0_{R}) \to {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
46	45	ex	$⊢ ((((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land i \in N) \land j \in N) \to ({coe}_{1} (i M j) (x) = 0_{R} \to {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
47	46	anasss	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land (i \in N \land j \in N)) \to ({coe}_{1} (i M j) (x) = 0_{R} \to {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
48	47	ralimdvva	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (\forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R} \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
49	48	imim2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to ((y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R}) \to (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
50	49	ralimdva	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R}) \to \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
51	50	reximdv	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) = 0_{R}) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
52	20 51	mpd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
53		simpl3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to M \in B$
54		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to x \in ℕ_{0}$
55	33 53 54	3jca	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (R \in Ring \land M \in B \land x \in ℕ_{0})$
56	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)$
57	55 56	sylan	$⊢ (((N \in Fin \land 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)$
58	57	oveq1d	$⊢ (((N \in Fin \land 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) \underset{˙}{\times} (x \underset{˙}{\times} X) = {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X)$
59	58	eqeq1d	$⊢ (((N \in Fin \land 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) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P} \leftrightarrow {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
60	59	2ralbidva	$⊢ ((N \in Fin \land 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) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P} \leftrightarrow \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
61	60	imbi2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to ((y < x \to \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}) \leftrightarrow (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
62	61	ralbidva	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}) \leftrightarrow \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
63	62	rexbidv	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}) \leftrightarrow \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N {coe}_{1} (i M j) (x) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
64	52 63	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
65		eqid	$⊢ N = N$
66	65	biantrur	$⊢ \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}) \leftrightarrow (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
67	65	biantrur	$⊢ \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P} \leftrightarrow (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
68	67	bicomi	$⊢ (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}) \leftrightarrow \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
69	68	ralbii	$⊢ \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}) \leftrightarrow \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
70	66 69	bitr3i	$⊢ (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})) \leftrightarrow \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}$
71	70	a1i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ((N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})) \leftrightarrow \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})$
72	71	imbi2d	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ((y < x \to (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))) \leftrightarrow (y < x \to \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
73	72	rexralbidv	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))) \leftrightarrow \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \forall i \in N \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))$
74	64 73	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})))$
75		mpoeq123	$⊢ (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P})) \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P})$
76	75	imim2i	$⊢ (y < x \to (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))) \to (y < x \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P}))$
77	76	ralimi	$⊢ \forall x \in ℕ_{0} (y < x \to (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))) \to \forall x \in ℕ_{0} (y < x \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P}))$
78	77	reximi	$⊢ \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (N = N \land \forall i \in N (N = N \land \forall j \in N (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X) = 0_{P}))) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P}))$
79	74 78	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P}))$
80		eqidd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) = (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
81		oveq2	$⊢ n = x \to M decompPMat n = M decompPMat x$
82	81	oveqd	$⊢ n = x \to i (M decompPMat n) j = i (M decompPMat x) j$
83		oveq1	$⊢ n = x \to n \underset{˙}{\times} X = x \underset{˙}{\times} X$
84	82 83	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)$
85	84	mpoeq3dv	$⊢ n = x \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X))$
86	85	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \land n = x) \to (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X))$
87		id	$⊢ N \in Fin \to N \in Fin$
88	87	ancri	$⊢ N \in Fin \to (N \in Fin \land N \in Fin)$
89	88	3ad2ant1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N \in Fin \land N \in Fin)$
90	89	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (N \in Fin \land N \in Fin)$
91		mpoexga	$⊢ (N \in Fin \land N \in Fin) \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) \in V$
92	90 91	syl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) \in V$
93	80 86 54 92	fvmptd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X))$
94	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
95	94	anim2i	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land P \in Ring)$
96	95	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N \in Fin \land P \in Ring)$
97	96	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to (N \in Fin \land P \in Ring)$
98		eqid	$⊢ 0_{P} = 0_{P}$
99	2 98	mat0op	$⊢ (N \in Fin \land P \in Ring) \to 0_{C} = (i \in N, j \in N ⟼ 0_{P})$
100	97 99	syl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to 0_{C} = (i \in N, j \in N ⟼ 0_{P})$
101	93 100	eqeq12d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to ((n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C} \leftrightarrow (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P}))$
102	101	imbi2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land x \in ℕ_{0}) \to ((y < x \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C}) \leftrightarrow (y < x \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P})))$
103	102	ralbidva	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\forall x \in ℕ_{0} (y < x \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C}) \leftrightarrow \forall x \in ℕ_{0} (y < x \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P})))$
104	103	rexbidv	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (\exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C}) \leftrightarrow \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (i \in N, j \in N ⟼ (i (M decompPMat x) j) \underset{˙}{\times} (x \underset{˙}{\times} X)) = (i \in N, j \in N ⟼ 0_{P})))$
105	79 104	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C})$
106		nne	$⊢ \neg (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C} \leftrightarrow (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C}$
107	106	imbi2i	$⊢ (y < x \to \neg (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C}) \leftrightarrow (y < x \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C})$
108	107	ralbii	$⊢ \forall x \in ℕ_{0} (y < x \to \neg (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C}) \leftrightarrow \forall x \in ℕ_{0} (y < x \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C})$
109	108	rexbii	$⊢ \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \neg (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C}) \leftrightarrow \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) = 0_{C})$
110	105 109	sylibr	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \neg (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C})$
111		rabssnn0fi	$⊢ \{x \in ℕ_{0} \| (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C}\} \in Fin \leftrightarrow \exists y \in ℕ_{0} \forall x \in ℕ_{0} (y < x \to \neg (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C})$
112	110 111	sylibr	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \{x \in ℕ_{0} \| (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) (x) \neq 0_{C}\} \in Fin$
113	18 112	eqeltrd	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) supp 0_{C} \in Fin$
114		funmpt	$⊢ Fun (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))$
115	14	mptex	$⊢ (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) \in V$
116		funisfsupp	$⊢ (Fun (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) \land (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) \in V \land 0_{C} \in V) \to ({finSupp}_{0_{C}} ((n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))) \leftrightarrow (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) supp 0_{C} \in Fin)$
117	114 115 16 116	mp3an12i	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ({finSupp}_{0_{C}} ((n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X)))) \leftrightarrow (n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))) supp 0_{C} \in Fin)$
118	113 117	mpbird	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to {finSupp}_{0_{C}} ((n \in ℕ_{0} ⟼ (i \in N, j \in N ⟼ (i (M decompPMat n) j) \underset{˙}{\times} (n \underset{˙}{\times} X))))$

Metamath Proof Explorer

Theorem pmatcollpw2lem

Proof