| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . 3
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) | 
| 2 |  | eqid 2737 | . . 3
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) | 
| 3 |  | psdmplcl.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ Mnd) | 
| 4 |  | mndmgm 18754 | . . . 4
⊢ (𝑅 ∈ Mnd → 𝑅 ∈ Mgm) | 
| 5 | 3, 4 | syl 17 | . . 3
⊢ (𝜑 → 𝑅 ∈ Mgm) | 
| 6 |  | psdmplcl.x | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝐼) | 
| 7 |  | psdmplcl.p | . . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 8 |  | psdmplcl.b | . . . . 5
⊢ 𝐵 = (Base‘𝑃) | 
| 9 | 7, 1, 8, 2 | mplbasss 22017 | . . . 4
⊢ 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅)) | 
| 10 |  | psdmplcl.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐵) | 
| 11 | 9, 10 | sselid 3981 | . . 3
⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐼 mPwSer 𝑅))) | 
| 12 | 1, 2, 5, 6, 11 | psdcl 22165 | . 2
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ (Base‘(𝐼 mPwSer 𝑅))) | 
| 13 |  | eqid 2737 | . . . 4
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 14 | 1, 2, 13, 6, 11 | psdval 22163 | . . 3
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 15 |  | ovex 7464 | . . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 16 | 15 | rabex 5339 | . . . . . 6
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V | 
| 17 | 16 | a1i 11 | . . . . 5
⊢ (𝜑 → {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V) | 
| 18 | 17 | mptexd 7244 | . . . 4
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) ∈ V) | 
| 19 |  | fvexd 6921 | . . . 4
⊢ (𝜑 → (0g‘𝑅) ∈ V) | 
| 20 |  | funmpt 6604 | . . . . 5
⊢ Fun
(𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 21 | 20 | a1i 11 | . . . 4
⊢ (𝜑 → Fun (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 22 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 23 |  | reldmmpl 22008 | . . . . . . . . . . . . 13
⊢ Rel dom
mPoly | 
| 24 | 7, 8, 23 | strov2rcl 17255 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) | 
| 25 | 10, 24 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ V) | 
| 26 | 13 | psrbagsn 22087 | . . . . . . . . . . 11
⊢ (𝐼 ∈ V → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 28 | 27 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 29 | 13 | psrbagaddcl 21944 | . . . . . . . . 9
⊢ ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 30 | 22, 28, 29 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 31 |  | eqidd 2738 | . . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 32 |  | eqid 2737 | . . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 33 | 7, 32, 8, 13, 10 | mplelf 22018 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 34 | 33 | feqmptd 6977 | . . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑧 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘𝑧))) | 
| 35 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑧 = (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) → (𝐹‘𝑧) = (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 36 | 30, 31, 34, 35 | fmptco 7149 | . . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 37 |  | eqid 2737 | . . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 38 | 7, 8, 37, 10 | mplelsfi 22015 | . . . . . . . 8
⊢ (𝜑 → 𝐹 finSupp (0g‘𝑅)) | 
| 39 | 30 | fmpttd 7135 | . . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 40 |  | ovex 7464 | . . . . . . . . . . . . . . 15
⊢ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ V | 
| 41 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) | 
| 42 | 40, 41 | fnmpti 6711 | . . . . . . . . . . . . . 14
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 43 | 42 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 44 |  | dffn3 6748 | . . . . . . . . . . . . 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))))) | 
| 45 | 43, 44 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶ran
(𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 46 | 45, 39 | fcod 6761 | . . . . . . . . . . 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))))) | 
| 47 | 46 | ffnd 6737 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 48 |  | fnresi 6697 | . . . . . . . . . . 11
⊢ ( I
↾ {ℎ ∈
(ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 49 | 48 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ( I ↾ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 50 | 13 | psrbagf 21938 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑑:𝐼⟶ℕ0) | 
| 51 | 50 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑:𝐼⟶ℕ0) | 
| 52 | 51 | ffvelcdmda 7104 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (𝑑‘𝑖) ∈
ℕ0) | 
| 53 | 52 | nn0cnd 12589 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (𝑑‘𝑖) ∈ ℂ) | 
| 54 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ | 
| 55 |  | 0cn 11253 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℂ | 
| 56 | 54, 55 | ifcli 4573 | . . . . . . . . . . . . . . 15
⊢ if(𝑖 = 𝑋, 1, 0) ∈ ℂ | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → if(𝑖 = 𝑋, 1, 0) ∈ ℂ) | 
| 58 | 53, 57 | pncand 11621 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0)) − if(𝑖 = 𝑋, 1, 0)) = (𝑑‘𝑖)) | 
| 59 | 58 | mpteq2dva 5242 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑖 ∈ 𝐼 ↦ (((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0)) − if(𝑖 = 𝑋, 1, 0))) = (𝑖 ∈ 𝐼 ↦ (𝑑‘𝑖))) | 
| 60 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 61 | 27 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 62 | 13 | psrbagaddcl 21944 | . . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 63 | 60, 61, 62 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 64 | 13 | psrbagf 21938 | . . . . . . . . . . . . . . 15
⊢ ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))):𝐼⟶ℕ0) | 
| 65 | 64 | ffnd 6737 | . . . . . . . . . . . . . 14
⊢ ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) Fn 𝐼) | 
| 66 | 63, 65 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) Fn 𝐼) | 
| 67 |  | 1ex 11257 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
V | 
| 68 |  | c0ex 11255 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
V | 
| 69 | 67, 68 | ifex 4576 | . . . . . . . . . . . . . . 15
⊢ if(𝑦 = 𝑋, 1, 0) ∈ V | 
| 70 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) | 
| 71 | 69, 70 | fnmpti 6711 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) Fn 𝐼 | 
| 72 | 71 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) Fn 𝐼) | 
| 73 | 25 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐼 ∈ V) | 
| 74 |  | inidm 4227 | . . . . . . . . . . . . 13
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 75 | 50 | ffnd 6737 | . . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑑 Fn 𝐼) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 Fn 𝐼) | 
| 77 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → (𝑑‘𝑖) = (𝑑‘𝑖)) | 
| 78 |  | eqeq1 2741 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑖 → (𝑦 = 𝑋 ↔ 𝑖 = 𝑋)) | 
| 79 | 78 | ifbid 4549 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑖 → if(𝑦 = 𝑋, 1, 0) = if(𝑖 = 𝑋, 1, 0)) | 
| 80 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) | 
| 81 | 67, 68 | ifex 4576 | . . . . . . . . . . . . . . . 16
⊢ if(𝑖 = 𝑋, 1, 0) ∈ V | 
| 82 | 81 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → if(𝑖 = 𝑋, 1, 0) ∈ V) | 
| 83 | 70, 79, 80, 82 | fvmptd3 7039 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))‘𝑖) = if(𝑖 = 𝑋, 1, 0)) | 
| 84 | 76, 72, 73, 73, 74, 77, 83 | ofval 7708 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑖 ∈ 𝐼) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))‘𝑖) = ((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0))) | 
| 85 | 66, 72, 73, 73, 74, 84, 83 | offval 7706 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = (𝑖 ∈ 𝐼 ↦ (((𝑑‘𝑖) + if(𝑖 = 𝑋, 1, 0)) − if(𝑖 = 𝑋, 1, 0)))) | 
| 86 | 51 | feqmptd 6977 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 = (𝑖 ∈ 𝐼 ↦ (𝑑‘𝑖))) | 
| 87 | 59, 85, 86 | 3eqtr4d 2787 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = 𝑑) | 
| 88 | 30 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 89 | 88 | fmpttd 7135 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 90 | 89, 60 | fvco3d 7009 | . . . . . . . . . . . 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))))‘𝑑))) | 
| 91 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) | 
| 92 |  | oveq1 7438 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑑 → (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) | 
| 93 |  | ovexd 7466 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ V) | 
| 94 | 91, 92, 60, 93 | fvmptd3 7039 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘𝑑) = (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) | 
| 95 | 94 | fveq2d 6910 | . . . . . . . . . . . 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))))) | 
| 96 |  | oveq1 7438 | . . . . . . . . . . . . 13
⊢ (𝑏 = (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) → (𝑏 ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) = ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) | 
| 97 |  | ovexd 7466 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ V) | 
| 98 | 41, 96, 63, 97 | fvmptd3 7039 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = ((𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∘f − (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) | 
| 99 | 90, 95, 98 | 3eqtrd 2781 | . . . . . . . . . . 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)))) | 
| 100 |  | fvresi 7193 | . . . . . . . . . . . 12
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (( I
↾ {ℎ ∈
(ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})‘𝑑) = 𝑑) | 
| 101 | 100 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (( I
↾ {ℎ ∈
(ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})‘𝑑) = 𝑑) | 
| 102 | 87, 99, 101 | 3eqtr4d 2787 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))‘𝑑) = (( I ↾ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin})‘𝑑)) | 
| 103 | 47, 49, 102 | eqfnfvd 7054 | . . . . . . . . 9
⊢ (𝜑 → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏 ∘f −
(𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = ( I ↾ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin})) | 
| 104 |  | fcof1 7307 | . . . . . . . . 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}) | 
| 105 | 39, 103, 104 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}–1-1→{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 106 | 38, 105, 19, 10 | fsuppco 9442 | . . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) finSupp
(0g‘𝑅)) | 
| 107 | 36, 106 | eqbrtrrd 5167 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) finSupp
(0g‘𝑅)) | 
| 108 | 107 | fsuppimpd 9409 | . . . . 5
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅)) ∈ Fin) | 
| 109 |  | ssidd 4007 | . . . . . 6
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅)) ⊆ ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅))) | 
| 110 |  | eqid 2737 | . . . . . . . 8
⊢
(.g‘𝑅) = (.g‘𝑅) | 
| 111 | 32, 110, 37 | mulgnn0z 19119 | . . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ 𝑛 ∈ ℕ0)
→ (𝑛(.g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) | 
| 112 | 3, 111 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑛(.g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) | 
| 113 | 13 | psrbagf 21938 | . . . . . . . . 9
⊢ (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑘:𝐼⟶ℕ0) | 
| 114 | 113 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0) | 
| 115 | 6 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑋 ∈ 𝐼) | 
| 116 | 114, 115 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑘‘𝑋) ∈
ℕ0) | 
| 117 |  | peano2nn0 12566 | . . . . . . 7
⊢ ((𝑘‘𝑋) ∈ ℕ0 → ((𝑘‘𝑋) + 1) ∈
ℕ0) | 
| 118 | 116, 117 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑘‘𝑋) + 1) ∈
ℕ0) | 
| 119 |  | fvexd 6921 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ V) | 
| 120 | 109, 112,
118, 119, 19 | suppssov2 8223 | . . . . 5
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) supp (0g‘𝑅)) ⊆ ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) supp (0g‘𝑅))) | 
| 121 | 108, 120 | ssfid 9301 | . . . 4
⊢ (𝜑 → ((𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) supp (0g‘𝑅)) ∈ Fin) | 
| 122 | 18, 19, 21, 121 | isfsuppd 9406 | . . 3
⊢ (𝜑 → (𝑘 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑘‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑘 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) finSupp
(0g‘𝑅)) | 
| 123 | 14, 122 | eqbrtrd 5165 | . 2
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) finSupp (0g‘𝑅)) | 
| 124 | 7, 1, 2, 37, 8 | mplelbas 22011 | . 2
⊢ ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵 ↔ ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) finSupp (0g‘𝑅))) | 
| 125 | 12, 123, 124 | sylanbrc 583 | 1
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) |