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.i 
|- ( ph -> I e. V )
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.i 
 |-  ( ph -> I e. V )
5 psdadd.r 
 |-  ( ph -> R e. CMnd )
6 psdadd.x 
 |-  ( ph -> X e. I )
7 psdadd.f 
 |-  ( ph -> F e. B )
8 psdadd.g 
 |-  ( ph -> G e. B )
9 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
10 1 2 9 4 5 6 7 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 ) ) ) ) ) ) )
11 1 2 9 4 5 6 8 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 ) ) ) ) ) ) )
12 10 11 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 ) ) ) ) ) ) ) )
13 ovex 
 |-  ( ( ( b ` X ) + 1 ) ( .g ` R ) ( F ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V
14 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 ) ) ) ) ) )
15 13 14 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 }
16 15 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 } )
17 ovex 
 |-  ( ( ( b ` X ) + 1 ) ( .g ` R ) ( G ` ( b oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) e. _V
18 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 ) ) ) ) ) )
19 17 18 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 }
20 19 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 } )
21 ovex 
 |-  ( NN0 ^m I ) e. _V
22 21 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
23 22 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
24 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 }
25 fveq1 
 |-  ( b = d -> ( b ` X ) = ( d ` X ) )
26 25 oveq1d 
 |-  ( b = d -> ( ( b ` X ) + 1 ) = ( ( d ` X ) + 1 ) )
27 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 ) ) ) ) )
28 26 27 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 ) ) ) ) ) )
29 simpr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
30 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 )
31 14 28 29 30 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 ) ) ) ) ) )
32 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 ) ) ) ) )
33 26 32 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 ) ) ) ) ) )
34 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 )
35 18 33 29 34 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 ) ) ) ) ) )
36 16 20 23 23 24 31 35 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 ) ) ) ) ) ) ) )
37 eqid 
 |-  ( +g ` R ) = ( +g ` R )
38 1 2 37 3 7 8 psradd 
 |-  ( ph -> ( F .+ G ) = ( F oF ( +g ` R ) G ) )
39 38 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F .+ G ) = ( F oF ( +g ` R ) G ) )
40 39 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 ) ) ) ) )
41 9 psrbagsn 
 |-  ( I e. V -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
42 4 41 syl 
 |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
43 42 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 } )
44 9 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 } )
45 29 43 44 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 } )
46 eqid 
 |-  ( Base ` R ) = ( Base ` R )
47 1 46 9 2 7 psrelbas 
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
48 47 ffnd 
 |-  ( ph -> F Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
49 1 46 9 2 8 psrelbas 
 |-  ( ph -> G : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
50 49 ffnd 
 |-  ( ph -> G Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
51 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 ) ) ) ) )
52 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 ) ) ) ) )
53 48 50 23 23 24 51 52 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 ) ) ) ) ) )
54 45 53 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 ) ) ) ) ) )
55 40 54 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 ) ) ) ) ) )
56 55 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 ) ) ) ) ) ) )
57 5 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. CMnd )
58 9 psrbagf 
 |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 )
59 58 adantl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 )
60 6 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
61 59 60 ffvelcdmd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d ` X ) e. NN0 )
62 peano2nn0 
 |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. NN0 )
63 61 62 syl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d ` X ) + 1 ) e. NN0 )
64 7 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F e. B )
65 1 46 9 2 64 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 ) )
66 65 45 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 ) )
67 49 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 ) )
68 67 45 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 ) )
69 eqid 
 |-  ( .g ` R ) = ( .g ` R )
70 46 69 37 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 ) ) ) ) ) ) )
71 57 63 66 68 70 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 ) ) ) ) ) ) )
72 56 71 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 ) ) ) ) ) )
73 72 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 ) ) ) ) ) ) )
74 12 36 73 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 ) ) ) ) ) ) )
75 5 cmnmndd 
 |-  ( ph -> R e. Mnd )
76 mndmgm 
 |-  ( R e. Mnd -> R e. Mgm )
77 75 76 syl 
 |-  ( ph -> R e. Mgm )
78 1 2 4 77 6 7 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )
79 1 2 4 77 6 8 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` G ) e. B )
80 1 2 37 3 78 79 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 ) ) )
81 1 2 3 77 7 8 psraddcl 
 |-  ( ph -> ( F .+ G ) e. B )
82 1 2 9 4 5 6 81 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 ) ) ) ) ) ) )
83 74 80 82 3eqtr4rd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( F .+ G ) ) = ( ( ( ( I mPSDer R ) ` X ) ` F ) .+ ( ( ( I mPSDer R ) ` X ) ` G ) ) )