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 ) ) )