Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin) |
2 | | simplr 788 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring) |
3 | | pm2mpmhm.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
4 | | pm2mpmhm.c |
. . . . . . . 8
⊢ 𝐶 = (𝑁 Mat 𝑃) |
5 | 3, 4 | pmatring 20317 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ Ring) |
7 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
8 | 7 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
9 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
10 | 9 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
11 | | pm2mpmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(.r‘𝐶) = (.r‘𝐶) |
13 | 11, 12 | ringcl 18384 |
. . . . . 6
⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
14 | 6, 8, 10, 13 | syl3anc 1318 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
15 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝑄) = ( ·𝑠
‘𝑄) |
16 | | eqid 2610 |
. . . . . 6
⊢
(.g‘(mulGrp‘𝑄)) =
(.g‘(mulGrp‘𝑄)) |
17 | | eqid 2610 |
. . . . . 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 20420 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
22 | 1, 2, 14, 21 | syl3anc 1318 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
23 | | simpllr 795 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
24 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
25 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
26 | 3, 4, 11, 18 | decpmatmul 20396 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
27 | 23, 24, 25, 26 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
28 | 27 | oveq1d 6564 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) = ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
29 | 28 | mpteq2dva 4672 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) |
30 | 29 | oveq2d 6565 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
31 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑄) =
(Base‘𝑄) |
32 | 18 | matring 20068 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
33 | 32 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring) |
34 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐴) =
(Base‘𝐴) |
35 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝐴) = (0g‘𝐴) |
36 | | ringcmn 18404 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd) |
37 | 32, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ CMnd) |
38 | 37 | ad3antrrr 762 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
CMnd) |
39 | | fzfid 12634 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0...𝑘) ∈
Fin) |
40 | 33 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
41 | | simp-5r 805 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
42 | 8 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
43 | | elfznn0 12302 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
45 | 3, 4, 11, 18, 34 | decpmatcl 20391 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ ℕ0) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
46 | 41, 42, 44, 45 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
47 | 10 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
48 | | fznn0sub 12244 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → (𝑘 − 𝑧) ∈
ℕ0) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
50 | 3, 4, 11, 18, 34 | decpmatcl 20391 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ (𝑘 − 𝑧) ∈ ℕ0) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
51 | 41, 47, 49, 50 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
52 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(.r‘𝐴) = (.r‘𝐴) |
53 | 34, 52 | ringcl 18384 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Ring ∧ (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴) ∧ (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
54 | 40, 46, 51, 53 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
55 | 54 | ralrimiva 2949 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ∀𝑧 ∈
(0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
56 | 34, 38, 39, 55 | gsummptcl 18189 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
57 | 56 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
58 | 3, 4, 11, 18, 52, 35 | decpmatmulsumfsupp 20397 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
59 | 58 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
60 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
61 | 19, 31, 17, 16, 33, 34, 15, 35, 57, 59, 60 | gsummoncoe1 19495 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ⦋𝑛 / 𝑘⦌(𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
62 | | csbov2g 6589 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg
⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
63 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) |
64 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (0...𝑘) = (0...𝑛)) |
65 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝑘 − 𝑧) = (𝑛 − 𝑧)) |
66 | 65 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝑦 decompPMat (𝑘 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑧))) |
67 | 66 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) = ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) |
68 | 64, 67 | mpteq12dv 4663 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
69 | 68 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 = 𝑛) → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
70 | 63, 69 | csbied 3526 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
71 | 70 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (𝐴
Σg ⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
72 | 62, 71 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
73 | 72 | adantl 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
⦋𝑛 / 𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
74 | | eqidd 2611 |
. . . . . . . . 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 6557 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑛 → (0...𝑟) = (0...𝑛)) |
76 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑛 → (𝑟 − 𝑙) = (𝑛 − 𝑙)) |
77 | 76 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑛 → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
78 | 77 | oveq2d 6565 |
. . . . . . . . . . . 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 4663 |
. . . . . . . . . . 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 6565 |
. . . . . . . . . 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 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
82 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐴 Σg
(𝑙 ∈ (0...𝑛) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) ∈ V |
83 | 82 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑙 ∈ (0...𝑛) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) ∈ V) |
84 | 74, 81, 60, 83 | fvmptd 6197 |
. . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
85 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝑄) = (0g‘𝑄) |
86 | 19 | ply1ring 19439 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
87 | 32, 86 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Ring) |
88 | | ringcmn 18404 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd) |
90 | 89 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑄 ∈ CMnd) |
91 | | nn0ex 11175 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
92 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
ℕ0 ∈ V) |
93 | 7 | anim2i 591 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
94 | | df-3an 1033 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
95 | 93, 94 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
96 | 95 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
97 | 3, 4, 11, 15, 16, 17, 18, 19, 31 | pm2mpghmlem1 20437 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
98 | 96, 97 | sylan 487 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑥 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
99 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
100 | 98, 99 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
101 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 20436 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
102 | 96, 101 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
103 | 31, 85, 90, 92, 100, 102 | gsumcl 18139 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
104 | 9 | anim2i 591 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
105 | | df-3an 1033 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
106 | 104, 105 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
107 | 106 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
108 | 3, 4, 11, 15, 16, 17, 18, 19, 31 | pm2mpghmlem1 20437 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
109 | 107, 108 | sylan 487 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑦 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
110 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
111 | 109, 110 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
112 | 1, 2, 10 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
113 | 112 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
114 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 20436 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
116 | 31, 85, 90, 92, 111, 115 | gsumcl 18139 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
117 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.r‘𝑄) = (.r‘𝑄) |
118 | 19, 117, 52, 31 | coe1mul 19461 |
. . . . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))) |
119 | 118 | fveq1d 6105 |
. . . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
120 | 33, 103, 116, 119 | syl3anc 1318 |
. . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
121 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑥 decompPMat 𝑧) = (𝑥 decompPMat 𝑙)) |
122 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑙 → (𝑛 − 𝑧) = (𝑛 − 𝑙)) |
123 | 122 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑦 decompPMat (𝑛 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑙))) |
124 | 121, 123 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑙 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))) = ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
125 | 124 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
126 | 32 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝐴 ∈ Ring) |
127 | | simp-5r 805 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
128 | 8 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
129 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
130 | 3, 4, 11, 18, 34 | decpmatcl 20391 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
131 | 127, 128,
129, 130 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
132 | 131 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
133 | 2, 8 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
134 | 133 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
135 | 3, 4, 11, 18, 35 | decpmatfsupp 20393 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
137 | | elfznn0 12302 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℕ0) |
138 | 137 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑙 ∈ ℕ0) |
139 | 19, 31, 17, 16, 126, 34, 15, 35, 132, 136, 138 | gsummoncoe1 19495 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘)) |
140 | | csbov2g 6589 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘)) |
141 | | csbvarg 3955 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌𝑘 = 𝑙) |
142 | 141 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘) = (𝑥 decompPMat 𝑙)) |
143 | 140, 142 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
144 | 143 | adantl 481 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
145 | 139, 144 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑥 decompPMat 𝑙) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)) |
146 | 10 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
147 | 3, 4, 11, 18, 34 | decpmatcl 20391 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
148 | 127, 146,
129, 147 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
149 | 148 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
150 | 2, 10 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
151 | 150 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
152 | 3, 4, 11, 18, 35 | decpmatfsupp 20393 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
154 | | fznn0sub 12244 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑛 − 𝑙) ∈
ℕ0) |
155 | 154 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑛 − 𝑙) ∈
ℕ0) |
156 | 19, 31, 17, 16, 126, 34, 15, 35, 149, 153, 155 | gsummoncoe1 19495 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)) = ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘)) |
157 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (𝑛 − 𝑙) ∈ V |
158 | | csbov2g 6589 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
159 | 157, 158 | mp1i 13 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
160 | | csbvarg 3955 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
161 | 157, 160 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
162 | 161 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘) = (𝑦 decompPMat (𝑛 − 𝑙))) |
163 | 156, 159,
162 | 3eqtrrd 2649 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat (𝑛 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
164 | 145, 163 | oveq12d 6567 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙))) = (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))) |
165 | 164 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
166 | 125, 165 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
167 | 166 | oveq2d 6565 |
. . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
168 | 84, 120, 167 | 3eqtr4rd 2655 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛)) |
169 | 61, 73, 168 | 3eqtrd 2648 |
. . . . . 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‘𝐴)))))))‘𝑛)) |
170 | 169 | ralrimiva 2949 |
. . . . 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‘𝐴)))))))‘𝑛)) |
171 | 32 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐴 ∈ Ring) |
172 | 89 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ CMnd) |
173 | 91 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ℕ0 ∈
V) |
174 | 19 | ply1lmod 19443 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
175 | 32, 174 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ LMod) |
176 | 175 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑄 ∈ LMod) |
177 | 37 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ CMnd) |
178 | | fzfid 12634 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
179 | 32 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
180 | | simp-4r 803 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
181 | | simplrl 796 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
182 | 181 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
183 | 43 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
184 | 180, 182,
183, 45 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
185 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
186 | 185 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
187 | 48 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
188 | 180, 186,
187, 50 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
189 | 179, 184,
188, 53 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
190 | 189 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
∀𝑧 ∈ (0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
191 | 34, 177, 178, 190 | gsummptcl 18189 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
192 | 32 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ Ring) |
193 | 19 | ply1sca 19444 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
194 | 192, 193 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 = (Scalar‘𝑄)) |
195 | 194 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Scalar‘𝑄) = 𝐴) |
196 | 195 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Base‘(Scalar‘𝑄)) = (Base‘𝐴)) |
197 | 191, 196 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄))) |
198 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
199 | 19, 17, 198, 16, 31 | ply1moncl 19462 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0)
→ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
200 | 192, 199 | sylancom 698 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
201 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
202 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑄)) = (Base‘(Scalar‘𝑄)) |
203 | 31, 201, 15, 202 | lmodvscl 18703 |
. . . . . . . . 9
⊢ ((𝑄 ∈ LMod ∧ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄)) ∧ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) → ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
204 | 176, 197,
200, 203 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
205 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
206 | 204, 205 | fmptd 6292 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
207 | 3, 4, 11, 15, 16, 17, 18, 19, 31, 20 | pm2mpmhmlem1 20442 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
208 | 31, 85, 172, 173, 206, 207 | gsumcl 18139 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
209 | 87 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ Ring) |
210 | 95, 97 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
211 | 210, 99 | fmptd 6292 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
212 | 95, 101 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
213 | 31, 85, 172, 173, 211, 212 | gsumcl 18139 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
214 | 106, 108 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
215 | 214, 110 | fmptd 6292 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
216 | 1, 2, 10, 114 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
217 | 31, 85, 172, 173, 215, 216 | gsumcl 18139 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
218 | 31, 117 | ringcl 18384 |
. . . . . . 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‘𝑄)) |
219 | 209, 213,
217, 218 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) ∈ (Base‘𝑄)) |
220 | | eqid 2610 |
. . . . . . 7
⊢
(coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
221 | | eqid 2610 |
. . . . . . 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‘𝐴))))))) |
222 | 19, 31, 220, 221 | ply1coe1eq 19489 |
. . . . . 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‘𝐴)))))))) |
223 | 171, 208,
219, 222 | syl3anc 1318 |
. . . . 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‘𝐴)))))))) |
224 | 170, 223 | mpbid 221 |
. . . 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‘𝐴))))))) |
225 | 22, 30, 224 | 3eqtrd 2648 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
226 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 20420 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
227 | 1, 2, 8, 226 | syl3anc 1318 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
228 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 20420 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
229 | 1, 2, 10, 228 | syl3anc 1318 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
230 | 227, 229 | oveq12d 6567 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
231 | 225, 230 | eqtr4d 2647 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |
232 | 231 | ralrimivva 2954 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |