Theorem decpmatmulsumfsupp

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

	Ref	Expression
Hypotheses	decpmatmul.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	decpmatmul.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	decpmatmul.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	decpmatmul.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	decpmatmulsumfsupp.m	⊢ · = ( .r ‘ 𝐴 )
	decpmatmulsumfsupp.0	⊢ 0 = ( 0g ‘ 𝐴 )
Assertion	decpmatmulsumfsupp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑙 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) ) finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		decpmatmul.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		decpmatmul.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		decpmatmul.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		decpmatmul.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
5		decpmatmulsumfsupp.m	⊢ · = ( .r ‘ 𝐴 )
6		decpmatmulsumfsupp.0	⊢ 0 = ( 0g ‘ 𝐴 )
7	6	fvexi	⊢ 0 ∈ V
8	7	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 0 ∈ V )
9		ovexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) ∈ V )
10		oveq2	⊢ ( 𝑙 = 𝑛 → ( 0 ... 𝑙 ) = ( 0 ... 𝑛 ) )
11		oveq1	⊢ ( 𝑙 = 𝑛 → ( 𝑙 − 𝑘 ) = ( 𝑛 − 𝑘 ) )
12	11	oveq2d	⊢ ( 𝑙 = 𝑛 → ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) = ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) )
13	12	oveq2d	⊢ ( 𝑙 = 𝑛 → ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) = ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) )
14	10 13	mpteq12dv	⊢ ( 𝑙 = 𝑛 → ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) )
15	14	oveq2d	⊢ ( 𝑙 = 𝑛 → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) )
16		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
17		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
18	1 2	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
19	18	anim1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐶 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
20		3anass	⊢ ( ( 𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝐶 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
21	19 20	sylibr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
22		eqid	⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
23	3 22	ringcl	⊢ ( ( 𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 )
24	21 23	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 )
25		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26	1 2 3 25	pmatcoe1fsupp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
27	16 17 24 26	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
28		fvoveq1	⊢ ( 𝑎 = 𝑖 → ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) = ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) )
29	28	fveq1d	⊢ ( 𝑎 = 𝑖 → ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) )
30	29	eqeq1d	⊢ ( 𝑎 = 𝑖 → ( ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
31		oveq2	⊢ ( 𝑏 = 𝑗 → ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) = ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) )
32	31	fveq2d	⊢ ( 𝑏 = 𝑗 → ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) = ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) )
33	32	fveq1d	⊢ ( 𝑏 = 𝑗 → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) )
34	33	eqeq1d	⊢ ( 𝑏 = 𝑗 → ( ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
35	30 34	rspc2va	⊢ ( ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) )
36	35	expcom	⊢ ( ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
37	36	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) )
38	37	3impib	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) )
39	38	mpoeq3dva	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
40	4 25	mat0op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
41	6 40	eqtrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 0 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
42	41	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → 0 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
43	39 42	eqtr4d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 )
44	43	ex	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) )
45	44	imim2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑠 < 𝑛 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) ) )
46	45	ralimdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) ) )
47	46	reximdv	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( ( coe1 ‘ ( 𝑎 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑏 ) ) ‘ 𝑛 ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) ) )
48	27 47	mpd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) )
49	5	oveqi	⊢ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) = ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) )
50	49	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) = ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) )
51	50	mpteq2dv	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) )
52	51	oveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) )
53	1 2 3 4	decpmatmul	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) )
54	53	ad4ant234	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) ( .r ‘ 𝐴 ) ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) )
55	2 3	decpmatval	⊢ ( ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) )
56	24 55	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) )
57	52 54 56	3eqtr2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) )
58	57	eqeq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = 0 ↔ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) )
59	58	imbi2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = 0 ) ↔ ( 𝑠 < 𝑛 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) ) )
60	59	ralbidva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = 0 ) ↔ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) ) )
61	60	rexbidv	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = 0 ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑛 ) ) = 0 ) ) )
62	48 61	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑛 − 𝑘 ) ) ) ) ) = 0 ) )
63	8 9 15 62	mptnn0fsuppd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑙 ∈ ℕ0 ↦ ( 𝐴 Σg ( 𝑘 ∈ ( 0 ... 𝑙 ) ↦ ( ( 𝑥 decompPMat 𝑘 ) · ( 𝑦 decompPMat ( 𝑙 − 𝑘 ) ) ) ) ) ) finSupp 0 )