Step | Hyp | Ref
| Expression |
1 | | mhpvscacl.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
2 | | mhpvscacl.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
3 | | mhpvscacl.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
4 | 3 | mpllmod 20231 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) |
5 | 1, 2, 4 | syl2anc 586 |
. . 3
⊢ (𝜑 → 𝑃 ∈ LMod) |
6 | | mhpvscacl.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐾) |
7 | | mhpvscacl.k |
. . . . 5
⊢ 𝐾 = (Base‘𝑅) |
8 | 6, 7 | eleqtrdi 2923 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑅)) |
9 | 3, 1, 2 | mplsca 20225 |
. . . . 5
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
10 | 9 | fveq2d 6674 |
. . . 4
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
11 | 8, 10 | eleqtrd 2915 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (Base‘(Scalar‘𝑃))) |
12 | | mhpvscacl.h |
. . . 4
⊢ 𝐻 = (𝐼 mHomP 𝑅) |
13 | | eqid 2821 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
14 | | mhpvscacl.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
15 | | mhpvscacl.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁)) |
16 | 12, 3, 13, 1, 2, 14, 15 | mhpmpl 20335 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (Base‘𝑃)) |
17 | | eqid 2821 |
. . . 4
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
18 | | mhpvscacl.t |
. . . 4
⊢ · = (
·𝑠 ‘𝑃) |
19 | | eqid 2821 |
. . . 4
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
20 | 13, 17, 18, 19 | lmodvscl 19651 |
. . 3
⊢ ((𝑃 ∈ LMod ∧ 𝑋 ∈
(Base‘(Scalar‘𝑃)) ∧ 𝐹 ∈ (Base‘𝑃)) → (𝑋 · 𝐹) ∈ (Base‘𝑃)) |
21 | 5, 11, 16, 20 | syl3anc 1367 |
. 2
⊢ (𝜑 → (𝑋 · 𝐹) ∈ (Base‘𝑃)) |
22 | | eqid 2821 |
. . . . 5
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
23 | 3, 7, 13, 22, 21 | mplelf 20213 |
. . . 4
⊢ (𝜑 → (𝑋 · 𝐹):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
24 | | eqid 2821 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
25 | 6 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → 𝑋 ∈ 𝐾) |
26 | 16 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → 𝐹 ∈ (Base‘𝑃)) |
27 | | eldifi 4103 |
. . . . . . 7
⊢ (𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅))) → 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
28 | 27 | adantl 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
29 | 3, 18, 7, 13, 24, 22, 25, 26, 28 | mplvscaval 20228 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → ((𝑋 · 𝐹)‘𝑘) = (𝑋(.r‘𝑅)(𝐹‘𝑘))) |
30 | 3, 7, 13, 22, 16 | mplelf 20213 |
. . . . . . 7
⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
31 | | ssidd 3990 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp (0g‘𝑅)) ⊆ (𝐹 supp (0g‘𝑅))) |
32 | | ovexd 7191 |
. . . . . . . 8
⊢ (𝜑 → (ℕ0
↑m 𝐼)
∈ V) |
33 | 22, 32 | rabexd 5236 |
. . . . . . 7
⊢ (𝜑 → {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V) |
34 | | fvexd 6685 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
35 | 30, 31, 33, 34 | suppssr 7861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → (𝐹‘𝑘) = (0g‘𝑅)) |
36 | 35 | oveq2d 7172 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → (𝑋(.r‘𝑅)(𝐹‘𝑘)) = (𝑋(.r‘𝑅)(0g‘𝑅))) |
37 | | eqid 2821 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
38 | 7, 24, 37 | ringrz 19338 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → (𝑋(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
39 | 2, 6, 38 | syl2anc 586 |
. . . . . 6
⊢ (𝜑 → (𝑋(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
40 | 39 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → (𝑋(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
41 | 29, 36, 40 | 3eqtrd 2860 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ (𝐹 supp (0g‘𝑅)))) → ((𝑋 · 𝐹)‘𝑘) = (0g‘𝑅)) |
42 | 23, 41 | suppss 7860 |
. . 3
⊢ (𝜑 → ((𝑋 · 𝐹) supp (0g‘𝑅)) ⊆ (𝐹 supp (0g‘𝑅))) |
43 | 12, 37, 22, 1, 2, 14, 15 | mhpdeg 20336 |
. . 3
⊢ (𝜑 → (𝐹 supp (0g‘𝑅)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
Σ𝑗 ∈
ℕ0 (𝑔‘𝑗) = 𝑁}) |
44 | 42, 43 | sstrd 3977 |
. 2
⊢ (𝜑 → ((𝑋 · 𝐹) supp (0g‘𝑅)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
Σ𝑗 ∈
ℕ0 (𝑔‘𝑗) = 𝑁}) |
45 | 12, 3, 13, 37, 22, 1, 2, 14 | ismhp 20334 |
. 2
⊢ (𝜑 → ((𝑋 · 𝐹) ∈ (𝐻‘𝑁) ↔ ((𝑋 · 𝐹) ∈ (Base‘𝑃) ∧ ((𝑋 · 𝐹) supp (0g‘𝑅)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
Σ𝑗 ∈
ℕ0 (𝑔‘𝑗) = 𝑁}))) |
46 | 21, 44, 45 | mpbir2and 711 |
1
⊢ (𝜑 → (𝑋 · 𝐹) ∈ (𝐻‘𝑁)) |