| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdmplcl.p |  |-  P = ( I mPoly R ) | 
						
							| 2 |  | psdmplcl.b |  |-  B = ( Base ` P ) | 
						
							| 3 |  | psdmplcl.r |  |-  ( ph -> R e. Mnd ) | 
						
							| 4 |  | psdmplcl.x |  |-  ( ph -> X e. I ) | 
						
							| 5 |  | psdmplcl.f |  |-  ( ph -> F e. B ) | 
						
							| 6 |  | eqid |  |-  ( I mPwSer R ) = ( I mPwSer R ) | 
						
							| 7 |  | eqid |  |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) ) | 
						
							| 8 |  | mndmgm |  |-  ( R e. Mnd -> R e. Mgm ) | 
						
							| 9 | 3 8 | syl |  |-  ( ph -> R e. Mgm ) | 
						
							| 10 | 1 6 2 7 | mplbasss |  |-  B C_ ( Base ` ( I mPwSer R ) ) | 
						
							| 11 | 10 5 | sselid |  |-  ( ph -> F e. ( Base ` ( I mPwSer R ) ) ) | 
						
							| 12 | 6 7 9 4 11 | psdcl |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. ( Base ` ( I mPwSer R ) ) ) | 
						
							| 13 |  | eqid |  |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | 
						
							| 14 | 6 7 13 4 11 | psdval |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) | 
						
							| 15 |  | ovex |  |-  ( NN0 ^m I ) e. _V | 
						
							| 16 | 15 | rabex |  |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V | 
						
							| 17 | 16 | a1i |  |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V ) | 
						
							| 18 | 17 | mptexd |  |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) e. _V ) | 
						
							| 19 |  | fvexd |  |-  ( ph -> ( 0g ` R ) e. _V ) | 
						
							| 20 |  | funmpt |  |-  Fun ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) | 
						
							| 21 | 20 | a1i |  |-  ( ph -> Fun ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) | 
						
							| 22 |  | simpr |  |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 23 |  | reldmmpl |  |-  Rel dom mPoly | 
						
							| 24 | 1 2 23 | strov2rcl |  |-  ( F e. B -> I e. _V ) | 
						
							| 25 | 5 24 | syl |  |-  ( ph -> I e. _V ) | 
						
							| 26 | 13 | psrbagsn |  |-  ( I e. _V -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 27 | 25 26 | syl |  |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 28 | 27 | adantr |  |-  ( ( ph /\ k 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 } ) | 
						
							| 29 | 13 | psrbagaddcl |  |-  ( ( k 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 } ) -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 30 | 22 28 29 | syl2anc |  |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 31 |  | eqidd |  |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) | 
						
							| 32 |  | eqid |  |-  ( Base ` R ) = ( Base ` R ) | 
						
							| 33 | 1 32 2 13 5 | mplelf |  |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) ) | 
						
							| 34 | 33 | feqmptd |  |-  ( ph -> F = ( z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` z ) ) ) | 
						
							| 35 |  | fveq2 |  |-  ( z = ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) -> ( F ` z ) = ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) | 
						
							| 36 | 30 31 34 35 | fmptco |  |-  ( ph -> ( F o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) | 
						
							| 37 |  | eqid |  |-  ( 0g ` R ) = ( 0g ` R ) | 
						
							| 38 | 1 2 37 5 | mplelsfi |  |-  ( ph -> F finSupp ( 0g ` R ) ) | 
						
							| 39 | 30 | fmpttd |  |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 40 |  | ovex |  |-  ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. _V | 
						
							| 41 |  | eqid |  |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) | 
						
							| 42 | 40 41 | fnmpti |  |-  ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | 
						
							| 43 | 42 | a1i |  |-  ( ph -> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 44 |  | dffn3 |  |-  ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } <-> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ran ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) | 
						
							| 45 | 43 44 | sylib |  |-  ( ph -> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ran ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) | 
						
							| 46 | 45 39 | fcod |  |-  ( ph -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ran ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) | 
						
							| 47 | 46 | ffnd |  |-  ( ph -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 48 |  | fnresi |  |-  ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | 
						
							| 49 | 48 | a1i |  |-  ( ph -> ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 50 | 13 | psrbagf |  |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 ) | 
						
							| 51 | 50 | adantl |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 ) | 
						
							| 52 | 51 | ffvelcdmda |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( d ` i ) e. NN0 ) | 
						
							| 53 | 52 | nn0cnd |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( d ` i ) e. CC ) | 
						
							| 54 |  | ax-1cn |  |-  1 e. CC | 
						
							| 55 |  | 0cn |  |-  0 e. CC | 
						
							| 56 | 54 55 | ifcli |  |-  if ( i = X , 1 , 0 ) e. CC | 
						
							| 57 | 56 | a1i |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> if ( i = X , 1 , 0 ) e. CC ) | 
						
							| 58 | 53 57 | pncand |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( ( ( d ` i ) + if ( i = X , 1 , 0 ) ) - if ( i = X , 1 , 0 ) ) = ( d ` i ) ) | 
						
							| 59 | 58 | mpteq2dva |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( i e. I |-> ( ( ( d ` i ) + if ( i = X , 1 , 0 ) ) - if ( i = X , 1 , 0 ) ) ) = ( i e. I |-> ( d ` i ) ) ) | 
						
							| 60 |  | simpr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 61 | 27 | 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 } ) | 
						
							| 62 | 13 | 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 } ) | 
						
							| 63 | 60 61 62 | 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 } ) | 
						
							| 64 | 13 | psrbagf |  |-  ( ( d oF + ( 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 ) ) ) : I --> NN0 ) | 
						
							| 65 | 64 | ffnd |  |-  ( ( d oF + ( 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 ) ) ) Fn I ) | 
						
							| 66 | 63 65 | syl |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) Fn I ) | 
						
							| 67 |  | 1ex |  |-  1 e. _V | 
						
							| 68 |  | c0ex |  |-  0 e. _V | 
						
							| 69 | 67 68 | ifex |  |-  if ( y = X , 1 , 0 ) e. _V | 
						
							| 70 |  | eqid |  |-  ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) | 
						
							| 71 | 69 70 | fnmpti |  |-  ( y e. I |-> if ( y = X , 1 , 0 ) ) Fn I | 
						
							| 72 | 71 | a1i |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) Fn I ) | 
						
							| 73 | 25 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. _V ) | 
						
							| 74 |  | inidm |  |-  ( I i^i I ) = I | 
						
							| 75 | 50 | ffnd |  |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d Fn I ) | 
						
							| 76 | 75 | adantl |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d Fn I ) | 
						
							| 77 |  | eqidd |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( d ` i ) = ( d ` i ) ) | 
						
							| 78 |  | eqeq1 |  |-  ( y = i -> ( y = X <-> i = X ) ) | 
						
							| 79 | 78 | ifbid |  |-  ( y = i -> if ( y = X , 1 , 0 ) = if ( i = X , 1 , 0 ) ) | 
						
							| 80 |  | simpr |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> i e. I ) | 
						
							| 81 | 67 68 | ifex |  |-  if ( i = X , 1 , 0 ) e. _V | 
						
							| 82 | 81 | a1i |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> if ( i = X , 1 , 0 ) e. _V ) | 
						
							| 83 | 70 79 80 82 | fvmptd3 |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( ( y e. I |-> if ( y = X , 1 , 0 ) ) ` i ) = if ( i = X , 1 , 0 ) ) | 
						
							| 84 | 76 72 73 73 74 77 83 | ofval |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ` i ) = ( ( d ` i ) + if ( i = X , 1 , 0 ) ) ) | 
						
							| 85 | 66 72 73 73 74 84 83 | offval |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( i e. I |-> ( ( ( d ` i ) + if ( i = X , 1 , 0 ) ) - if ( i = X , 1 , 0 ) ) ) ) | 
						
							| 86 | 51 | feqmptd |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d = ( i e. I |-> ( d ` i ) ) ) | 
						
							| 87 | 59 85 86 | 3eqtr4d |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = d ) | 
						
							| 88 | 30 | adantlr |  |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 89 | 88 | fmpttd |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 90 | 89 60 | fvco3d |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ` d ) = ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` d ) ) ) | 
						
							| 91 |  | eqid |  |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) | 
						
							| 92 |  | oveq1 |  |-  ( k = d -> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) | 
						
							| 93 |  | ovexd |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. _V ) | 
						
							| 94 | 91 92 60 93 | fvmptd3 |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` d ) = ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) | 
						
							| 95 | 94 | fveq2d |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` d ) ) = ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) | 
						
							| 96 |  | oveq1 |  |-  ( b = ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) -> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) | 
						
							| 97 |  | ovexd |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) e. _V ) | 
						
							| 98 | 41 96 63 97 | 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 oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) | 
						
							| 99 | 90 95 98 | 3eqtrd |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ` d ) = ( ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) | 
						
							| 100 |  | fvresi |  |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> ( ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ` d ) = d ) | 
						
							| 101 | 100 | adantl |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ` d ) = d ) | 
						
							| 102 | 87 99 101 | 3eqtr4d |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ` d ) = ( ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ` d ) ) | 
						
							| 103 | 47 49 102 | eqfnfvd |  |-  ( ph -> ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ) | 
						
							| 104 |  | fcof1 |  |-  ( ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } /\ ( ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b oF - ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( _I |` { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ) -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -1-1-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 105 | 39 103 104 | syl2anc |  |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -1-1-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 106 | 38 105 19 5 | fsuppco |  |-  ( ph -> ( F o. ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) finSupp ( 0g ` R ) ) | 
						
							| 107 | 36 106 | eqbrtrrd |  |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) finSupp ( 0g ` R ) ) | 
						
							| 108 | 107 | fsuppimpd |  |-  ( ph -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) e. Fin ) | 
						
							| 109 |  | ssidd |  |-  ( ph -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) C_ ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) ) | 
						
							| 110 |  | eqid |  |-  ( .g ` R ) = ( .g ` R ) | 
						
							| 111 | 32 110 37 | mulgnn0z |  |-  ( ( R e. Mnd /\ n e. NN0 ) -> ( n ( .g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) | 
						
							| 112 | 3 111 | sylan |  |-  ( ( ph /\ n e. NN0 ) -> ( n ( .g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) | 
						
							| 113 | 13 | psrbagf |  |-  ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> k : I --> NN0 ) | 
						
							| 114 | 113 | adantl |  |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> k : I --> NN0 ) | 
						
							| 115 | 4 | adantr |  |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I ) | 
						
							| 116 | 114 115 | ffvelcdmd |  |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k ` X ) e. NN0 ) | 
						
							| 117 |  | peano2nn0 |  |-  ( ( k ` X ) e. NN0 -> ( ( k ` X ) + 1 ) e. NN0 ) | 
						
							| 118 | 116 117 | syl |  |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k ` X ) + 1 ) e. NN0 ) | 
						
							| 119 |  | fvexd |  |-  ( ( ph /\ k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. _V ) | 
						
							| 120 | 109 112 118 119 19 | suppssov2 |  |-  ( ph -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) supp ( 0g ` R ) ) C_ ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) supp ( 0g ` R ) ) ) | 
						
							| 121 | 108 120 | ssfid |  |-  ( ph -> ( ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) supp ( 0g ` R ) ) e. Fin ) | 
						
							| 122 | 18 19 21 121 | isfsuppd |  |-  ( ph -> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) finSupp ( 0g ` R ) ) | 
						
							| 123 | 14 122 | eqbrtrd |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) finSupp ( 0g ` R ) ) | 
						
							| 124 | 1 6 7 37 2 | mplelbas |  |-  ( ( ( ( I mPSDer R ) ` X ) ` F ) e. B <-> ( ( ( ( I mPSDer R ) ` X ) ` F ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( ( I mPSDer R ) ` X ) ` F ) finSupp ( 0g ` R ) ) ) | 
						
							| 125 | 12 123 124 | sylanbrc |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B ) |