| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin) |
| 2 | | simplr 769 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring) |
| 3 | | pm2mpmhm.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
| 4 | | pm2mpmhm.c |
. . . . . . . 8
⊢ 𝐶 = (𝑁 Mat 𝑃) |
| 5 | 3, 4 | pmatring 22698 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
| 6 | 5 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ Ring) |
| 7 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
| 8 | 7 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
| 9 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
| 10 | 9 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
| 11 | | pm2mpmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝐶) = (.r‘𝐶) |
| 13 | 11, 12 | ringcl 20247 |
. . . . . 6
⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
| 14 | 6, 8, 10, 13 | syl3anc 1373 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
| 15 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑄) = ( ·𝑠
‘𝑄) |
| 16 | | eqid 2737 |
. . . . . 6
⊢
(.g‘(mulGrp‘𝑄)) =
(.g‘(mulGrp‘𝑄)) |
| 17 | | eqid 2737 |
. . . . . 6
⊢
(var1‘𝐴) = (var1‘𝐴) |
| 18 | | pm2mpmhm.a |
. . . . . 6
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 19 | | pm2mpmhm.q |
. . . . . 6
⊢ 𝑄 = (Poly1‘𝐴) |
| 20 | | pm2mpmhm.t |
. . . . . 6
⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) |
| 21 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 22802 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 22 | 1, 2, 14, 21 | syl3anc 1373 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 23 | 3, 4, 11, 18 | decpmatmul 22778 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
| 24 | 23 | ad4ant234 1176 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
| 25 | 24 | oveq1d 7446 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) = ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
| 26 | 25 | mpteq2dva 5242 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) |
| 27 | 26 | oveq2d 7447 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 28 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑄) =
(Base‘𝑄) |
| 29 | 18 | matring 22449 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
| 30 | 29 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring) |
| 31 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐴) =
(Base‘𝐴) |
| 32 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐴) = (0g‘𝐴) |
| 33 | | ringcmn 20279 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd) |
| 34 | 29, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ CMnd) |
| 35 | 34 | ad3antrrr 730 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
CMnd) |
| 36 | | fzfid 14014 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0...𝑘) ∈
Fin) |
| 37 | 30 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
| 38 | | simp-5r 786 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
| 39 | 8 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
| 40 | | elfznn0 13660 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
| 42 | 3, 4, 11, 18, 31 | decpmatcl 22773 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ ℕ0) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
| 43 | 38, 39, 41, 42 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
| 44 | 10 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
| 45 | | fznn0sub 13596 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → (𝑘 − 𝑧) ∈
ℕ0) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
| 47 | 3, 4, 11, 18, 31 | decpmatcl 22773 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ (𝑘 − 𝑧) ∈ ℕ0) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
| 48 | 38, 44, 46, 47 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
| 49 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.r‘𝐴) = (.r‘𝐴) |
| 50 | 31, 49 | ringcl 20247 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Ring ∧ (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴) ∧ (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
| 51 | 37, 43, 48, 50 | syl3anc 1373 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
| 52 | 51 | ralrimiva 3146 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ∀𝑧 ∈
(0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
| 53 | 31, 35, 36, 52 | gsummptcl 19985 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
| 54 | 53 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
| 55 | 3, 4, 11, 18, 49, 32 | decpmatmulsumfsupp 22779 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
| 56 | 55 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
| 57 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
| 58 | 19, 28, 17, 16, 30, 31, 15, 32, 54, 56, 57 | gsummoncoe1 22312 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ⦋𝑛 / 𝑘⦌(𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
| 59 | | csbov2g 7479 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg
⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
| 60 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) |
| 61 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (0...𝑘) = (0...𝑛)) |
| 62 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝑘 − 𝑧) = (𝑛 − 𝑧)) |
| 63 | 62 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝑦 decompPMat (𝑘 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑧))) |
| 64 | 63 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) = ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) |
| 65 | 61, 64 | mpteq12dv 5233 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
| 66 | 65 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 = 𝑛) → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
| 67 | 60, 66 | csbied 3935 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (𝐴
Σg ⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
| 69 | 59, 68 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
| 70 | 69 | adantl 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
⦋𝑛 / 𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
| 71 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑟 ∈ ℕ0
↦ (𝐴
Σg (𝑙 ∈ (0...𝑟) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙)))))) = (𝑟 ∈ ℕ0 ↦ (𝐴 Σg
(𝑙 ∈ (0...𝑟) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))))))) |
| 72 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑛 → (0...𝑟) = (0...𝑛)) |
| 73 | | fvoveq1 7454 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑛 → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
| 74 | 73 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑛 → (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))) = (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))) |
| 75 | 72, 74 | mpteq12dv 5233 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑛 → (𝑙 ∈ (0...𝑟) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
| 76 | 75 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑛 → (𝐴 Σg (𝑙 ∈ (0...𝑟) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))))) = (𝐴 Σg (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))))) |
| 77 | 76 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑟 = 𝑛) → (𝐴 Σg (𝑙 ∈ (0...𝑟) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))))) = (𝐴 Σg (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))))) |
| 78 | | ovexd 7466 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑙 ∈ (0...𝑛) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) ∈ V) |
| 79 | 71, 77, 57, 78 | fvmptd 7023 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → ((𝑟 ∈ ℕ0
↦ (𝐴
Σg (𝑙 ∈ (0...𝑟) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛) = (𝐴 Σg (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))))) |
| 80 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝑄) = (0g‘𝑄) |
| 81 | 19 | ply1ring 22249 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
| 82 | 29, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Ring) |
| 83 | | ringcmn 20279 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd) |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd) |
| 85 | 84 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑄 ∈ CMnd) |
| 86 | | nn0ex 12532 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
| 87 | 86 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
ℕ0 ∈ V) |
| 88 | 7 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
| 89 | | df-3an 1089 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
| 90 | 88, 89 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
| 91 | 90 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
| 92 | 3, 4, 11, 15, 16, 17, 18, 19, 28 | pm2mpghmlem1 22819 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 93 | 91, 92 | sylan 580 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑥 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 94 | 93 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
| 95 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 22818 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
| 96 | 91, 95 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
| 97 | 28, 80, 85, 87, 94, 96 | gsumcl 19933 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
| 98 | 9 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
| 99 | | df-3an 1089 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
| 100 | 98, 99 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
| 101 | 100 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
| 102 | 3, 4, 11, 15, 16, 17, 18, 19, 28 | pm2mpghmlem1 22819 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 103 | 101, 102 | sylan 580 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑦 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 104 | 103 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
| 105 | 1, 2, 10 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
| 106 | 105 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
| 107 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 22818 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
| 109 | 28, 80, 85, 87, 104, 108 | gsumcl 19933 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
| 110 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑄) = (.r‘𝑄) |
| 111 | 19, 110, 49, 28 | coe1mul 22273 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Ring ∧ (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄) ∧ (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) →
(coe1‘((𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) = (𝑟 ∈ ℕ0 ↦ (𝐴 Σg
(𝑙 ∈ (0...𝑟) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))))))) |
| 112 | 111 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Ring ∧ (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄) ∧ (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) →
((coe1‘((𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛) = ((𝑟 ∈ ℕ0 ↦ (𝐴 Σg
(𝑙 ∈ (0...𝑟) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
| 113 | 30, 97, 109, 112 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
((coe1‘((𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛) = ((𝑟 ∈ ℕ0 ↦ (𝐴 Σg
(𝑙 ∈ (0...𝑟) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
| 114 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑥 decompPMat 𝑧) = (𝑥 decompPMat 𝑙)) |
| 115 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑙 → (𝑛 − 𝑧) = (𝑛 − 𝑙)) |
| 116 | 115 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑦 decompPMat (𝑛 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑙))) |
| 117 | 114, 116 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑙 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))) = ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
| 118 | 117 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
| 119 | 29 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝐴 ∈ Ring) |
| 120 | | simp-5r 786 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
| 121 | 8 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
| 122 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
| 123 | 3, 4, 11, 18, 31 | decpmatcl 22773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
| 124 | 120, 121,
122, 123 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
| 125 | 124 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
| 126 | 2, 8 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
| 127 | 126 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
| 128 | 3, 4, 11, 18, 32 | decpmatfsupp 22775 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
| 129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
| 130 | | elfznn0 13660 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℕ0) |
| 131 | 130 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑙 ∈ ℕ0) |
| 132 | 19, 28, 17, 16, 119, 31, 15, 32, 125, 129, 131 | gsummoncoe1 22312 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘)) |
| 133 | | csbov2g 7479 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘)) |
| 134 | | csbvarg 4434 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌𝑘 = 𝑙) |
| 135 | 134 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘) = (𝑥 decompPMat 𝑙)) |
| 136 | 133, 135 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
| 137 | 136 | adantl 481 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
| 138 | 132, 137 | eqtr2d 2778 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑥 decompPMat 𝑙) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)) |
| 139 | 10 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
| 140 | 3, 4, 11, 18, 31 | decpmatcl 22773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
| 141 | 120, 139,
122, 140 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
| 142 | 141 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
| 143 | 2, 10 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
| 144 | 143 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
| 145 | 3, 4, 11, 18, 32 | decpmatfsupp 22775 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
| 146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
| 147 | | fznn0sub 13596 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑛 − 𝑙) ∈
ℕ0) |
| 148 | 147 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑛 − 𝑙) ∈
ℕ0) |
| 149 | 19, 28, 17, 16, 119, 31, 15, 32, 142, 146, 148 | gsummoncoe1 22312 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)) = ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘)) |
| 150 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢ (𝑛 − 𝑙) ∈ V |
| 151 | | csbov2g 7479 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
| 152 | 150, 151 | mp1i 13 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
| 153 | | csbvarg 4434 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
| 154 | 150, 153 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
| 155 | 154 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘) = (𝑦 decompPMat (𝑛 − 𝑙))) |
| 156 | 149, 152,
155 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat (𝑛 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
| 157 | 138, 156 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙))) = (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))) |
| 158 | 157 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
| 159 | 118, 158 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
| 160 | 159 | oveq2d 7447 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) = (𝐴 Σg (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))))) |
| 161 | 79, 113, 160 | 3eqtr4rd 2788 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛)) |
| 162 | 58, 70, 161 | 3eqtrd 2781 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛)) |
| 163 | 162 | ralrimiva 3146 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑛 ∈ ℕ0
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛)) |
| 164 | 29 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐴 ∈ Ring) |
| 165 | 84 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ CMnd) |
| 166 | 86 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ℕ0 ∈
V) |
| 167 | 19 | ply1lmod 22253 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
| 168 | 29, 167 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ LMod) |
| 169 | 168 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑄 ∈ LMod) |
| 170 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ CMnd) |
| 171 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
| 172 | 29 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
| 173 | | simp-4r 784 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
| 174 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
| 175 | 174 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
| 176 | 40 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
| 177 | 173, 175,
176, 42 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
| 178 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
| 179 | 178 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
| 180 | 45 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
| 181 | 173, 179,
180, 47 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
| 182 | 172, 177,
181, 50 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
| 183 | 182 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
∀𝑧 ∈ (0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
| 184 | 31, 170, 171, 183 | gsummptcl 19985 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
| 185 | 29 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ Ring) |
| 186 | 19 | ply1sca 22254 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
| 187 | 185, 186 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 = (Scalar‘𝑄)) |
| 188 | 187 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Scalar‘𝑄) = 𝐴) |
| 189 | 188 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Base‘(Scalar‘𝑄)) = (Base‘𝐴)) |
| 190 | 184, 189 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄))) |
| 191 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
| 192 | 19, 17, 191, 16, 28 | ply1moncl 22274 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0)
→ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
| 193 | 185, 192 | sylancom 588 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
| 194 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
| 195 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑄)) = (Base‘(Scalar‘𝑄)) |
| 196 | 28, 194, 15, 195 | lmodvscl 20876 |
. . . . . . . . 9
⊢ ((𝑄 ∈ LMod ∧ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄)) ∧ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) → ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 197 | 169, 190,
193, 196 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 198 | 197 | fmpttd 7135 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
| 199 | 3, 4, 11, 15, 16, 17, 18, 19, 28, 20 | pm2mpmhmlem1 22824 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
| 200 | 28, 80, 165, 166, 198, 199 | gsumcl 19933 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
| 201 | 82 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ Ring) |
| 202 | 90, 92 | sylan 580 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 203 | 202 | fmpttd 7135 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
| 204 | 90, 95 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
| 205 | 28, 80, 165, 166, 203, 204 | gsumcl 19933 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
| 206 | 100, 102 | sylan 580 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
| 207 | 206 | fmpttd 7135 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
| 208 | 1, 2, 10, 107 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
| 209 | 28, 80, 165, 166, 207, 208 | gsumcl 19933 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
| 210 | 28, 110 | ringcl 20247 |
. . . . . . 7
⊢ ((𝑄 ∈ Ring ∧ (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄) ∧ (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) → ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) ∈ (Base‘𝑄)) |
| 211 | 201, 205,
209, 210 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) ∈ (Base‘𝑄)) |
| 212 | | eqid 2737 |
. . . . . . 7
⊢
(coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 213 | | eqid 2737 |
. . . . . . 7
⊢
(coe1‘((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) =
(coe1‘((𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
| 214 | 19, 28, 212, 213 | ply1coe1eq 22304 |
. . . . . 6
⊢ ((𝐴 ∈ Ring ∧ (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄) ∧ ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) ∈ (Base‘𝑄)) → (∀𝑛 ∈ ℕ0
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛) ↔ (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))) |
| 215 | 164, 200,
211, 214 | syl3anc 1373 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑛 ∈ ℕ0
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛) ↔ (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))) |
| 216 | 163, 215 | mpbid 232 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
| 217 | 22, 27, 216 | 3eqtrd 2781 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
| 218 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 22802 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 219 | 1, 2, 8, 218 | syl3anc 1373 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 220 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 22802 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 221 | 1, 2, 10, 220 | syl3anc 1373 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
| 222 | 219, 221 | oveq12d 7449 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
| 223 | 217, 222 | eqtr4d 2780 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |
| 224 | 223 | ralrimivva 3202 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |