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