mp2pm2mplem4

Description: Lemma 4 for mp2pm2mp . (Contributed by AV, 12-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	mp2pm2mp.a	$⊢ A = N Mat R$
	mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
	mp2pm2mp.l	$⊢ L = {Base}_{Q}$
	mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
	mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
	mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
	mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
Assertion	mp2pm2mplem4	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to I (O) decompPMat K = {coe}_{1} (O) (K)$

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	$⊢ A = N Mat R$
2		mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
3		mp2pm2mp.l	$⊢ L = {Base}_{Q}$
4		mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
6		mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
7		mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
8		mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
9	1 2 3 4 5 6 7 8	mp2pm2mplem3	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to I (O) decompPMat K = (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K))$
10		eqid	$⊢ {Base}_{P} = {Base}_{P}$
11		eqid	$⊢ 0_{P} = 0_{P}$
12	8	ply1ring	$⊢ R \in Ring \to P \in Ring$
13	12	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in Ring$
14		ringcmn	$⊢ P \in Ring \to P \in CMnd$
15	13 14	syl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in CMnd$
16	15	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to P \in CMnd$
17	16	3ad2ant1	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to P \in CMnd$
18		simpl2	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to R \in Ring$
19	18	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to R \in Ring$
20	19	3ad2ant1	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to R \in Ring$
21	20	adantr	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to R \in Ring$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23		eqid	$⊢ {Base}_{A} = {Base}_{A}$
24		simpl2	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to i \in N$
25		simpl3	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to j \in N$
26		simpl3	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to O \in L$
27	26	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to O \in L$
28	27	3ad2ant1	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to O \in L$
29		eqid	$⊢ {coe}_{1} (O) = {coe}_{1} (O)$
30	29 3 2 23	coe1fvalcl	$⊢ (O \in L \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
31	28 30	sylan	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
32	1 22 23 24 25 31	matecld	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to i {coe}_{1} (O) (k) j \in {Base}_{R}$
33		simpr	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
34		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
35	22 8 6 4 34 5 10	ply1tmcl	$⊢ (R \in Ring \land i {coe}_{1} (O) (k) j \in {Base}_{R} \land k \in ℕ_{0}) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
36	21 32 33 35	syl3anc	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
37	36	ralrimiva	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to \forall k \in ℕ_{0} (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
38		simp1lr	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to s \in ℕ_{0}$
39		oveq	$⊢ {coe}_{1} (O) (x) = 0_{A} \to i {coe}_{1} (O) (x) j = i 0_{A} j$
40	39	oveq1d	$⊢ {coe}_{1} (O) (x) = 0_{A} \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = (i 0_{A} j) \underset{˙}{\cdot} (x E Y)$
41		3simpa	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (N \in Fin \land R \in Ring)$
42	41	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \to (N \in Fin \land R \in Ring)$
43		eqid	$⊢ 0_{R} = 0_{R}$
44	1 43	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (a \in N, b \in N ⟼ 0_{R})$
45	42 44	syl	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \to 0_{A} = (a \in N, b \in N ⟼ 0_{R})$
46		eqidd	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land (a = i \land b = j)) \to 0_{R} = 0_{R}$
47		simprl	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \to i \in N$
48		simprr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \to j \in N$
49		fvexd	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \to 0_{R} \in V$
50	45 46 47 48 49	ovmpod	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \to i 0_{A} j = 0_{R}$
51	50	adantr	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to i 0_{A} j = 0_{R}$
52	51	oveq1d	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to (i 0_{A} j) \underset{˙}{\cdot} (x E Y) = 0_{R} \underset{˙}{\cdot} (x E Y)$
53	18	ad3antrrr	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to R \in Ring$
54	8	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
55	53 54	syl	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to R = Scalar (P)$
56	55	fveq2d	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to 0_{R} = 0_{Scalar (P)}$
57	56	oveq1d	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to 0_{R} \underset{˙}{\cdot} (x E Y) = 0_{Scalar (P)} \underset{˙}{\cdot} (x E Y)$
58	8	ply1lmod	$⊢ R \in Ring \to P \in LMod$
59	58	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in LMod$
60	59	ad4antr	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to P \in LMod$
61		simpr	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to x \in ℕ_{0}$
62	8 6 34 5 10	ply1moncl	$⊢ (R \in Ring \land x \in ℕ_{0}) \to x E Y \in {Base}_{P}$
63	53 61 62	syl2anc	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to x E Y \in {Base}_{P}$
64		eqid	$⊢ Scalar (P) = Scalar (P)$
65		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
66	10 64 4 65 11	lmod0vs	$⊢ (P \in LMod \land x E Y \in {Base}_{P}) \to 0_{Scalar (P)} \underset{˙}{\cdot} (x E Y) = 0_{P}$
67	60 63 66	syl2anc	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to 0_{Scalar (P)} \underset{˙}{\cdot} (x E Y) = 0_{P}$
68	52 57 67	3eqtrd	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to (i 0_{A} j) \underset{˙}{\cdot} (x E Y) = 0_{P}$
69	68	adantr	$⊢ ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \land s < x) \to (i 0_{A} j) \underset{˙}{\cdot} (x E Y) = 0_{P}$
70	40 69	sylan9eqr	$⊢ (((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \land s < x) \land {coe}_{1} (O) (x) = 0_{A}) \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P}$
71	70	exp31	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to (s < x \to ({coe}_{1} (O) (x) = 0_{A} \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P}))$
72	71	a2d	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \land x \in ℕ_{0}) \to ((s < x \to {coe}_{1} (O) (x) = 0_{A}) \to (s < x \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P}))$
73	72	ralimdva	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land (i \in N \land j \in N)) \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}) \to \forall x \in ℕ_{0} (s < x \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P}))$
74	73	impancom	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to ((i \in N \land j \in N) \to \forall x \in ℕ_{0} (s < x \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P}))$
75	74	3impib	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to \forall x \in ℕ_{0} (s < x \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P})$
76		breq2	$⊢ k = x \to (s < k \leftrightarrow s < x)$
77		fveq2	$⊢ k = x \to {coe}_{1} (O) (k) = {coe}_{1} (O) (x)$
78	77	oveqd	$⊢ k = x \to i {coe}_{1} (O) (k) j = i {coe}_{1} (O) (x) j$
79		oveq1	$⊢ k = x \to k E Y = x E Y$
80	78 79	oveq12d	$⊢ k = x \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) = (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y)$
81	80	eqeq1d	$⊢ k = x \to ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) = 0_{P} \leftrightarrow (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P})$
82	76 81	imbi12d	$⊢ k = x \to ((s < k \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) = 0_{P}) \leftrightarrow (s < x \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P}))$
83	82	cbvralvw	$⊢ \forall k \in ℕ_{0} (s < k \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) = 0_{P}) \leftrightarrow \forall x \in ℕ_{0} (s < x \to (i {coe}_{1} (O) (x) j) \underset{˙}{\cdot} (x E Y) = 0_{P})$
84	75 83	sylibr	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to \forall k \in ℕ_{0} (s < k \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) = 0_{P})$
85	10 11 17 37 38 84	gsummptnn0fz	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) = {\sum_{P}}_{k = 0}^{s} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))$
86	85	fveq2d	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) = {coe}_{1} ({\sum_{P}}_{k = 0}^{s} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)))$
87	86	fveq1d	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K) = {coe}_{1} ({\sum_{P}}_{k = 0}^{s} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K)$
88		simpllr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to K \in ℕ_{0}$
89	88	3ad2ant1	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to K \in ℕ_{0}$
90	36	expcom	$⊢ k \in ℕ_{0} \to ((((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P})$
91		elfznn0	$⊢ k \in (0 \dots s) \to k \in ℕ_{0}$
92	90 91	syl11	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to (k \in (0 \dots s) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P})$
93	92	ralrimiv	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to \forall k \in (0 \dots s) (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
94		fzfid	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to (0 \dots s) \in Fin$
95	8 10 20 89 93 94	coe1fzgsumd	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to {coe}_{1} ({\sum_{P}}_{k = 0}^{s} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K) = {\sum_{R}}_{k = 0}^{s} {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K)$
96	87 95	eqtrd	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \land i \in N \land j \in N) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K) = {\sum_{R}}_{k = 0}^{s} {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K)$
97	96	mpoeq3dva	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K)) = (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K))$
98	18	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to R \in Ring$
99	98	adantr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to R \in Ring$
100		simpl2	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to i \in N$
101		simpl3	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to j \in N$
102	26	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to O \in L$
103	102 91 30	syl2an	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to {coe}_{1} (O) (k) \in {Base}_{A}$
104	1 22 23 100 101 103	matecld	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to i {coe}_{1} (O) (k) j \in {Base}_{R}$
105	91	adantl	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to k \in ℕ_{0}$
106	43 22 8 6 4 34 5	coe1tm	$⊢ (R \in Ring \land i {coe}_{1} (O) (k) j \in {Base}_{R} \land k \in ℕ_{0}) \to {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) = (l \in ℕ_{0} ⟼ if (l = k, i {coe}_{1} (O) (k) j, 0_{R}))$
107	99 104 105 106	syl3anc	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) = (l \in ℕ_{0} ⟼ if (l = k, i {coe}_{1} (O) (k) j, 0_{R}))$
108		eqeq1	$⊢ l = K \to (l = k \leftrightarrow K = k)$
109	108	ifbid	$⊢ l = K \to if (l = k, i {coe}_{1} (O) (k) j, 0_{R}) = if (K = k, i {coe}_{1} (O) (k) j, 0_{R})$
110	109	adantl	$⊢ (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \land l = K) \to if (l = k, i {coe}_{1} (O) (k) j, 0_{R}) = if (K = k, i {coe}_{1} (O) (k) j, 0_{R})$
111		simpl1r	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to K \in ℕ_{0}$
112		ovex	$⊢ i {coe}_{1} (O) (k) j \in V$
113		fvex	$⊢ 0_{R} \in V$
114	112 113	ifex	$⊢ if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) \in V$
115	114	a1i	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) \in V$
116	107 110 111 115	fvmptd	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K) = if (K = k, i {coe}_{1} (O) (k) j, 0_{R})$
117	116	mpteq2dva	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to (k \in (0 \dots s) ⟼ {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K)) = (k \in (0 \dots s) ⟼ if (K = k, i {coe}_{1} (O) (k) j, 0_{R}))$
118	117	oveq2d	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to {\sum_{R}}_{k = 0}^{s} {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K) = {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})$
119	118	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K)) = (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R}))$
120	119	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} {coe}_{1} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) (K)) = (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R}))$
121		breq2	$⊢ x = K \to (s < x \leftrightarrow s < K)$
122		fveqeq2	$⊢ x = K \to ({coe}_{1} (O) (x) = 0_{A} \leftrightarrow {coe}_{1} (O) (K) = 0_{A})$
123	121 122	imbi12d	$⊢ x = K \to ((s < x \to {coe}_{1} (O) (x) = 0_{A}) \leftrightarrow (s < K \to {coe}_{1} (O) (K) = 0_{A}))$
124	123	rspcva	$⊢ (K \in ℕ_{0} \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (s < K \to {coe}_{1} (O) (K) = 0_{A})$
125	1 43	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (i \in N, j \in N ⟼ 0_{R})$
126	125	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to (i \in N, j \in N ⟼ 0_{R}) = 0_{A}$
127	126	3adant3	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (i \in N, j \in N ⟼ 0_{R}) = 0_{A}$
128	127	ad3antlr	$⊢ (((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \to (i \in N, j \in N ⟼ 0_{R}) = 0_{A}$
129		elfz2nn0	$⊢ k \in (0 \dots s) \leftrightarrow (k \in ℕ_{0} \land s \in ℕ_{0} \land k \leq s)$
130		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
131	130	ad2antrr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \to k \in ℝ$
132		nn0re	$⊢ s \in ℕ_{0} \to s \in ℝ$
133	132	ad2antlr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \to s \in ℝ$
134		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
135	134	adantl	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \to K \in ℝ$
136		lelttr	$⊢ (k \in ℝ \land s \in ℝ \land K \in ℝ) \to ((k \leq s \land s < K) \to k < K)$
137	131 133 135 136	syl3anc	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \to ((k \leq s \land s < K) \to k < K)$
138		animorr	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \land k < K) \to (K < k \lor k < K)$
139		df-ne	$⊢ K \neq k \leftrightarrow \neg K = k$
140	130	adantr	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to k \in ℝ$
141		lttri2	$⊢ (K \in ℝ \land k \in ℝ) \to (K \neq k \leftrightarrow (K < k \lor k < K))$
142	134 140 141	syl2anr	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \to (K \neq k \leftrightarrow (K < k \lor k < K))$
143	142	adantr	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \land k < K) \to (K \neq k \leftrightarrow (K < k \lor k < K))$
144	139 143	bitr3id	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \land k < K) \to (\neg K = k \leftrightarrow (K < k \lor k < K))$
145	138 144	mpbird	$⊢ (((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \land k < K) \to \neg K = k$
146	145	ex	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \to (k < K \to \neg K = k)$
147	137 146	syld	$⊢ ((k \in ℕ_{0} \land s \in ℕ_{0}) \land K \in ℕ_{0}) \to ((k \leq s \land s < K) \to \neg K = k)$
148	147	exp4b	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to (K \in ℕ_{0} \to (k \leq s \to (s < K \to \neg K = k)))$
149	148	com24	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0}) \to (s < K \to (k \leq s \to (K \in ℕ_{0} \to \neg K = k)))$
150	149	expimpd	$⊢ k \in ℕ_{0} \to ((s \in ℕ_{0} \land s < K) \to (k \leq s \to (K \in ℕ_{0} \to \neg K = k)))$
151	150	com23	$⊢ k \in ℕ_{0} \to (k \leq s \to ((s \in ℕ_{0} \land s < K) \to (K \in ℕ_{0} \to \neg K = k)))$
152	151	imp	$⊢ (k \in ℕ_{0} \land k \leq s) \to ((s \in ℕ_{0} \land s < K) \to (K \in ℕ_{0} \to \neg K = k))$
153	152	3adant2	$⊢ (k \in ℕ_{0} \land s \in ℕ_{0} \land k \leq s) \to ((s \in ℕ_{0} \land s < K) \to (K \in ℕ_{0} \to \neg K = k))$
154	129 153	sylbi	$⊢ k \in (0 \dots s) \to ((s \in ℕ_{0} \land s < K) \to (K \in ℕ_{0} \to \neg K = k))$
155	154	com13	$⊢ K \in ℕ_{0} \to ((s \in ℕ_{0} \land s < K) \to (k \in (0 \dots s) \to \neg K = k))$
156	155	adantr	$⊢ (K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \to ((s \in ℕ_{0} \land s < K) \to (k \in (0 \dots s) \to \neg K = k))$
157	156	imp	$⊢ ((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \to (k \in (0 \dots s) \to \neg K = k)$
158	157	adantr	$⊢ (((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \to (k \in (0 \dots s) \to \neg K = k)$
159	158	3ad2ant1	$⊢ ((((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \land i \in N \land j \in N) \to (k \in (0 \dots s) \to \neg K = k)$
160	159	imp	$⊢ (((((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to \neg K = k$
161	160	iffalsed	$⊢ (((((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) = 0_{R}$
162	161	mpteq2dva	$⊢ ((((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \land i \in N \land j \in N) \to (k \in (0 \dots s) ⟼ if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = (k \in (0 \dots s) ⟼ 0_{R})$
163	162	oveq2d	$⊢ ((((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \land i \in N \land j \in N) \to {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) = {\sum_{R}}_{k = 0}^{s} 0_{R}$
164		ringmnd	$⊢ R \in Ring \to R \in Mnd$
165	164	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to R \in Mnd$
166		ovex	$⊢ (0 \dots s) \in V$
167	43	gsumz	$⊢ (R \in Mnd \land (0 \dots s) \in V) \to {\sum_{R}}_{k = 0}^{s} 0_{R} = 0_{R}$
168	165 166 167	sylancl	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {\sum_{R}}_{k = 0}^{s} 0_{R} = 0_{R}$
169	168	ad3antlr	$⊢ (((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \to {\sum_{R}}_{k = 0}^{s} 0_{R} = 0_{R}$
170	169	3ad2ant1	$⊢ ((((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \land i \in N \land j \in N) \to {\sum_{R}}_{k = 0}^{s} 0_{R} = 0_{R}$
171	163 170	eqtrd	$⊢ ((((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \land i \in N \land j \in N) \to {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) = 0_{R}$
172	171	mpoeq3dva	$⊢ (((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = (i \in N, j \in N ⟼ 0_{R})$
173		simpr	$⊢ (((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \to {coe}_{1} (O) (K) = 0_{A}$
174	128 172 173	3eqtr4d	$⊢ (((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \land {coe}_{1} (O) (K) = 0_{A}) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)$
175	174	ex	$⊢ ((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land (s \in ℕ_{0} \land s < K)) \to ({coe}_{1} (O) (K) = 0_{A} \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K))$
176	175	expr	$⊢ ((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land s \in ℕ_{0}) \to (s < K \to ({coe}_{1} (O) (K) = 0_{A} \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)))$
177	176	a2d	$⊢ ((K \in ℕ_{0} \land (N \in Fin \land R \in Ring \land O \in L)) \land s \in ℕ_{0}) \to ((s < K \to {coe}_{1} (O) (K) = 0_{A}) \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)))$
178	177	exp31	$⊢ K \in ℕ_{0} \to ((N \in Fin \land R \in Ring \land O \in L) \to (s \in ℕ_{0} \to ((s < K \to {coe}_{1} (O) (K) = 0_{A}) \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)))))$
179	178	com14	$⊢ (s < K \to {coe}_{1} (O) (K) = 0_{A}) \to ((N \in Fin \land R \in Ring \land O \in L) \to (s \in ℕ_{0} \to (K \in ℕ_{0} \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)))))$
180	124 179	syl	$⊢ (K \in ℕ_{0} \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to ((N \in Fin \land R \in Ring \land O \in L) \to (s \in ℕ_{0} \to (K \in ℕ_{0} \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)))))$
181	180	ex	$⊢ K \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}) \to ((N \in Fin \land R \in Ring \land O \in L) \to (s \in ℕ_{0} \to (K \in ℕ_{0} \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K))))))$
182	181	com25	$⊢ K \in ℕ_{0} \to (K \in ℕ_{0} \to ((N \in Fin \land R \in Ring \land O \in L) \to (s \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}) \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K))))))$
183	182	pm2.43i	$⊢ K \in ℕ_{0} \to ((N \in Fin \land R \in Ring \land O \in L) \to (s \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}) \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)))))$
184	183	impcom	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (s \in ℕ_{0} \to (\forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}) \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K))))$
185	184	imp31	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (s < K \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K))$
186	185	com12	$⊢ s < K \to (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K))$
187	165	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to R \in Mnd$
188	187	adantl	$⊢ (\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \to R \in Mnd$
189	188	3ad2ant1	$⊢ ((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \to R \in Mnd$
190		ovexd	$⊢ ((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \to (0 \dots s) \in V$
191		lenlt	$⊢ (K \in ℝ \land s \in ℝ) \to (K \leq s \leftrightarrow \neg s < K)$
192	134 132 191	syl2an	$⊢ (K \in ℕ_{0} \land s \in ℕ_{0}) \to (K \leq s \leftrightarrow \neg s < K)$
193		simpll	$⊢ ((K \in ℕ_{0} \land s \in ℕ_{0}) \land K \leq s) \to K \in ℕ_{0}$
194		simplr	$⊢ ((K \in ℕ_{0} \land s \in ℕ_{0}) \land K \leq s) \to s \in ℕ_{0}$
195		simpr	$⊢ ((K \in ℕ_{0} \land s \in ℕ_{0}) \land K \leq s) \to K \leq s$
196		elfz2nn0	$⊢ K \in (0 \dots s) \leftrightarrow (K \in ℕ_{0} \land s \in ℕ_{0} \land K \leq s)$
197	193 194 195 196	syl3anbrc	$⊢ ((K \in ℕ_{0} \land s \in ℕ_{0}) \land K \leq s) \to K \in (0 \dots s)$
198	197	ex	$⊢ (K \in ℕ_{0} \land s \in ℕ_{0}) \to (K \leq s \to K \in (0 \dots s))$
199	192 198	sylbird	$⊢ (K \in ℕ_{0} \land s \in ℕ_{0}) \to (\neg s < K \to K \in (0 \dots s))$
200	199	ad4ant23	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (\neg s < K \to K \in (0 \dots s))$
201	200	impcom	$⊢ (\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \to K \in (0 \dots s)$
202	201	3ad2ant1	$⊢ ((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \to K \in (0 \dots s)$
203		eqcom	$⊢ K = k \leftrightarrow k = K$
204		ifbi	$⊢ (K = k \leftrightarrow k = K) \to if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) = if (k = K, i {coe}_{1} (O) (k) j, 0_{R})$
205	203 204	ax-mp	$⊢ if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) = if (k = K, i {coe}_{1} (O) (k) j, 0_{R})$
206	205	mpteq2i	$⊢ (k \in (0 \dots s) ⟼ if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = (k \in (0 \dots s) ⟼ if (k = K, i {coe}_{1} (O) (k) j, 0_{R}))$
207		simpl2	$⊢ (((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to i \in N$
208		simpl3	$⊢ (((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to j \in N$
209	27	adantl	$⊢ (\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \to O \in L$
210	209	3ad2ant1	$⊢ ((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \to O \in L$
211	210 30	sylan	$⊢ (((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
212	1 22 23 207 208 211	matecld	$⊢ (((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to i {coe}_{1} (O) (k) j \in {Base}_{R}$
213	91 212	sylan2	$⊢ (((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \land k \in (0 \dots s)) \to i {coe}_{1} (O) (k) j \in {Base}_{R}$
214	213	ralrimiva	$⊢ ((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \to \forall k \in (0 \dots s) i {coe}_{1} (O) (k) j \in {Base}_{R}$
215	43 189 190 202 206 214	gsummpt1n0	$⊢ ((\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \land i \in N \land j \in N) \to {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R}) = ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)$
216	215	mpoeq3dva	$⊢ (\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j))$
217		csbov	$⊢ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j) = i ⦋ K / k ⦌ {coe}_{1} (O) (k) j$
218		csbfv	$⊢ ⦋ K / k ⦌ {coe}_{1} (O) (k) = {coe}_{1} (O) (K)$
219	218	a1i	$⊢ K \in ℕ_{0} \to ⦋ K / k ⦌ {coe}_{1} (O) (k) = {coe}_{1} (O) (K)$
220	219	oveqd	$⊢ K \in ℕ_{0} \to i ⦋ K / k ⦌ {coe}_{1} (O) (k) j = i {coe}_{1} (O) (K) j$
221	217 220	eqtrid	$⊢ K \in ℕ_{0} \to ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j) = i {coe}_{1} (O) (K) j$
222	221	ad2antlr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land (a \in N \land b \in N)) \to ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j) = i {coe}_{1} (O) (K) j$
223	222	mpoeq3dv	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land (a \in N \land b \in N)) \to (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) = (i \in N, j \in N ⟼ i {coe}_{1} (O) (K) j)$
224		oveq12	$⊢ (i = a \land j = b) \to i {coe}_{1} (O) (K) j = a {coe}_{1} (O) (K) b$
225	224	adantl	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land (a \in N \land b \in N)) \land (i = a \land j = b)) \to i {coe}_{1} (O) (K) j = a {coe}_{1} (O) (K) b$
226		simprl	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land (a \in N \land b \in N)) \to a \in N$
227		simprr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land (a \in N \land b \in N)) \to b \in N$
228		ovexd	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land (a \in N \land b \in N)) \to a {coe}_{1} (O) (K) b \in V$
229	223 225 226 227 228	ovmpod	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land (a \in N \land b \in N)) \to a (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) b = a {coe}_{1} (O) (K) b$
230	229	ralrimivva	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) b = a {coe}_{1} (O) (K) b$
231		simpl1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to N \in Fin$
232	218	oveqi	$⊢ i ⦋ K / k ⦌ {coe}_{1} (O) (k) j = i {coe}_{1} (O) (K) j$
233	217 232	eqtri	$⊢ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j) = i {coe}_{1} (O) (K) j$
234		simp2	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to i \in N$
235		simp3	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to j \in N$
236	29 3 2 23	coe1fvalcl	$⊢ (O \in L \land K \in ℕ_{0}) \to {coe}_{1} (O) (K) \in {Base}_{A}$
237	236	3ad2antl3	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to {coe}_{1} (O) (K) \in {Base}_{A}$
238	237	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (O) (K) \in {Base}_{A}$
239	1 22 23 234 235 238	matecld	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to i {coe}_{1} (O) (K) j \in {Base}_{R}$
240	233 239	eqeltrid	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land i \in N \land j \in N) \to ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j) \in {Base}_{R}$
241	1 22 23 231 18 240	matbas2d	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) \in {Base}_{A}$
242	1 23	eqmat	$⊢ ((i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) \in {Base}_{A} \land {coe}_{1} (O) (K) \in {Base}_{A}) \to ((i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) = {coe}_{1} (O) (K) \leftrightarrow \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) b = a {coe}_{1} (O) (K) b)$
243	241 237 242	syl2anc	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to ((i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) = {coe}_{1} (O) (K) \leftrightarrow \forall a \in N \forall b \in N a (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) b = a {coe}_{1} (O) (K) b)$
244	230 243	mpbird	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) = {coe}_{1} (O) (K)$
245	244	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) = {coe}_{1} (O) (K)$
246	245	adantl	$⊢ (\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \to (i \in N, j \in N ⟼ ⦋ K / k ⦌ (i {coe}_{1} (O) (k) j)) = {coe}_{1} (O) (K)$
247	216 246	eqtrd	$⊢ (\neg s < K \land ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A}))) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)$
248	247	ex	$⊢ \neg s < K \to (((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K))$
249	186 248	pm2.61i	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (i \in N, j \in N ⟼ {\sum_{R}}_{k = 0}^{s} if (K = k, i {coe}_{1} (O) (k) j, 0_{R})) = {coe}_{1} (O) (K)$
250	97 120 249	3eqtrd	$⊢ ((((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \land s \in ℕ_{0}) \land \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})) \to (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K)) = {coe}_{1} (O) (K)$
251		eqid	$⊢ 0_{A} = 0_{A}$
252	29 3 2 251	coe1sfi	$⊢ O \in L \to {finSupp}_{0_{A}} ({coe}_{1} (O))$
253	26 252	syl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to {finSupp}_{0_{A}} ({coe}_{1} (O))$
254	29 3 2 251 23	coe1fsupp	$⊢ O \in L \to {coe}_{1} (O) \in \{x \in ({Base}_{A}^{ℕ_{0}}) \| {finSupp}_{0_{A}} (x)\}$
255		elrabi	$⊢ {coe}_{1} (O) \in \{x \in ({Base}_{A}^{ℕ_{0}}) \| {finSupp}_{0_{A}} (x)\} \to {coe}_{1} (O) \in ({Base}_{A}^{ℕ_{0}})$
256	26 254 255	3syl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to {coe}_{1} (O) \in ({Base}_{A}^{ℕ_{0}})$
257		fvex	$⊢ 0_{A} \in V$
258		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}))$
259	256 257 258	sylancl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \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}))$
260	253 259	mpd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to {coe}_{1} (O) (x) = 0_{A})$
261	250 260	r19.29a	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) (K)) = {coe}_{1} (O) (K)$
262	9 261	eqtrd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land K \in ℕ_{0}) \to I (O) decompPMat K = {coe}_{1} (O) (K)$

Metamath Proof Explorer

Theorem mp2pm2mplem4

Proof