Step |
Hyp |
Ref |
Expression |
1 |
|
psdval.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
psdval.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
3 |
|
psdval.d |
⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
4 |
|
psdval.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
5 |
|
psdval.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝐵 ) |
6 |
|
psdcoef.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝐷 ) |
7 |
|
fveq1 |
⊢ ( 𝑘 = 𝐾 → ( 𝑘 ‘ 𝑋 ) = ( 𝐾 ‘ 𝑋 ) ) |
8 |
7
|
oveq1d |
⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 ‘ 𝑋 ) + 1 ) = ( ( 𝐾 ‘ 𝑋 ) + 1 ) ) |
9 |
|
fvoveq1 |
⊢ ( 𝑘 = 𝐾 → ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) |
10 |
8 9
|
oveq12d |
⊢ ( 𝑘 = 𝐾 → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) |
11 |
1 2 3 4 5
|
psdval |
⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) |
12 |
|
ovexd |
⊢ ( 𝜑 → ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ V ) |
13 |
10 11 6 12
|
fvmptd4 |
⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝐾 ) = ( ( ( 𝐾 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝐾 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) |