Step | Hyp | Ref
| Expression |
1 | | simpll 783 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin) |
2 | | simplr 785 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring) |
3 | | pm2mpmhm.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
4 | | pm2mpmhm.c |
. . . . . . . 8
⊢ 𝐶 = (𝑁 Mat 𝑃) |
5 | 3, 4 | pmatring 20875 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
6 | 5 | adantr 474 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ Ring) |
7 | | simpl 476 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
8 | 7 | adantl 475 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
9 | | simpr 479 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
10 | 9 | adantl 475 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
11 | | pm2mpmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
12 | | eqid 2825 |
. . . . . . 7
⊢
(.r‘𝐶) = (.r‘𝐶) |
13 | 11, 12 | ringcl 18922 |
. . . . . 6
⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
14 | 6, 8, 10, 13 | syl3anc 1494 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) |
15 | | eqid 2825 |
. . . . . 6
⊢ (
·𝑠 ‘𝑄) = ( ·𝑠
‘𝑄) |
16 | | eqid 2825 |
. . . . . 6
⊢
(.g‘(mulGrp‘𝑄)) =
(.g‘(mulGrp‘𝑄)) |
17 | | eqid 2825 |
. . . . . 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 20978 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐶)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
22 | 1, 2, 14, 21 | syl3anc 1494 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
23 | | simpllr 793 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
24 | | simplr 785 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
25 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
26 | 3, 4, 11, 18 | decpmatmul 20954 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
27 | 23, 24, 25, 26 | syl3anc 1494 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘) = (𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
28 | 27 | oveq1d 6925 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) = ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) |
29 | 28 | mpteq2dva 4969 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) = (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) |
30 | 29 | oveq2d 6926 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((𝑥(.r‘𝐶)𝑦) decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
31 | | eqid 2825 |
. . . . . . . 8
⊢
(Base‘𝑄) =
(Base‘𝑄) |
32 | 18 | matring 20623 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
33 | 32 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring) |
34 | | eqid 2825 |
. . . . . . . 8
⊢
(Base‘𝐴) =
(Base‘𝐴) |
35 | | eqid 2825 |
. . . . . . . 8
⊢
(0g‘𝐴) = (0g‘𝐴) |
36 | | ringcmn 18942 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd) |
37 | 32, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ CMnd) |
38 | 37 | ad3antrrr 721 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
CMnd) |
39 | | fzfid 13074 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0...𝑘) ∈
Fin) |
40 | 33 | ad2antrr 717 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
41 | | simp-5r 807 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
42 | 8 | ad3antrrr 721 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
43 | | elfznn0 12734 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0) |
44 | 43 | adantl 475 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
45 | 3, 4, 11, 18, 34 | decpmatcl 20949 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ ℕ0) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
46 | 41, 42, 44, 45 | syl3anc 1494 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
47 | 10 | ad3antrrr 721 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
48 | | fznn0sub 12673 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0...𝑘) → (𝑘 − 𝑧) ∈
ℕ0) |
49 | 48 | adantl 475 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
50 | 3, 4, 11, 18, 34 | decpmatcl 20949 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ (𝑘 − 𝑧) ∈ ℕ0) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
51 | 41, 47, 49, 50 | syl3anc 1494 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
52 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢
(.r‘𝐴) = (.r‘𝐴) |
53 | 34, 52 | ringcl 18922 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Ring ∧ (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴) ∧ (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
54 | 40, 46, 51, 53 | syl3anc 1494 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
55 | 54 | ralrimiva 3175 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ∀𝑧 ∈
(0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
56 | 34, 38, 39, 55 | gsummptcl 18726 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
57 | 56 | ralrimiva 3175 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
58 | 3, 4, 11, 18, 52, 35 | decpmatmulsumfsupp 20955 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
59 | 58 | adantr 474 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) finSupp (0g‘𝐴)) |
60 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
61 | 19, 31, 17, 16, 33, 34, 15, 35, 57, 59, 60 | gsummoncoe1 20041 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑛) = ⦋𝑛 / 𝑘⦌(𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
62 | | csbov2g 6955 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg
⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))) |
63 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) |
64 | | oveq2 6918 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (0...𝑘) = (0...𝑛)) |
65 | | oveq1 6917 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝑘 − 𝑧) = (𝑛 − 𝑧)) |
66 | 65 | oveq2d 6926 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝑦 decompPMat (𝑘 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑧))) |
67 | 66 | oveq2d 6926 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) = ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) |
68 | 64, 67 | mpteq12dv 4958 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
69 | 68 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 = 𝑛) → (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
70 | 63, 69 | csbied 3784 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))) = (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) |
71 | 70 | oveq2d 6926 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (𝐴
Σg ⦋𝑛 / 𝑘⦌(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
72 | 62, 71 | eqtrd 2861 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ⦋𝑛 /
𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
73 | 72 | adantl 475 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
⦋𝑛 / 𝑘⦌(𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) = (𝐴 Σg (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))))) |
74 | | eqidd 2826 |
. . . . . . . . 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 6918 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑛 → (0...𝑟) = (0...𝑛)) |
76 | | fvoveq1 6933 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑛 → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑟 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
77 | 76 | oveq2d 6926 |
. . . . . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))) |
78 | 75, 77 | mpteq12dv 4958 |
. . . . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙))))) |
79 | 78 | oveq2d 6926 |
. . . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
80 | 79 | adantl 475 |
. . . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
81 | | ovexd 6944 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑙 ∈ (0...𝑛) ↦
(((coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) ∈ V) |
82 | 74, 80, 60, 81 | fvmptd 6539 |
. . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
83 | | eqid 2825 |
. . . . . . . . . 10
⊢
(0g‘𝑄) = (0g‘𝑄) |
84 | 19 | ply1ring 19985 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
85 | 32, 84 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Ring) |
86 | | ringcmn 18942 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd) |
88 | 87 | ad2antrr 717 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑄 ∈ CMnd) |
89 | | nn0ex 11632 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
90 | 89 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) →
ℕ0 ∈ V) |
91 | 7 | anim2i 610 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
92 | | df-3an 1113 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
93 | 91, 92 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
94 | 93 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
95 | 3, 4, 11, 15, 16, 17, 18, 19, 31 | pm2mpghmlem1 20995 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
96 | 94, 95 | sylan 575 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑥 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
97 | 96 | fmpttd 6639 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
98 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 20994 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
99 | 94, 98 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
100 | 31, 83, 88, 90, 97, 99 | gsumcl 18676 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
101 | 9 | anim2i 610 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
102 | | df-3an 1113 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
103 | 101, 102 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
104 | 103 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
105 | 3, 4, 11, 15, 16, 17, 18, 19, 31 | pm2mpghmlem1 20995 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
106 | 104, 105 | sylan 575 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑦 decompPMat 𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
107 | 106 | fmpttd 6639 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
108 | 1, 2, 10 | 3jca 1162 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
109 | 108 | adantr 474 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
110 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 20994 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
112 | 31, 83, 88, 90, 107, 111 | gsumcl 18676 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
113 | | eqid 2825 |
. . . . . . . . . . 11
⊢
(.r‘𝑄) = (.r‘𝑄) |
114 | 19, 113, 52, 31 | coe1mul 20007 |
. . . . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))) |
115 | 114 | fveq1d 6439 |
. . . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
116 | 33, 100, 112, 115 | syl3anc 1494 |
. . . . . . . 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‘𝐴))))))‘(𝑟 − 𝑙))))))‘𝑛)) |
117 | | oveq2 6918 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑥 decompPMat 𝑧) = (𝑥 decompPMat 𝑙)) |
118 | | oveq2 6918 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑙 → (𝑛 − 𝑧) = (𝑛 − 𝑙)) |
119 | 118 | oveq2d 6926 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑙 → (𝑦 decompPMat (𝑛 − 𝑧)) = (𝑦 decompPMat (𝑛 − 𝑙))) |
120 | 117, 119 | oveq12d 6928 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑙 → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))) = ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
121 | 120 | cbvmptv 4975 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) |
122 | 32 | ad3antrrr 721 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝐴 ∈ Ring) |
123 | | simp-5r 807 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
124 | 8 | ad3antrrr 721 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
125 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
126 | 3, 4, 11, 18, 34 | decpmatcl 20949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
127 | 123, 124,
125, 126 | syl3anc 1494 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
128 | 127 | ralrimiva 3175 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑥 decompPMat 𝑘) ∈ (Base‘𝐴)) |
129 | 2, 8 | jca 507 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
130 | 129 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
131 | 3, 4, 11, 18, 35 | decpmatfsupp 20951 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑥 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
133 | | elfznn0 12734 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℕ0) |
134 | 133 | adantl 475 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑙 ∈ ℕ0) |
135 | 19, 31, 17, 16, 122, 34, 15, 35, 128, 132, 134 | gsummoncoe1 20041 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙) = ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘)) |
136 | | csbov2g 6955 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘)) |
137 | | csbvarg 4229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌𝑘 = 𝑙) |
138 | 137 | oveq2d 6926 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑥 decompPMat ⦋𝑙 / 𝑘⦌𝑘) = (𝑥 decompPMat 𝑙)) |
139 | 136, 138 | eqtrd 2861 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ (0...𝑛) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
140 | 139 | adantl 475 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋𝑙 / 𝑘⦌(𝑥 decompPMat 𝑘) = (𝑥 decompPMat 𝑙)) |
141 | 135, 140 | eqtr2d 2862 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑥 decompPMat 𝑙) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)) |
142 | 10 | ad3antrrr 721 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
143 | 3, 4, 11, 18, 34 | decpmatcl 20949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
144 | 123, 142,
125, 143 | syl3anc 1494 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ 𝑘 ∈ ℕ0) → (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
145 | 144 | ralrimiva 3175 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ∀𝑘 ∈ ℕ0 (𝑦 decompPMat 𝑘) ∈ (Base‘𝐴)) |
146 | 2, 10 | jca 507 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
147 | 146 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
148 | 3, 4, 11, 18, 35 | decpmatfsupp 20951 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
149 | 147, 148 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ↦ (𝑦 decompPMat 𝑘)) finSupp (0g‘𝐴)) |
150 | | fznn0sub 12673 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ (0...𝑛) → (𝑛 − 𝑙) ∈
ℕ0) |
151 | 150 | adantl 475 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑛 − 𝑙) ∈
ℕ0) |
152 | 19, 31, 17, 16, 122, 34, 15, 35, 145, 149, 151 | gsummoncoe1 20041 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)) = ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘)) |
153 | | ovex 6942 |
. . . . . . . . . . . . . 14
⊢ (𝑛 − 𝑙) ∈ V |
154 | | csbov2g 6955 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
155 | 153, 154 | mp1i 13 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌(𝑦 decompPMat 𝑘) = (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘)) |
156 | | csbvarg 4229 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 𝑙) ∈ V → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
157 | 153, 156 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘 = (𝑛 − 𝑙)) |
158 | 157 | oveq2d 6926 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat ⦋(𝑛 − 𝑙) / 𝑘⦌𝑘) = (𝑦 decompPMat (𝑛 − 𝑙))) |
159 | 152, 155,
158 | 3eqtrrd 2866 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑦 decompPMat (𝑛 − 𝑙)) = ((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))) |
160 | 141, 159 | oveq12d 6928 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙))) = (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙)))) |
161 | 160 | mpteq2dva 4969 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑙 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑙)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
162 | 121, 161 | syl5eq 2873 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧)))) = (𝑙 ∈ (0...𝑛) ↦ (((coe1‘(𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘𝑙)(.r‘𝐴)((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))‘(𝑛 − 𝑙))))) |
163 | 162 | oveq2d 6926 |
. . . . . . . 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‘𝐴))))))‘(𝑛 − 𝑙)))))) |
164 | 82, 116, 163 | 3eqtr4rd 2872 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑛 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑛) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑛 − 𝑧))))) = ((coe1‘((𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))))‘𝑛)) |
165 | 61, 73, 164 | 3eqtrd 2865 |
. . . . . 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‘𝐴)))))))‘𝑛)) |
166 | 165 | ralrimiva 3175 |
. . . . 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‘𝐴)))))))‘𝑛)) |
167 | 32 | adantr 474 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐴 ∈ Ring) |
168 | 87 | adantr 474 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ CMnd) |
169 | 89 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ℕ0 ∈
V) |
170 | 19 | ply1lmod 19989 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
171 | 32, 170 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ LMod) |
172 | 171 | ad2antrr 717 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑄 ∈ LMod) |
173 | 37 | ad2antrr 717 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ CMnd) |
174 | | fzfid 13074 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
175 | 32 | ad3antrrr 721 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝐴 ∈ Ring) |
176 | | simp-4r 803 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
177 | | simplrl 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈ 𝐵) |
178 | 177 | adantr 474 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑥 ∈ 𝐵) |
179 | 43 | adantl 475 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑧 ∈ ℕ0) |
180 | 176, 178,
179, 45 | syl3anc 1494 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑥 decompPMat 𝑧) ∈ (Base‘𝐴)) |
181 | | simplrr 796 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝑦 ∈ 𝐵) |
182 | 181 | adantr 474 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → 𝑦 ∈ 𝐵) |
183 | 48 | adantl 475 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑘 − 𝑧) ∈
ℕ0) |
184 | 176, 182,
183, 50 | syl3anc 1494 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → (𝑦 decompPMat (𝑘 − 𝑧)) ∈ (Base‘𝐴)) |
185 | 175, 180,
184, 53 | syl3anc 1494 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) ∧ 𝑧 ∈ (0...𝑘)) → ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
186 | 185 | ralrimiva 3175 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
∀𝑧 ∈ (0...𝑘)((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))) ∈ (Base‘𝐴)) |
187 | 34, 173, 174, 186 | gsummptcl 18726 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘𝐴)) |
188 | 32 | ad2antrr 717 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ Ring) |
189 | 19 | ply1sca 19990 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
190 | 188, 189 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → 𝐴 = (Scalar‘𝑄)) |
191 | 190 | eqcomd 2831 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Scalar‘𝑄) = 𝐴) |
192 | 191 | fveq2d 6441 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) →
(Base‘(Scalar‘𝑄)) = (Base‘𝐴)) |
193 | 187, 192 | eleqtrrd 2909 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄))) |
194 | | eqid 2825 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
195 | 19, 17, 194, 16, 31 | ply1moncl 20008 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0)
→ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
196 | 188, 195 | sylancom 582 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) |
197 | | eqid 2825 |
. . . . . . . . . 10
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
198 | | eqid 2825 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑄)) = (Base‘(Scalar‘𝑄)) |
199 | 31, 197, 15, 198 | lmodvscl 19243 |
. . . . . . . . 9
⊢ ((𝑄 ∈ LMod ∧ (𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧))))) ∈ (Base‘(Scalar‘𝑄)) ∧ (𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)) ∈ (Base‘𝑄)) → ((𝐴 Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
200 | 172, 193,
196, 199 | syl3anc 1494 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
201 | 200 | fmpttd 6639 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
202 | 3, 4, 11, 15, 16, 17, 18, 19, 31, 20 | pm2mpmhmlem1 21000 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
203 | 31, 83, 168, 169, 201, 202 | gsumcl 18676 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
204 | 85 | adantr 474 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑄 ∈ Ring) |
205 | 93, 95 | sylan 575 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
206 | 205 | fmpttd 6639 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
207 | 93, 98 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑥 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
208 | 31, 83, 168, 169, 206, 207 | gsumcl 18676 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
209 | 103, 105 | sylan 575 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ ℕ0) → ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))) ∈ (Base‘𝑄)) |
210 | 209 | fmpttd 6639 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))):ℕ0⟶(Base‘𝑄)) |
211 | 1, 2, 10, 110 | syl3anc 1494 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ ℕ0 ↦ ((𝑦 decompPMat 𝑘)( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))) finSupp
(0g‘𝑄)) |
212 | 31, 83, 168, 169, 210, 211 | gsumcl 18676 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))) ∈ (Base‘𝑄)) |
213 | 31, 113 | ringcl 18922 |
. . . . . . 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‘𝑄)) |
214 | 204, 208,
212, 213 | syl3anc 1494 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) ∈ (Base‘𝑄)) |
215 | | eqid 2825 |
. . . . . . 7
⊢
(coe1‘(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝐴
Σg (𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) =
(coe1‘(𝑄
Σg (𝑘 ∈ ℕ0 ↦ ((𝐴 Σg
(𝑧 ∈ (0...𝑘) ↦ ((𝑥 decompPMat 𝑧)(.r‘𝐴)(𝑦 decompPMat (𝑘 − 𝑧)))))( ·𝑠
‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
216 | | eqid 2825 |
. . . . . . 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‘𝐴))))))) |
217 | 19, 31, 215, 216 | ply1coe1eq 20035 |
. . . . . 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‘𝐴)))))))) |
218 | 167, 203,
214, 217 | syl3anc 1494 |
. . . . 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‘𝐴)))))))) |
219 | 166, 218 | mpbid 224 |
. . . 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‘𝐴))))))) |
220 | 22, 30, 219 | 3eqtrd 2865 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
221 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 20978 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
222 | 1, 2, 8, 221 | syl3anc 1494 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
223 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 20978 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
224 | 1, 2, 10, 223 | syl3anc 1494 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))) |
225 | 222, 224 | oveq12d 6928 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦)) = ((𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑥 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴)))))(.r‘𝑄)(𝑄 Σg (𝑘 ∈ ℕ0
↦ ((𝑦 decompPMat
𝑘)(
·𝑠 ‘𝑄)(𝑘(.g‘(mulGrp‘𝑄))(var1‘𝐴))))))) |
226 | 220, 225 | eqtr4d 2864 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |
227 | 226 | ralrimivva 3180 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) |