Step | Hyp | Ref
| Expression |
1 | | eqid 2728 |
. . 3
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
2 | | eqid 2728 |
. . 3
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
3 | | psdmplcl.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
4 | | psdmplcl.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Mnd) |
5 | | mndmgm 18708 |
. . . 4
⊢ (𝑅 ∈ Mnd → 𝑅 ∈ Mgm) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ Mgm) |
7 | | psdmplcl.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐼) |
8 | | psdmplcl.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
9 | | psdmplcl.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑃) |
10 | 8, 1, 9, 2 | mplbasss 21946 |
. . . 4
⊢ 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅)) |
11 | | psdmplcl.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
12 | 10, 11 | sselid 3980 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐼 mPwSer 𝑅))) |
13 | 1, 2, 3, 6, 7, 12 | psdcl 22092 |
. 2
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ (Base‘(𝐼 mPwSer 𝑅))) |
14 | | eqid 2728 |
. . . 4
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
15 | 1, 2, 14, 3, 6, 7,
12 | psdval 22090 |
. . 3
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
16 | | ovex 7459 |
. . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V |
17 | 16 | rabex 5338 |
. . . . . 6
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V |
18 | 17 | a1i 11 |
. . . . 5
⊢ (𝜑 → {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V) |
19 | 18 | mptexd 7242 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) ∈ V) |
20 | | fvexd 6917 |
. . . 4
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
21 | | funmpt 6596 |
. . . . 5
⊢ Fun
(𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
22 | 21 | a1i 11 |
. . . 4
⊢ (𝜑 → Fun (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
23 | | simpr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
24 | 14 | psrbagsn 22014 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ 𝑉 → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
25 | 3, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
26 | 25 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
27 | 14 | psrbagaddcl 21868 |
. . . . . . . . 9
⊢ ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
28 | 23, 26, 27 | syl2anc 582 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
29 | | eqidd 2729 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) |
30 | | eqid 2728 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
31 | 8, 30, 9, 14, 11 | mplelf 21947 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
32 | 31 | feqmptd 6972 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑧 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘𝑧))) |
33 | | fveq2 6902 |
. . . . . . . 8
⊢ (𝑧 = (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) → (𝐹‘𝑧) = (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) |
34 | 28, 29, 32, 33 | fmptco 7144 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
35 | | eqid 2728 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
36 | 8, 9, 35, 11, 4 | mplelsfi 21944 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 finSupp (0g‘𝑅)) |
37 | 28 | fmpttd 7130 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
38 | | ovex 7459 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ V |
39 | | eqid 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
40 | 38, 39 | fnmpti 6703 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
42 | | dffn3 6740 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↔ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶ran
(𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) |
43 | 41, 42 | sylib 217 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶ran
(𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) |
44 | 43, 37 | fcod 6754 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶ran
(𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) |
45 | 44 | ffnd 6728 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
46 | | fnresi 6689 |
. . . . . . . . . . 11
⊢ ( I
↾ {ℎ ∈
(ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ( I ↾ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
48 | 14 | psrbagf 21858 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑑:𝐼⟶ℕ0) |
49 | 48 | adantl 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑:𝐼⟶ℕ0) |
50 | 49 | ffvelcdmda 7099 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (𝑑‘𝑖) ∈
ℕ0) |
51 | 50 | nn0cnd 12572 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (𝑑‘𝑖) ∈ ℂ) |
52 | | ax-1cn 11204 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
53 | | 0cn 11244 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℂ |
54 | 52, 53 | ifcli 4579 |
. . . . . . . . . . . . . . 15
⊢ if(𝑖 = 𝑋, 1, 0) ∈ ℂ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → if(𝑖 = 𝑋, 1, 0) ∈ ℂ) |
56 | 51, 55 | pncand 11610 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0)) − if(𝑖 = 𝑋, 1, 0)) = (𝑑‘𝑖)) |
57 | 56 | mpteq2dva 5252 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑖 ∈ 𝐼 ↦ (((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0)) − if(𝑖 = 𝑋, 1, 0))) = (𝑖 ∈ 𝐼 ↦ (𝑑‘𝑖))) |
58 | | simpr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
59 | 25 | adantr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
60 | 14 | psrbagaddcl 21868 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
61 | 58, 59, 60 | syl2anc 582 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
62 | 14 | psrbagf 21858 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))):𝐼⟶ℕ0) |
63 | 62 | ffnd 6728 |
. . . . . . . . . . . . . 14
⊢ ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) Fn 𝐼) |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) Fn 𝐼) |
65 | | 1ex 11248 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
V |
66 | | c0ex 11246 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
V |
67 | 65, 66 | ifex 4582 |
. . . . . . . . . . . . . . 15
⊢ if(𝑦 = 𝑋, 1, 0) ∈ V |
68 | | eqid 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) |
69 | 67, 68 | fnmpti 6703 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) Fn 𝐼 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) Fn 𝐼) |
71 | 3 | adantr 479 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑉) |
72 | | inidm 4221 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
73 | 48 | ffnd 6728 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑑 Fn 𝐼) |
74 | 73 | adantl 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 Fn 𝐼) |
75 | | eqidd 2729 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (𝑑‘𝑖) = (𝑑‘𝑖)) |
76 | | eqeq1 2732 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑖 → (𝑦 = 𝑋 ↔ 𝑖 = 𝑋)) |
77 | 76 | ifbid 4555 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑖 → if(𝑦 = 𝑋, 1, 0) = if(𝑖 = 𝑋, 1, 0)) |
78 | | simpr 483 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) |
79 | 65, 66 | ifex 4582 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑖 = 𝑋, 1, 0) ∈ V |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → if(𝑖 = 𝑋, 1, 0) ∈ V) |
81 | 68, 77, 78, 80 | fvmptd3 7033 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))‘𝑖) = if(𝑖 = 𝑋, 1, 0)) |
82 | 74, 70, 71, 71, 72, 75, 81 | ofval 7702 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))‘𝑖) = ((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0))) |
83 | 64, 70, 71, 71, 72, 82, 81 | offval 7700 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = (𝑖 ∈ 𝐼 ↦ (((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0)) − if(𝑖 = 𝑋, 1, 0)))) |
84 | 49 | feqmptd 6972 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 = (𝑖 ∈ 𝐼 ↦ (𝑑‘𝑖))) |
85 | 57, 83, 84 | 3eqtr4d 2778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = 𝑑) |
86 | 28 | adantlr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
87 | 86 | fmpttd 7130 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
88 | 87, 58 | fvco3d 7003 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))‘𝑑) = ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘𝑑))) |
89 | | eqid 2728 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
90 | | oveq1 7433 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑑 → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
91 | | ovexd 7461 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ V) |
92 | 89, 90, 58, 91 | fvmptd3 7033 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘𝑑) = (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
93 | 92 | fveq2d 6906 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘𝑑)) = ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) |
94 | | oveq1 7433 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) → (𝑏 ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
95 | | ovexd 7461 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ V) |
96 | 39, 94, 61, 95 | fvmptd3 7033 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
97 | 88, 93, 96 | 3eqtrd 2772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))‘𝑑) = ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) |
98 | | fvresi 7188 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (( I
↾ {ℎ ∈
(ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})‘𝑑) = 𝑑) |
99 | 98 | adantl 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (( I
↾ {ℎ ∈
(ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})‘𝑑) = 𝑑) |
100 | 85, 97, 99 | 3eqtr4d 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))‘𝑑) = (( I ↾ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin})‘𝑑)) |
101 | 45, 47, 100 | eqfnfvd 7048 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = ( I ↾ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin})) |
102 | | fcof1 7302 |
. . . . . . . . 9
⊢ (((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = ( I ↾ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin})) → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}–1-1→{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
103 | 37, 101, 102 | syl2anc 582 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}–1-1→{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
104 | 36, 103, 20, 11 | fsuppco 9433 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) finSupp
(0g‘𝑅)) |
105 | 34, 104 | eqbrtrrd 5176 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) finSupp
(0g‘𝑅)) |
106 | 105 | fsuppimpd 9401 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅)) ∈ Fin) |
107 | | ssidd 4005 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅)) ⊆ ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅))) |
108 | | eqid 2728 |
. . . . . . . 8
⊢
(.g‘𝑅) = (.g‘𝑅) |
109 | 30, 108, 35 | mulgnn0z 19063 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝑛 ∈ ℕ0)
→ (𝑛(.g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
110 | 4, 109 | sylan 578 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑛(.g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
111 | 14 | psrbagf 21858 |
. . . . . . . . 9
⊢ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑘:𝐼⟶ℕ0) |
112 | 111 | adantl 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0) |
113 | 7 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑋 ∈ 𝐼) |
114 | 112, 113 | ffvelcdmd 7100 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘‘𝑋) ∈
ℕ0) |
115 | | peano2nn0 12550 |
. . . . . . 7
⊢ ((𝑘‘𝑋) ∈ ℕ0 → ((𝑘‘𝑋) + 1) ∈
ℕ0) |
116 | 114, 115 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑘‘𝑋) + 1) ∈
ℕ0) |
117 | | fvexd 6917 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ V) |
118 | 107, 110,
116, 117, 20 | suppssov2 8210 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) supp (0g‘𝑅)) ⊆ ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅))) |
119 | 106, 118 | ssfid 9298 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) supp (0g‘𝑅)) ∈ Fin) |
120 | 19, 20, 22, 119 | isfsuppd 9398 |
. . 3
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) finSupp
(0g‘𝑅)) |
121 | 15, 120 | eqbrtrd 5174 |
. 2
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) finSupp (0g‘𝑅)) |
122 | 8, 1, 2, 35, 9 | mplelbas 21940 |
. 2
⊢ ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵 ↔ ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) finSupp (0g‘𝑅))) |
123 | 13, 121, 122 | sylanbrc 581 |
1
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) |