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 
|- S = ( I mPwSer R )
psdadd.b 
|- B = ( Base ` S )
psdadd.p 
|- .+ = ( +g ` S )
psdadd.r 
|- ( ph -> R e. CMnd )
psdadd.x 
|- ( ph -> X e. I )
psdadd.f 
|- ( ph -> F e. B )
psdadd.g 
|- ( ph -> G e. B )
Assertion psdadd 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( F .+ G ) ) = ( ( ( ( I mPSDer R ) ` X ) ` F ) .+ ( ( ( I mPSDer R ) ` X ) ` G ) ) )

Proof

Step Hyp Ref Expression
1 psdadd.s 
 |-  S = ( I mPwSer R )
2 psdadd.b 
 |-  B = ( Base ` S )
3 psdadd.p 
 |-  .+ = ( +g ` S )
4 psdadd.r 
 |-  ( ph -> R e. CMnd )
5 psdadd.x 
 |-  ( ph -> X e. I )
6 psdadd.f 
 |-  ( ph -> F e. B )
7 psdadd.g 
 |-  ( ph -> G e. B )
8 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
9 1 2 8 5 6 psdval 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) = ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
10 1 2 8 5 7 psdval 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` G ) = ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
11 9 10 oveq12d 
 |-  ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` F ) oF ( +g ` R ) ( ( ( I mPSDer R ) ` X ) ` G ) ) = ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) oF ( +g ` R ) ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) )
12 ovex 
 |-  ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V
13 eqid 
 |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
14 12 13 fnmpti 
 |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
15 14 a1i 
 |-  ( ph -> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
16 ovex 
 |-  ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V
17 eqid 
 |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
18 16 17 fnmpti 
 |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
19 18 a1i 
 |-  ( ph -> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
20 ovex 
 |-  ( NN0 ^m I ) e. _V
21 20 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
22 21 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
23 inidm 
 |-  ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } i^i { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
24 fveq1 
 |-  ( b = d -> ( b ` X ) = ( d ` X ) )
25 24 oveq1d 
 |-  ( b = d -> ( ( b ` X ) + 1 ) = ( ( d ` X ) + 1 ) )
26 fvoveq1 
 |-  ( b = d -> ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
27 25 26 oveq12d 
 |-  ( b = d -> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
28 simpr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
29 ovexd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V )
30 13 27 28 29 fvmptd3 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ` d ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
31 fvoveq1 
 |-  ( b = d -> ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
32 25 31 oveq12d 
 |-  ( b = d -> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
33 ovexd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V )
34 17 32 28 33 fvmptd3 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ` d ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
35 15 19 22 22 23 30 34 offval 
 |-  ( ph -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) oF ( +g ` R ) ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ( +g ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) )
36 eqid 
 |-  ( +g ` R ) = ( +g ` R )
37 1 2 36 3 6 7 psradd 
 |-  ( ph -> ( F .+ G ) = ( F oF ( +g ` R ) G ) )
38 37 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F .+ G ) = ( F oF ( +g ` R ) G ) )
39 38 fveq1d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( F .+ G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( ( F oF ( +g ` R ) G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
40 reldmpsr 
 |-  Rel dom mPwSer
41 1 2 40 strov2rcl 
 |-  ( F e. B -> I e. _V )
42 6 41 syl 
 |-  ( ph -> I e. _V )
43 8 psrbagsn 
 |-  ( I e. _V -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
44 42 43 syl 
 |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
45 44 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
46 8 psrbagaddcl 
 |-  ( ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } /\ ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
47 28 45 46 syl2anc 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
48 eqid 
 |-  ( Base ` R ) = ( Base ` R )
49 1 48 8 2 6 psrelbas 
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
50 49 ffnd 
 |-  ( ph -> F Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
51 1 48 8 2 7 psrelbas 
 |-  ( ph -> G : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
52 51 ffnd 
 |-  ( ph -> G Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
53 eqidd 
 |-  ( ( ph /\ ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
54 eqidd 
 |-  ( ( ph /\ ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) )
55 50 52 22 22 23 53 54 ofval 
 |-  ( ( ph /\ ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( F oF ( +g ` R ) G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ( +g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
56 47 55 syldan 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( F oF ( +g ` R ) G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ( +g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
57 39 56 eqtrd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( F .+ G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ( +g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
58 57 oveq2d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F .+ G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ( +g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
59 4 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. CMnd )
60 8 psrbagf 
 |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 )
61 60 adantl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 )
62 5 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
63 61 62 ffvelcdmd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d ` X ) e. NN0 )
64 peano2nn0 
 |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. NN0 )
65 63 64 syl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d ` X ) + 1 ) e. NN0 )
66 6 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F e. B )
67 1 48 8 2 66 psrelbas 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
68 67 47 ffvelcdmd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. ( Base ` R ) )
69 51 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> G : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
70 69 47 ffvelcdmd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. ( Base ` R ) )
71 eqid 
 |-  ( .g ` R ) = ( .g ` R )
72 48 71 36 mulgnn0di 
 |-  ( ( R e. CMnd /\ ( ( ( d ` X ) + 1 ) e. NN0 /\ ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. ( Base ` R ) /\ ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. ( Base ` R ) ) ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ( +g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ( +g ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
73 59 65 68 70 72 syl13anc 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ( +g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ( +g ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
74 58 73 eqtr2d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ( +g ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F .+ G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) )
75 74 mpteq2dva 
 |-  ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ( +g ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( G ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F .+ G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
76 11 35 75 3eqtrd 
 |-  ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` F ) oF ( +g ` R ) ( ( ( I mPSDer R ) ` X ) ` G ) ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F .+ G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
77 4 cmnmndd 
 |-  ( ph -> R e. Mnd )
78 mndmgm 
 |-  ( R e. Mnd -> R e. Mgm )
79 77 78 syl 
 |-  ( ph -> R e. Mgm )
80 1 2 79 5 6 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )
81 1 2 79 5 7 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` G ) e. B )
82 1 2 36 3 80 81 psradd 
 |-  ( ph -> ( ( ( ( I mPSDer R ) ` X ) ` F ) .+ ( ( ( I mPSDer R ) ` X ) ` G ) ) = ( ( ( ( I mPSDer R ) ` X ) ` F ) oF ( +g ` R ) ( ( ( I mPSDer R ) ` X ) ` G ) ) )
83 1 2 3 79 6 7 psraddcl 
 |-  ( ph -> ( F .+ G ) e. B )
84 1 2 8 5 83 psdval 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( F .+ G ) ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( F .+ G ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) )
85 76 82 84 3eqtr4rd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( F .+ G ) ) = ( ( ( ( I mPSDer R ) ` X ) ` F ) .+ ( ( ( I mPSDer R ) ` X ) ` G ) ) )