| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdvsca.s |  |-  S = ( I mPwSer R ) | 
						
							| 2 |  | psdvsca.b |  |-  B = ( Base ` S ) | 
						
							| 3 |  | psdvsca.m |  |-  .x. = ( .s ` S ) | 
						
							| 4 |  | psdvsca.k |  |-  K = ( Base ` R ) | 
						
							| 5 |  | psdvsca.r |  |-  ( ph -> R e. CRing ) | 
						
							| 6 |  | psdvsca.x |  |-  ( ph -> X e. I ) | 
						
							| 7 |  | psdvsca.f |  |-  ( ph -> F e. B ) | 
						
							| 8 |  | psdvsca.c |  |-  ( ph -> C e. K ) | 
						
							| 9 |  | eqid |  |-  ( Base ` R ) = ( Base ` R ) | 
						
							| 10 |  | eqid |  |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | 
						
							| 11 | 5 | crngringd |  |-  ( ph -> R e. Ring ) | 
						
							| 12 |  | ringmgm |  |-  ( R e. Ring -> R e. Mgm ) | 
						
							| 13 | 11 12 | syl |  |-  ( ph -> R e. Mgm ) | 
						
							| 14 | 1 3 4 2 11 8 7 | psrvscacl |  |-  ( ph -> ( C .x. F ) e. B ) | 
						
							| 15 | 1 2 13 6 14 | psdcl |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) e. B ) | 
						
							| 16 | 1 9 10 2 15 | psrelbas |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) ) | 
						
							| 17 | 16 | ffnd |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 18 | 1 2 13 6 7 | psdcl |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B ) | 
						
							| 19 | 1 3 4 2 11 8 18 | psrvscacl |  |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) e. B ) | 
						
							| 20 | 1 9 10 2 19 | psrelbas |  |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) ) | 
						
							| 21 | 20 | ffnd |  |-  ( ph -> ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 22 | 11 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Ring ) | 
						
							| 23 | 10 | psrbagf |  |-  ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 ) | 
						
							| 24 | 23 | adantl |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 ) | 
						
							| 25 | 6 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I ) | 
						
							| 26 | 24 25 | ffvelcdmd |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d ` X ) e. NN0 ) | 
						
							| 27 |  | peano2nn0 |  |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. NN0 ) | 
						
							| 28 | 27 | nn0zd |  |-  ( ( d ` X ) e. NN0 -> ( ( d ` X ) + 1 ) e. ZZ ) | 
						
							| 29 | 26 28 | syl |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d ` X ) + 1 ) e. ZZ ) | 
						
							| 30 | 8 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> C e. K ) | 
						
							| 31 | 1 4 10 2 7 | psrelbas |  |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K ) | 
						
							| 32 | 31 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K ) | 
						
							| 33 |  | simpr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 34 |  | reldmpsr |  |-  Rel dom mPwSer | 
						
							| 35 | 1 2 34 | strov2rcl |  |-  ( F e. B -> I e. _V ) | 
						
							| 36 | 7 35 | syl |  |-  ( ph -> I e. _V ) | 
						
							| 37 | 10 | psrbagsn |  |-  ( I e. _V -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 38 | 36 37 | syl |  |-  ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) | 
						
							| 39 | 38 | 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 } ) | 
						
							| 40 | 10 | 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 } ) | 
						
							| 41 | 33 39 40 | 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 } ) | 
						
							| 42 | 32 41 | 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. K ) | 
						
							| 43 |  | eqid |  |-  ( .g ` R ) = ( .g ` R ) | 
						
							| 44 |  | eqid |  |-  ( .r ` R ) = ( .r ` R ) | 
						
							| 45 | 4 43 44 | mulgass3 |  |-  ( ( R e. Ring /\ ( ( ( d ` X ) + 1 ) e. ZZ /\ C e. K /\ ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) e. K ) ) -> ( C ( .r ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) | 
						
							| 46 | 22 29 30 42 45 | syl13anc |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( C ( .r ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) | 
						
							| 47 | 7 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F e. B ) | 
						
							| 48 | 1 2 10 25 47 33 | psdcoef |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) | 
						
							| 49 | 48 | oveq2d |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( C ( .r ` R ) ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) ) = ( C ( .r ` R ) ( ( ( d ` X ) + 1 ) ( .g ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) | 
						
							| 50 | 1 3 4 2 44 10 30 47 41 | psrvscaval |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) | 
						
							| 51 | 50 | oveq2d |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( C ( .r ` R ) ( F ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) | 
						
							| 52 | 46 49 51 | 3eqtr4rd |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( C ( .r ` R ) ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) ) ) | 
						
							| 53 | 14 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( C .x. F ) e. B ) | 
						
							| 54 | 1 2 10 25 53 33 | psdcoef |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) ` d ) = ( ( ( d ` X ) + 1 ) ( .g ` R ) ( ( C .x. F ) ` ( d oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) | 
						
							| 55 | 18 | adantr |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B ) | 
						
							| 56 | 1 3 4 2 44 10 30 55 33 | psrvscaval |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) ` d ) = ( C ( .r ` R ) ( ( ( ( I mPSDer R ) ` X ) ` F ) ` d ) ) ) | 
						
							| 57 | 52 54 56 | 3eqtr4d |  |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) ` d ) = ( ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) ` d ) ) | 
						
							| 58 | 17 21 57 | eqfnfvd |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C .x. F ) ) = ( C .x. ( ( ( I mPSDer R ) ` X ) ` F ) ) ) |