Metamath Proof Explorer

Theorem psdadd

Description: The derivative of a sum is the sum of the derivatives. (Contributed by SN, 12-Apr-2025)

Ref Expression
Hypotheses psdadd.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdadd.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psdadd.p ⊢ + = ( +g ‘ 𝑆 )
psdadd.r ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
psdadd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
psdadd.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
psdadd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion psdadd ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐹 + 𝐺 ) ) = ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) + ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 psdadd.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdadd.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psdadd.p ⊢ + = ( +g ‘ 𝑆 )
4 psdadd.r ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
5 psdadd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
6 psdadd.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 psdadd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
9 1 2 8 5 6 psdval ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
10 1 2 8 5 7 psdval ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) = ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
11 9 10 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∘f ( +g ‘ 𝑅 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) = ( ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) )
12 ovex ⊢ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ V
13 eqid ⊢ ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
14 12 13 fnmpti ⊢ ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
15 14 a1i ⊢ ( 𝜑 → ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
16 ovex ⊢ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ V
17 eqid ⊢ ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
18 16 17 fnmpti ⊢ ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
19 18 a1i ⊢ ( 𝜑 → ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
20 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
21 20 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
22 21 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
23 inidm ⊢ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∩ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
24 fveq1 ⊢ ( 𝑏 = 𝑑 → ( 𝑏 ‘ 𝑋 ) = ( 𝑑 ‘ 𝑋 ) )
25 24 oveq1d ⊢ ( 𝑏 = 𝑑 → ( ( 𝑏 ‘ 𝑋 ) + 1 ) = ( ( 𝑑 ‘ 𝑋 ) + 1 ) )
26 fvoveq1 ⊢ ( 𝑏 = 𝑑 → ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
27 25 26 oveq12d ⊢ ( 𝑏 = 𝑑 → ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
29 ovexd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ V )
30 13 27 28 29 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ‘ 𝑑 ) = ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
31 fvoveq1 ⊢ ( 𝑏 = 𝑑 → ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
32 25 31 oveq12d ⊢ ( 𝑏 = 𝑑 → ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
33 ovexd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ∈ V )
34 17 32 28 33 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ‘ 𝑑 ) = ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
35 15 19 22 22 23 30 34 offval ⊢ ( 𝜑 → ( ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑏 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) = ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) )
36 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
37 1 2 36 3 6 7 psradd ⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) = ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐹 + 𝐺 ) = ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) )
39 38 fveq1d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝐹 + 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
40 reldmpsr ⊢ Rel dom mPwSer
41 1 2 40 strov2rcl ⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V )
42 6 41 syl ⊢ ( 𝜑 → 𝐼 ∈ V )
43 8 psrbagsn ⊢ ( 𝐼 ∈ V → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
44 42 43 syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
46 8 psrbagaddcl ⊢ ( ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
47 28 45 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
48 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
49 1 48 8 2 6 psrelbas ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
50 49 ffnd ⊢ ( 𝜑 → 𝐹 Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
51 1 48 8 2 7 psrelbas ⊢ ( 𝜑 → 𝐺 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
52 51 ffnd ⊢ ( 𝜑 → 𝐺 Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
53 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
54 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
55 50 52 22 22 23 53 54 ofval ⊢ ( ( 𝜑 ∧ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
56 47 55 syldan ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
57 39 56 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝐹 + 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
58 57 oveq2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 + 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
59 4 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑅 ∈ CMnd )
60 8 psrbagf ⊢ ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑑 : 𝐼 ⟶ ℕ0 )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑑 : 𝐼 ⟶ ℕ0 )
62 5 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑋 ∈ 𝐼 )
63 61 62 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑑 ‘ 𝑋 ) ∈ ℕ0 )
64 peano2nn0 ⊢ ( ( 𝑑 ‘ 𝑋 ) ∈ ℕ0 → ( ( 𝑑 ‘ 𝑋 ) + 1 ) ∈ ℕ0 )
65 63 64 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑑 ‘ 𝑋 ) + 1 ) ∈ ℕ0 )
66 6 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐹 ∈ 𝐵 )
67 1 48 8 2 66 psrelbas ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
68 67 47 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
69 51 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝐺 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
70 69 47 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
71 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
72 48 71 36 mulgnn0di ⊢ ( ( 𝑅 ∈ CMnd ∧ ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ∈ ℕ0 ∧ ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
73 59 65 68 70 72 syl13anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
74 58 73 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 + 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
75 74 mpteq2dva ⊢ ( 𝜑 → ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) = ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 + 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
76 11 35 75 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∘f ( +g ‘ 𝑅 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) = ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 + 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
77 4 cmnmndd ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
78 mndmgm ⊢ ( 𝑅 ∈ Mnd → 𝑅 ∈ Mgm )
79 77 78 syl ⊢ ( 𝜑 → 𝑅 ∈ Mgm )
80 1 2 79 5 6 psdcl ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )
81 1 2 79 5 7 psdcl ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ∈ 𝐵 )
82 1 2 36 3 80 81 psradd ⊢ ( 𝜑 → ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) + ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) = ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∘f ( +g ‘ 𝑅 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) )
83 1 2 3 79 6 7 psraddcl ⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
84 1 2 8 5 83 psdval ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐹 + 𝐺 ) ) = ( 𝑑 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑑 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 + 𝐺 ) ‘ ( 𝑑 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
85 76 82 84 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐹 + 𝐺 ) ) = ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) + ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) )