Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin) |
2 | | simplr 792 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring) |
3 | | pm2mpmhm.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
4 | | pm2mpmhm.c |
. . . . . . . 8
⊢ 𝐶 = (𝑁 Mat 𝑃) |
5 | 3, 4 | pmatring 20498 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
6 | 5 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ Ring) |
7 | | simpl 473 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
8 | 7 | adantl 482 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
9 | | simpr 477 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
11 | | pm2mpmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
12 | | eqid 2622 |
. . . . . . 7
⊢
(.r‘𝐶) = (.r‘𝐶) |
13 | 11, 12 | ringcl 18561 |
. . . . . 6
⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
14 | 6, 8, 10, 13 | syl3anc 1326 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
15 | | eqid 2622 |
. . . . . 6
⊢ (
·𝑠 ‘𝑄) = ( ·𝑠
‘𝑄) |
16 | | eqid 2622 |
. . . . . 6
⊢
(.g‘(mulGrp‘𝑄)) =
(.g‘(mulGrp‘𝑄)) |
17 | | eqid 2622 |
. . . . . 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 20601 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
22 | 1, 2, 14, 21 | syl3anc 1326 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
23 | | simpllr 799 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
24 | | simplr 792 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
25 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
26 | 3, 4, 11, 18 | decpmatmul 20577 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
27 | 23, 24, 25, 26 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
28 | 27 | oveq1d 6665 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) = ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
29 | 28 | mpteq2dva 4744 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) |
30 | 29 | oveq2d 6666 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
31 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑄) =
(Base‘𝑄) |
32 | 18 | matring 20249 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
33 | 32 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring) |
34 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝐴) =
(Base‘𝐴) |
35 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝐴) = (0g‘𝐴) |
36 | | ringcmn 18581 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd) |
37 | 32, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ CMnd) |
38 | 37 | ad3antrrr 766 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
CMnd) |
39 | | fzfid 12772 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0...𝑘) ∈
Fin) |
40 | 33 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
41 | | simp-5r 809 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
42 | 8 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
43 | | elfznn0 12433 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
45 | 3, 4, 11, 18, 34 | decpmatcl 20572 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ ℕ0) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
46 | 41, 42, 44, 45 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
47 | 10 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
48 | | fznn0sub 12373 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → (𝑘 − 𝑧) ∈
ℕ0) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
50 | 3, 4, 11, 18, 34 | decpmatcl 20572 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ (𝑘 − 𝑧) ∈ ℕ0) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
51 | 41, 47, 49, 50 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
52 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(.r‘𝐴) = (.r‘𝐴) |
53 | 34, 52 | ringcl 18561 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Ring ∧ (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴) ∧ (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
54 | 40, 46, 51, 53 | syl3anc 1326 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
55 | 54 | ralrimiva 2966 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ∀𝑧 ∈
(0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
56 | 34, 38, 39, 55 | gsummptcl 18366 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
57 | 56 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
58 | 3, 4, 11, 18, 52, 35 | decpmatmulsumfsupp 20578 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
59 | 58 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
60 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
61 | 19, 31, 17, 16, 33, 34, 15, 35, 57, 59, 60 | gsummoncoe1 19674 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ⦋𝑛 / 𝑘⦌(𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
62 | | csbov2g 6691 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg
⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
63 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) |
64 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (0...𝑘) = (0...𝑛)) |
65 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝑘 − 𝑧) = (𝑛 − 𝑧)) |
66 | 65 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝑦 decompPMat (𝑘 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑧))) |
67 | 66 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) = ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) |
68 | 64, 67 | mpteq12dv 4733 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
69 | 68 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 = 𝑛) → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
70 | 63, 69 | csbied 3560 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
71 | 70 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (𝐴
Σg ⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
72 | 62, 71 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
73 | 72 | adantl 482 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
⦋𝑛 / 𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
74 | | eqidd 2623 |
. . . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))) |
75 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑛 → (0...𝑟) = (0...𝑛)) |
76 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑛 → (𝑟 − 𝑙) = (𝑛 − 𝑙)) |
77 | 76 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑛 → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
78 | 77 | oveq2d 6666 |
. . . . . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))) |
79 | 75, 78 | mpteq12dv 4733 |
. . . . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙))))) |
80 | 79 | oveq2d 6666 |
. . . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
81 | 80 | adantl 482 |
. . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
82 | | ovexd 6680 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑙 ∈ (0...𝑛) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) ∈ V) |
83 | 74, 81, 60, 82 | fvmptd 6288 |
. . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
84 | | eqid 2622 |
. . . . . . . . . 10
⊢
(0g‘𝑄) = (0g‘𝑄) |
85 | 19 | ply1ring 19618 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
86 | 32, 85 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Ring) |
87 | | ringcmn 18581 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd) |
89 | 88 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑄 ∈ CMnd) |
90 | | nn0ex 11298 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
91 | 90 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
ℕ0 ∈ V) |
92 | 7 | anim2i 593 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
93 | | df-3an 1039 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
94 | 92, 93 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
95 | 94 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
96 | 3, 4, 11, 15, 16, 17, 18, 19, 31 | pm2mpghmlem1 20618 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
97 | 95, 96 | sylan 488 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑥 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
98 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
99 | 97, 98 | fmptd 6385 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
100 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 20617 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
101 | 95, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
102 | 31, 84, 89, 91, 99, 101 | gsumcl 18316 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
103 | 9 | anim2i 593 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
104 | | df-3an 1039 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
105 | 103, 104 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
106 | 105 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
107 | 3, 4, 11, 15, 16, 17, 18, 19, 31 | pm2mpghmlem1 20618 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
108 | 106, 107 | sylan 488 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑦 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
109 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
110 | 108, 109 | fmptd 6385 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
111 | 1, 2, 10 | 3jca 1242 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
112 | 111 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
113 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 20617 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
114 | 112, 113 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
115 | 31, 84, 89, 91, 110, 114 | gsumcl 18316 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
116 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.r‘𝑄) = (.r‘𝑄) |
117 | 19, 116, 52, 31 | coe1mul 19640 |
. . . . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))) |
118 | 117 | fveq1d 6193 |
. . . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
119 | 33, 102, 115, 118 | syl3anc 1326 |
. . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
120 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑥 decompPMat 𝑧) = (𝑥 decompPMat 𝑙)) |
121 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑙 → (𝑛 − 𝑧) = (𝑛 − 𝑙)) |
122 | 121 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑦 decompPMat (𝑛 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑙))) |
123 | 120, 122 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑙 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))) = ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
124 | 123 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
125 | 32 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝐴 ∈ Ring) |
126 | | simp-5r 809 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
127 | 8 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
128 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
129 | 3, 4, 11, 18, 34 | decpmatcl 20572 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
130 | 126, 127,
128, 129 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
131 | 130 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
132 | 2, 8 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
133 | 132 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
134 | 3, 4, 11, 18, 35 | decpmatfsupp 20574 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
136 | | elfznn0 12433 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℕ0) |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑙 ∈ ℕ0) |
138 | 19, 31, 17, 16, 125, 34, 15, 35, 131, 135, 137 | gsummoncoe1 19674 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘)) |
139 | | csbov2g 6691 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘)) |
140 | | csbvarg 4003 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌𝑘 = 𝑙) |
141 | 140 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘) = (𝑥 decompPMat 𝑙)) |
142 | 139, 141 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
143 | 142 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
144 | 138, 143 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑥 decompPMat 𝑙) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)) |
145 | 10 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
146 | 3, 4, 11, 18, 34 | decpmatcl 20572 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
147 | 126, 145,
128, 146 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
148 | 147 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
149 | 2, 10 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
150 | 149 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
151 | 3, 4, 11, 18, 35 | decpmatfsupp 20574 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
153 | | fznn0sub 12373 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑛 − 𝑙) ∈
ℕ0) |
154 | 153 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑛 − 𝑙) ∈
ℕ0) |
155 | 19, 31, 17, 16, 125, 34, 15, 35, 148, 152, 154 | gsummoncoe1 19674 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)) = ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘)) |
156 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (𝑛 − 𝑙) ∈ V |
157 | | csbov2g 6691 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
158 | 156, 157 | mp1i 13 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
159 | | csbvarg 4003 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
160 | 156, 159 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
161 | 160 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘) = (𝑦 decompPMat (𝑛 − 𝑙))) |
162 | 155, 158,
161 | 3eqtrrd 2661 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat (𝑛 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
163 | 144, 162 | oveq12d 6668 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙))) = (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))) |
164 | 163 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
165 | 124, 164 | syl5eq 2668 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
166 | 165 | oveq2d 6666 |
. . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
167 | 83, 119, 166 | 3eqtr4rd 2667 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛)) |
168 | 61, 73, 167 | 3eqtrd 2660 |
. . . . . 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‘𝐴)))))))‘𝑛)) |
169 | 168 | ralrimiva 2966 |
. . . . 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‘𝐴)))))))‘𝑛)) |
170 | 32 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐴 ∈ Ring) |
171 | 88 | adantr 481 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ CMnd) |
172 | 90 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ℕ0 ∈
V) |
173 | 19 | ply1lmod 19622 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
174 | 32, 173 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ LMod) |
175 | 174 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑄 ∈ LMod) |
176 | 37 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ CMnd) |
177 | | fzfid 12772 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
178 | 32 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
179 | | simp-4r 807 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
180 | | simplrl 800 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
181 | 180 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
182 | 43 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
183 | 179, 181,
182, 45 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
184 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
185 | 184 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
186 | 48 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
187 | 179, 185,
186, 50 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
188 | 178, 183,
187, 53 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
189 | 188 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
∀𝑧 ∈ (0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
190 | 34, 176, 177, 189 | gsummptcl 18366 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
191 | 32 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ Ring) |
192 | 19 | ply1sca 19623 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
193 | 191, 192 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 = (Scalar‘𝑄)) |
194 | 193 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Scalar‘𝑄) = 𝐴) |
195 | 194 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Base‘(Scalar‘𝑄)) = (Base‘𝐴)) |
196 | 190, 195 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄))) |
197 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
198 | 19, 17, 197, 16, 31 | ply1moncl 19641 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0)
→ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
199 | 191, 198 | sylancom 701 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
200 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
201 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑄)) = (Base‘(Scalar‘𝑄)) |
202 | 31, 200, 15, 201 | lmodvscl 18880 |
. . . . . . . . 9
⊢ ((𝑄 ∈ LMod ∧ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄)) ∧ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) → ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
203 | 175, 196,
199, 202 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
204 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
205 | 203, 204 | fmptd 6385 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
206 | 3, 4, 11, 15, 16, 17, 18, 19, 31, 20 | pm2mpmhmlem1 20623 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
207 | 31, 84, 171, 172, 205, 206 | gsumcl 18316 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
208 | 86 | adantr 481 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ Ring) |
209 | 94, 96 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
210 | 209, 98 | fmptd 6385 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
211 | 94, 100 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
212 | 31, 84, 171, 172, 210, 211 | gsumcl 18316 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
213 | 105, 107 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
214 | 213, 109 | fmptd 6385 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
215 | 1, 2, 10, 113 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
216 | 31, 84, 171, 172, 214, 215 | gsumcl 18316 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
217 | 31, 116 | ringcl 18561 |
. . . . . . 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‘𝑄)) |
218 | 208, 212,
216, 217 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) ∈ (Base‘𝑄)) |
219 | | eqid 2622 |
. . . . . . 7
⊢
(coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
220 | | eqid 2622 |
. . . . . . 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‘𝐴))))))) |
221 | 19, 31, 219, 220 | ply1coe1eq 19668 |
. . . . . 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‘𝐴)))))))) |
222 | 170, 207,
218, 221 | syl3anc 1326 |
. . . . 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‘𝐴)))))))) |
223 | 169, 222 | mpbid 222 |
. . . 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‘𝐴))))))) |
224 | 22, 30, 223 | 3eqtrd 2660 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
225 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 20601 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
226 | 1, 2, 8, 225 | syl3anc 1326 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
227 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 20601 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
228 | 1, 2, 10, 227 | syl3anc 1326 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
229 | 226, 228 | oveq12d 6668 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
230 | 224, 229 | eqtr4d 2659 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |
231 | 230 | ralrimivva 2971 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |