Theorem decpmatmulsumfsupp 21381

Description: Lemma 0 for pm2mpmhm 21428. (Contributed by AV, 21-Oct-2019.)

Hypotheses

Ref	Expression
decpmatmul.p	⊢ 𝑃 = (Poly1‘𝑅)
decpmatmul.c	⊢ 𝐶 = (𝑁 Mat 𝑃)
decpmatmul.b	⊢ 𝐵 = (Base‘𝐶)
decpmatmul.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
decpmatmulsumfsupp.m	⊢ · = (.r‘𝐴)
decpmatmulsumfsupp.0	⊢ 0 = (0g‘𝐴)

Assertion

Ref	Expression
decpmatmulsumfsupp	⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 )

Distinct variable groups:   𝐵,𝑘,𝑙   𝑘,𝑁   𝑃,𝑘   𝑅,𝑘,𝑙   𝐴,𝑘   𝑥,𝐵,𝑦,𝑘   𝑥,𝑁,𝑦   𝑥,𝑅,𝑦   𝐴,𝑙   𝐵,𝑙   𝑁,𝑙,𝑥,𝑦   · ,𝑙

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐶(𝑥,𝑦,𝑘,𝑙)   𝑃(𝑥,𝑦,𝑙)   · (𝑥,𝑦,𝑘)   0 (𝑥,𝑦,𝑘,𝑙)

Proof of Theorem decpmatmulsumfsupp

