Step | Hyp | Ref
| Expression |
1 | | pm2mpval.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | pm2mpval.c |
. . . . 5
⊢ 𝐶 = (𝑁 Mat 𝑃) |
3 | 1, 2 | pmatring 20317 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
4 | | pm2mpval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
5 | | eqid 2610 |
. . . . 5
⊢
(1r‘𝐶) = (1r‘𝐶) |
6 | 4, 5 | ringidcl 18391 |
. . . 4
⊢ (𝐶 ∈ Ring →
(1r‘𝐶)
∈ 𝐵) |
7 | 3, 6 | syl 17 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐶)
∈ 𝐵) |
8 | | pm2mpval.m |
. . . 4
⊢ ∗ = (
·𝑠 ‘𝑄) |
9 | | pm2mpval.e |
. . . 4
⊢ ↑ =
(.g‘(mulGrp‘𝑄)) |
10 | | pm2mpval.x |
. . . 4
⊢ 𝑋 = (var1‘𝐴) |
11 | | pm2mpval.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
12 | | pm2mpval.q |
. . . 4
⊢ 𝑄 = (Poly1‘𝐴) |
13 | | pm2mpval.t |
. . . 4
⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) |
14 | 1, 2, 4, 8, 9, 10,
11, 12, 13 | pm2mpfval 20420 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧
(1r‘𝐶)
∈ 𝐵) → (𝑇‘(1r‘𝐶)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((1r‘𝐶) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
15 | 7, 14 | mpd3an3 1417 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(1r‘𝐶)) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (((1r‘𝐶) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) |
16 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐴) = (0g‘𝐴) |
17 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝐴) = (1r‘𝐴) |
18 | 1, 2, 5, 11, 16, 17 | decpmatid 20394 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑘 ∈ ℕ0)
→ ((1r‘𝐶) decompPMat 𝑘) = if(𝑘 = 0, (1r‘𝐴), (0g‘𝐴))) |
19 | 18 | 3expa 1257 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ ((1r‘𝐶) decompPMat 𝑘) = if(𝑘 = 0, (1r‘𝐴), (0g‘𝐴))) |
20 | 19 | oveq1d 6564 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ (((1r‘𝐶) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) = (if(𝑘 = 0, (1r‘𝐴), (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋))) |
21 | 20 | mpteq2dva 4672 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑘 ∈ ℕ0
↦ (((1r‘𝐶) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, (1r‘𝐴), (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋)))) |
22 | 21 | oveq2d 6565 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ (((1r‘𝐶) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ (if(𝑘 = 0,
(1r‘𝐴),
(0g‘𝐴))
∗
(𝑘 ↑ 𝑋))))) |
23 | | ovif 6635 |
. . . . . 6
⊢ (if(𝑘 = 0, (1r‘𝐴), (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋)) = if(𝑘 = 0, ((1r‘𝐴) ∗ (𝑘 ↑ 𝑋)), ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋))) |
24 | 11 | matring 20068 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
25 | 12 | ply1sca 19444 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 = (Scalar‘𝑄)) |
27 | 26 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 =
(Scalar‘𝑄)) |
28 | 27 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ (1r‘𝐴) = (1r‘(Scalar‘𝑄))) |
29 | 28 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ ((1r‘𝐴) ∗ (𝑘 ↑ 𝑋)) =
((1r‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋))) |
30 | 12 | ply1lmod 19443 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
31 | 24, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ LMod) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ 𝑄 ∈
LMod) |
33 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
34 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑄) =
(Base‘𝑄) |
35 | 12, 10, 33, 9, 34 | ply1moncl 19462 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) |
36 | 24, 35 | sylan 487 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) |
37 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Scalar‘𝑄) =
(Scalar‘𝑄) |
38 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1r‘(Scalar‘𝑄)) =
(1r‘(Scalar‘𝑄)) |
39 | 34, 37, 8, 38 | lmodvs1 18714 |
. . . . . . . . 9
⊢ ((𝑄 ∈ LMod ∧ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) →
((1r‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋)) = (𝑘 ↑ 𝑋)) |
40 | 32, 36, 39 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ ((1r‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋)) = (𝑘 ↑ 𝑋)) |
41 | 29, 40 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ ((1r‘𝐴) ∗ (𝑘 ↑ 𝑋)) = (𝑘 ↑ 𝑋)) |
42 | 27 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ (0g‘𝐴) = (0g‘(Scalar‘𝑄))) |
43 | 42 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋)) =
((0g‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋))) |
44 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑄)) =
(0g‘(Scalar‘𝑄)) |
45 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝑄) = (0g‘𝑄) |
46 | 34, 37, 8, 44, 45 | lmod0vs 18719 |
. . . . . . . . 9
⊢ ((𝑄 ∈ LMod ∧ (𝑘 ↑ 𝑋) ∈ (Base‘𝑄)) →
((0g‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑄)) |
47 | 32, 36, 46 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘(Scalar‘𝑄)) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑄)) |
48 | 43, 47 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋)) = (0g‘𝑄)) |
49 | 41, 48 | ifeq12d 4056 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ if(𝑘 = 0,
((1r‘𝐴)
∗
(𝑘 ↑ 𝑋)), ((0g‘𝐴) ∗ (𝑘 ↑ 𝑋))) = if(𝑘 = 0, (𝑘 ↑ 𝑋), (0g‘𝑄))) |
50 | 23, 49 | syl5eq 2656 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑘 ∈ ℕ0)
→ (if(𝑘 = 0,
(1r‘𝐴),
(0g‘𝐴))
∗
(𝑘 ↑ 𝑋)) = if(𝑘 = 0, (𝑘 ↑ 𝑋), (0g‘𝑄))) |
51 | 50 | mpteq2dva 4672 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑘 ∈ ℕ0
↦ (if(𝑘 = 0,
(1r‘𝐴),
(0g‘𝐴))
∗
(𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, (𝑘 ↑ 𝑋), (0g‘𝑄)))) |
52 | 51 | oveq2d 6565 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, (1r‘𝐴), (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋)))) = (𝑄 Σg (𝑘 ∈ ℕ0
↦ if(𝑘 = 0, (𝑘 ↑ 𝑋), (0g‘𝑄))))) |
53 | 12 | ply1ring 19439 |
. . . . 5
⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring) |
54 | | ringmnd 18379 |
. . . . 5
⊢ (𝑄 ∈ Ring → 𝑄 ∈ Mnd) |
55 | 24, 53, 54 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Mnd) |
56 | | nn0ex 11175 |
. . . . 5
⊢
ℕ0 ∈ V |
57 | 56 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
ℕ0 ∈ V) |
58 | | 0nn0 11184 |
. . . . 5
⊢ 0 ∈
ℕ0 |
59 | 58 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 ∈
ℕ0) |
60 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 = 0, (𝑘 ↑ 𝑋), (0g‘𝑄))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, (𝑘 ↑ 𝑋), (0g‘𝑄))) |
61 | 36 | ralrimiva 2949 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑘 ∈
ℕ0 (𝑘
↑
𝑋) ∈ (Base‘𝑄)) |
62 | 45, 55, 57, 59, 60, 61 | gsummpt1n0 18187 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ if(𝑘 = 0, (𝑘 ↑ 𝑋), (0g‘𝑄)))) = ⦋0 / 𝑘⦌(𝑘 ↑ 𝑋)) |
63 | | c0ex 9913 |
. . . . 5
⊢ 0 ∈
V |
64 | | csbov1g 6588 |
. . . . 5
⊢ (0 ∈
V → ⦋0 / 𝑘⦌(𝑘 ↑ 𝑋) = (⦋0 / 𝑘⦌𝑘 ↑ 𝑋)) |
65 | 63, 64 | mp1i 13 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
⦋0 / 𝑘⦌(𝑘 ↑ 𝑋) = (⦋0 / 𝑘⦌𝑘 ↑ 𝑋)) |
66 | | csbvarg 3955 |
. . . . . 6
⊢ (0 ∈
V → ⦋0 / 𝑘⦌𝑘 = 0) |
67 | 63, 66 | mp1i 13 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
⦋0 / 𝑘⦌𝑘 = 0) |
68 | 67 | oveq1d 6564 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(⦋0 / 𝑘⦌𝑘 ↑ 𝑋) = (0 ↑ 𝑋)) |
69 | 12, 10, 33, 9 | ply1idvr1 19484 |
. . . . 5
⊢ (𝐴 ∈ Ring → (0 ↑ 𝑋) = (1r‘𝑄)) |
70 | 24, 69 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0 ↑ 𝑋) = (1r‘𝑄)) |
71 | 65, 68, 70 | 3eqtrd 2648 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
⦋0 / 𝑘⦌(𝑘 ↑ 𝑋) = (1r‘𝑄)) |
72 | 52, 62, 71 | 3eqtrd 2648 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑄 Σg
(𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, (1r‘𝐴), (0g‘𝐴)) ∗ (𝑘 ↑ 𝑋)))) = (1r‘𝑄)) |
73 | 15, 22, 72 | 3eqtrd 2648 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(1r‘𝐶)) = (1r‘𝑄)) |