Metamath Proof Explorer

Theorem psdffval

Description: Value of the power series differentiation operation. (Contributed by SN, 11-Apr-2025)

Ref Expression
Hypotheses psdffval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdffval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psdffval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psdffval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psdffval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion psdffval ( 𝜑 → ( 𝐼 mPSDer 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psdffval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdffval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psdffval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
4 psdffval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 psdffval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
6 df-psd ⊢ mPSDer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )
7 6 a1i ⊢ ( 𝜑 → mPSDer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) ) )
8 simpl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝑖 = 𝐼 )
9 oveq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPwSer 𝑟 ) = ( 𝐼 mPwSer 𝑅 ) )
10 9 1 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPwSer 𝑟 ) = 𝑆 )
11 10 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) = ( Base ‘ 𝑆 ) )
12 11 2 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) = 𝐵 )
13 8 oveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
14 13 rabeqdv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
15 14 3 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = 𝐷 )
16 fveq2 ⊢ ( 𝑟 = 𝑅 → ( .g ‘ 𝑟 ) = ( .g ‘ 𝑅 ) )
17 16 adantl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( .g ‘ 𝑟 ) = ( .g ‘ 𝑅 ) )
18 eqidd ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝑘 ‘ 𝑥 ) + 1 ) = ( ( 𝑘 ‘ 𝑥 ) + 1 ) )
19 8 mpteq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) )
20 19 oveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) = ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) )
21 20 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) = ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) )
22 17 18 21 oveq123d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) )
23 15 22 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) )
24 12 23 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) )
25 8 24 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPwSer 𝑟 ) ) ↦ ( 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )
27 4 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
28 5 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
29 4 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) ∈ V )
30 7 26 27 28 29 ovmpod ⊢ ( 𝜑 → ( 𝐼 mPSDer 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑥 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) ) ) ) ) ) )