Dummy variables 𝑖 𝑗 𝑛 𝑠 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		decpmatmulsumfsupp.0	. . . 4 ⊢ 0 = (0g‘𝐴)
2	1	fvexi 6684	. . 3 ⊢ 0 ∈ V
3	2	a1i 11	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 0 ∈ V)
4		ovexd 7191	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑙 ∈ ℕ0) → (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘))))) ∈ V)
5		oveq2 7164	. . . 4 ⊢ (𝑙 = 𝑛 → (0...𝑙) = (0...𝑛))
6		oveq1 7163	. . . . . 6 ⊢ (𝑙 = 𝑛 → (𝑙 − 𝑘) = (𝑛 − 𝑘))
7	6	oveq2d 7172	. . . . 5 ⊢ (𝑙 = 𝑛 → (𝑦 decompPMat (𝑙 − 𝑘)) = (𝑦 decompPMat (𝑛 − 𝑘)))
8	7	oveq2d 7172	. . . 4 ⊢ (𝑙 = 𝑛 → ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘))) = ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))
9	5, 8	mpteq12dv 5151	. . 3 ⊢ (𝑙 = 𝑛 → (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘)))))
10	9	oveq2d 7172	. 2 ⊢ (𝑙 = 𝑛 → (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘))))) = (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))))
11		simpll 765	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin)
12		simplr 767	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring)
13		decpmatmul.p	. . . . . . . . 9 ⊢ 𝑃 = (Poly1‘𝑅)
14		decpmatmul.c	. . . . . . . . 9 ⊢ 𝐶 = (𝑁 Mat 𝑃)
15	13, 14	pmatring 21301	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
16	15	anim1i 616	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐶 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
17		3anass 1091	. . . . . . 7 ⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝐶 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
18	16, 17	sylibr 236	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
19		decpmatmul.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐶)
20		eqid 2821	. . . . . . 7 ⊢ (.r‘𝐶) = (.r‘𝐶)
21	19, 20	ringcl 19311	. . . . . 6 ⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵)
22	18, 21	syl 17	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵)
23		eqid 2821	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
24	13, 14, 19, 23	pmatcoe1fsupp 21309	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)))
25	11, 12, 22, 24	syl3anc 1367	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)))
26		fvoveq1 7179	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑖 → (coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏)) = (coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑏)))
27	26	fveq1d 6672	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑖 → ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛))
28	27	eqeq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑖 → (((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅) ↔ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)))
29		oveq2 7164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑗 → (𝑖(𝑥(.r‘𝐶)𝑦)𝑏) = (𝑖(𝑥(.r‘𝐶)𝑦)𝑗))
30	29	fveq2d 6674	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑗 → (coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑏)) = (coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗)))
31	30	fveq1d 6672	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑗 → ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛))
32	31	eqeq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑗 → (((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅) ↔ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛) = (0g‘𝑅)))
33	28, 32	rspc2va 3634	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛) = (0g‘𝑅))
34	33	expcom 416	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛) = (0g‘𝑅)))
35	34	adantl 484	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛) = (0g‘𝑅)))
36	35	3impib 1112	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛) = (0g‘𝑅))
37	36	mpoeq3dva 7231	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)))
38		decpmatmul.a	. . . . . . . . . . . 12 ⊢ 𝐴 = (𝑁 Mat 𝑅)
39	38, 23	mat0op 21028	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)))
40	1, 39	syl5eq 2868	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)))
41	40	ad3antrrr 728	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → 0 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)))
42	37, 41	eqtr4d 2859	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 )
43	42	ex 415	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 ))
44	43	imim2d 57	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑠 < 𝑛 → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → (𝑠 < 𝑛 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 )))
45	44	ralimdva 3177	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 )))
46	45	reximdv 3273	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 ((coe1‘(𝑎(𝑥(.r‘𝐶)𝑦)𝑏))‘𝑛) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 )))
47	25, 46	mpd 15	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 ))
48		decpmatmulsumfsupp.m	. . . . . . . . . . . 12 ⊢ · = (.r‘𝐴)
49	48	oveqi 7169	. . . . . . . . . . 11 ⊢ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))) = ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑘)))
50	49	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))) = ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑘))))
51	50	mpteq2dv 5162	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑘)))))
52	51	oveq2d 7172	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))) = (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑘))))))
53	13, 14, 19, 38	decpmatmul 21380	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑛) = (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑘))))))
54	53	ad4ant234 1171	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑛) = (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑘))))))
55	14, 19	decpmatval 21373	. . . . . . . . 9 ⊢ (((𝑥(.r‘𝐶)𝑦) ∈ 𝐵 ∧ 𝑛 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑛) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)))
56	22, 55	sylan 582	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑛) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)))
57	52, 54, 56	3eqtr2d 2862	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)))
58	57	eqeq1d 2823	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))) = 0 ↔ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 ))
59	58	imbi2d 343	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑠 < 𝑛 → (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))) = 0 ) ↔ (𝑠 < 𝑛 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 )))
60	59	ralbidva 3196	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))) = 0 ) ↔ ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 )))
61	60	rexbidv 3297	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))) = 0 ) ↔ ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖(𝑥(.r‘𝐶)𝑦)𝑗))‘𝑛)) = 0 )))
62	47, 61	mpbird 259	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝐴 Σg (𝑘 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑛 − 𝑘))))) = 0 ))
63	3, 4, 10, 62	mptnn0fsuppd 13367	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ (𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘) · (𝑦 decompPMat (𝑙 − 𝑘)))))) finSupp 0 )

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  Vcvv 3494   class class class wbr 5066   ↦ cmpt 5146  ‘cfv 6355  (class class class)co 7156   ∈ cmpo 7158  Fincfn 8509   finSupp cfsupp 8833  0cc0 10537   < clt 10675   − cmin 10870  ℕ₀cn0 11898  ...cfz 12893  Basecbs 16483  ._rcmulr 16566  0_gc0g 16713   Σ_g cgsu 16714  Ringcrg 19297  Poly₁cpl1 20345  coe₁cco1 20346   Mat cmat 21016   decompPMat cdecpmat 21370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-ot 4576  df-uni 4839  df-int 4877  df-iun 4921  df-iin 4922  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7409  df-ofr 7410  df-om 7581  df-1st 7689  df-2nd 7690  df-supp 7831  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-2o 8103  df-oadd 8106  df-er 8289  df-map 8408  df-pm 8409  df-ixp 8462  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-fsupp 8834  df-sup 8906  df-oi 8974  df-card 9368  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-2 11701  df-3 11702  df-4 11703  df-5 11704  df-6 11705  df-7 11706  df-8 11707  df-9 11708  df-n0 11899  df-z 11983  df-dec 12100  df-uz 12245  df-fz 12894  df-fzo 13035  df-seq 13371  df-hash 13692  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-hom 16589  df-cco 16590  df-0g 16715  df-gsum 16716  df-prds 16721  df-pws 16723  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mhm 17956  df-submnd 17957  df-grp 18106  df-minusg 18107  df-sbg 18108  df-mulg 18225  df-subg 18276  df-ghm 18356  df-cntz 18447  df-cmn 18908  df-abl 18909  df-mgp 19240  df-ur 19252  df-ring 19299  df-subrg 19533  df-lmod 19636  df-lss 19704  df-sra 19944  df-rgmod 19945  df-psr 20136  df-mpl 20138  df-opsr 20140  df-psr1 20348  df-ply1 20350  df-coe1 20351  df-dsmm 20876  df-frlm 20891  df-mamu 20995  df-mat 21017  df-decpmat 21371

This theorem is referenced by:  pm2mpmhmlem2  21427