Metamath Proof Explorer

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 )