Step | Hyp | Ref
| Expression |
1 | | crngring 18381 |
. . 3
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
2 | | simpll 786 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ Fin) |
3 | | simplr 788 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → 𝑅 ∈ Ring) |
4 | | monmat2matmon.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
5 | | monmat2matmon.k |
. . . . 5
⊢ 𝐾 = (Base‘𝐴) |
6 | | monmat2matmon.t |
. . . . 5
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
7 | | monmat2matmon.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
8 | | monmat2matmon.c |
. . . . 5
⊢ 𝐶 = (𝑁 Mat 𝑃) |
9 | | monmat2matmon.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
10 | | monmat2matmon.m2 |
. . . . 5
⊢ · = (
·𝑠 ‘𝐶) |
11 | | monmat2matmon.e2 |
. . . . 5
⊢ 𝐸 =
(.g‘(mulGrp‘𝑃)) |
12 | | monmat2matmon.y |
. . . . 5
⊢ 𝑌 = (var1‘𝑅) |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | mat2pmatscmxcl 20364 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → ((𝐿𝐸𝑌) · (𝑇‘𝑀)) ∈ 𝐵) |
14 | | monmat2matmon.m1 |
. . . . 5
⊢ ∗ = (
·𝑠 ‘𝑄) |
15 | | monmat2matmon.e1 |
. . . . 5
⊢ ↑ =
(.g‘(mulGrp‘𝑄)) |
16 | | monmat2matmon.x |
. . . . 5
⊢ 𝑋 = (var1‘𝐴) |
17 | | monmat2matmon.q |
. . . . 5
⊢ 𝑄 = (Poly1‘𝐴) |
18 | | monmat2matmon.i |
. . . . 5
⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) |
19 | 7, 8, 9, 14, 15, 16, 4, 17, 18 | pm2mpfval 20420 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ((𝐿𝐸𝑌) · (𝑇‘𝑀)) ∈ 𝐵) → (𝐼‘((𝐿𝐸𝑌) · (𝑇‘𝑀))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
20 | 2, 3, 13, 19 | syl3anc 1318 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝐼‘((𝐿𝐸𝑌) · (𝑇‘𝑀))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
21 | 1, 20 | sylanl2 681 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝐼‘((𝐿𝐸𝑌) · (𝑇‘𝑀))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
22 | | simpll 786 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (𝑁 ∈ Fin ∧
𝑅 ∈
CRing)) |
23 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝑀 ∈ 𝐾 ∧ 𝐿 ∈
ℕ0)) |
24 | 23 | anim1i 590 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ ((𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 ∈
ℕ0)) |
25 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0)
↔ ((𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 ∈
ℕ0)) |
26 | 24, 25 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝑘 ∈
ℕ0)) |
27 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐴) = (0g‘𝐴) |
28 | 7, 8, 4, 5, 27, 11, 12, 10, 6 | monmatcollpw 20403 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0))
→ (((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) = if(𝑘 = 𝐿, 𝑀, (0g‘𝐴))) |
29 | 22, 26, 28 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) = if(𝑘 = 𝐿, 𝑀, (0g‘𝐴))) |
30 | 29 | oveq1d 6564 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) = (if(𝑘 = 𝐿, 𝑀, (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋))) |
31 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑅 ∈ CRing
→ 𝑅 ∈
Ring)) |
32 | 31 | anim2d 587 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((𝑁 ∈ Fin ∧
𝑅 ∈ CRing) →
(𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))) |
33 | 32 | anim1d 586 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing) ∧
(𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈
ℕ0)))) |
34 | 33 | imdistanri 723 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈
ℕ0)) |
35 | | ovif 6635 |
. . . . . . . 8
⊢ (if(𝑘 = 𝐿, 𝑀, (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋)) = if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋))) |
36 | 4 | matring 20068 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
37 | 17 | ply1sca 19444 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 = (Scalar‘𝑄)) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 =
(Scalar‘𝑄)) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (0g‘𝐴) = (0g‘(Scalar‘𝑄))) |
41 | 40 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋)) =
((0g‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋))) |
42 | 17 | ply1lmod 19443 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
43 | 36, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ LMod) |
44 | 43 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ 𝑄 ∈
LMod) |
45 | 17 | ply1ring 19439 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
46 | 36, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Ring) |
47 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
48 | 47 | ringmgp 18376 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ Ring →
(mulGrp‘𝑄) ∈
Mnd) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(mulGrp‘𝑄) ∈
Mnd) |
50 | 49 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (mulGrp‘𝑄)
∈ Mnd) |
51 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) |
52 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑄) =
(Base‘𝑄) |
53 | 16, 17, 52 | vr1cl 19408 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Ring → 𝑋 ∈ (Base‘𝑄)) |
54 | 36, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑋 ∈ (Base‘𝑄)) |
55 | 54 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ 𝑋 ∈
(Base‘𝑄)) |
56 | 47, 52 | mgpbas 18318 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑄) =
(Base‘(mulGrp‘𝑄)) |
57 | 56, 15 | mulgnn0cl 17381 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑄)
∈ Mnd ∧ 𝑘 ∈
ℕ0 ∧ 𝑋
∈ (Base‘𝑄))
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) |
58 | 50, 51, 55, 57 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) |
59 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
60 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝑄)) =
(0g‘(Scalar‘𝑄)) |
61 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘𝑄) = (0g‘𝑄) |
62 | 52, 59, 14, 60, 61 | lmod0vs 18719 |
. . . . . . . . . . 11
⊢ ((𝑄 ∈ LMod ∧ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) →
((0g‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑄)) |
63 | 44, 58, 62 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑄)) |
64 | 41, 63 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑄)) |
65 | 64 | ifeq2d 4055 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋))) = if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄))) |
66 | 35, 65 | syl5eq 2656 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (if(𝑘 = 𝐿, 𝑀, (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋)) = if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄))) |
67 | 34, 66 | syl 17 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (if(𝑘 = 𝐿, 𝑀, (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋)) = if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄))) |
68 | 30, 67 | eqtrd 2644 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) = if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄))) |
69 | 68 | mpteq2dva 4672 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝑘 ∈ ℕ0
↦ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄)))) |
70 | 69 | oveq2d 6565 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄))))) |
71 | | ringmnd 18379 |
. . . . . . 7
⊢ (𝑄 ∈ Ring → 𝑄 ∈ Mnd) |
72 | 46, 71 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Mnd) |
73 | 72 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → 𝑄 ∈ Mnd) |
74 | | nn0ex 11175 |
. . . . . 6
⊢
ℕ0 ∈ V |
75 | 74 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) →
ℕ0 ∈ V) |
76 | | simprr 792 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈
ℕ0) |
77 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄))) |
78 | 38 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝐴) =
(Base‘(Scalar‘𝑄))) |
79 | 5, 78 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐾 =
(Base‘(Scalar‘𝑄))) |
80 | 79 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝐾 ↔ 𝑀 ∈ (Base‘(Scalar‘𝑄)))) |
81 | 80 | biimpcd 238 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝐾 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑀 ∈ (Base‘(Scalar‘𝑄)))) |
82 | 81 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑀 ∈
(Base‘(Scalar‘𝑄)))) |
83 | 82 | impcom 445 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈
(Base‘(Scalar‘𝑄))) |
84 | 83 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ 𝑀 ∈
(Base‘(Scalar‘𝑄))) |
85 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑄)) = (Base‘(Scalar‘𝑄)) |
86 | 52, 59, 14, 85 | lmodvscl 18703 |
. . . . . . 7
⊢ ((𝑄 ∈ LMod ∧ 𝑀 ∈
(Base‘(Scalar‘𝑄)) ∧ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) → (𝑀 ∗ (𝑘 ↑ 𝑋)) ∈ (Base‘𝑄)) |
87 | 44, 84, 58, 86 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) ∧ 𝑘 ∈ ℕ0)
→ (𝑀 ∗ (𝑘 ↑ 𝑋)) ∈ (Base‘𝑄)) |
88 | 87 | ralrimiva 2949 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) →
∀𝑘 ∈
ℕ0 (𝑀
∗
(𝑘 ↑ 𝑋)) ∈ (Base‘𝑄)) |
89 | 61, 73, 75, 76, 77, 88 | gsummpt1n0 18187 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄)))) = ⦋𝐿 / 𝑘⦌(𝑀 ∗ (𝑘 ↑ 𝑋))) |
90 | 1, 89 | sylanl2 681 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ if(𝑘 = 𝐿, (𝑀 ∗ (𝑘 ↑ 𝑋)), (0g‘𝑄)))) = ⦋𝐿 / 𝑘⦌(𝑀 ∗ (𝑘 ↑ 𝑋))) |
91 | 70, 90 | eqtrd 2644 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ ((((𝐿𝐸𝑌) · (𝑇‘𝑀)) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) = ⦋𝐿 / 𝑘⦌(𝑀 ∗ (𝑘 ↑ 𝑋))) |
92 | | csbov2g 6589 |
. . . 4
⊢ (𝐿 ∈ ℕ0
→ ⦋𝐿 /
𝑘⦌(𝑀 ∗ (𝑘 ↑ 𝑋)) = (𝑀 ∗
⦋𝐿 / 𝑘⦌(𝑘 ↑ 𝑋))) |
93 | | csbov1g 6588 |
. . . . . 6
⊢ (𝐿 ∈ ℕ0
→ ⦋𝐿 /
𝑘⦌(𝑘 ↑ 𝑋) = (⦋𝐿 / 𝑘⦌𝑘 ↑ 𝑋)) |
94 | | csbvarg 3955 |
. . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ ⦋𝐿 /
𝑘⦌𝑘 = 𝐿) |
95 | 94 | oveq1d 6564 |
. . . . . 6
⊢ (𝐿 ∈ ℕ0
→ (⦋𝐿 /
𝑘⦌𝑘 ↑ 𝑋) = (𝐿 ↑ 𝑋)) |
96 | 93, 95 | eqtrd 2644 |
. . . . 5
⊢ (𝐿 ∈ ℕ0
→ ⦋𝐿 /
𝑘⦌(𝑘 ↑ 𝑋) = (𝐿 ↑ 𝑋)) |
97 | 96 | oveq2d 6565 |
. . . 4
⊢ (𝐿 ∈ ℕ0
→ (𝑀 ∗
⦋𝐿 / 𝑘⦌(𝑘 ↑ 𝑋)) = (𝑀 ∗ (𝐿 ↑ 𝑋))) |
98 | 92, 97 | eqtrd 2644 |
. . 3
⊢ (𝐿 ∈ ℕ0
→ ⦋𝐿 /
𝑘⦌(𝑀 ∗ (𝑘 ↑ 𝑋)) = (𝑀 ∗ (𝐿 ↑ 𝑋))) |
99 | 98 | ad2antll 761 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) →
⦋𝐿 / 𝑘⦌(𝑀 ∗ (𝑘 ↑ 𝑋)) = (𝑀 ∗ (𝐿 ↑ 𝑋))) |
100 | 21, 91, 99 | 3eqtrd 2648 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝐼‘((𝐿𝐸𝑌) · (𝑇‘𝑀))) = (𝑀 ∗ (𝐿 ↑ 𝑋))) |