MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resspsrmul Structured version   Unicode version

Theorem resspsrmul 17612
Description: A restricted power series algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015.)
Hypotheses
Ref Expression
resspsr.s  |-  S  =  ( I mPwSer  R )
resspsr.h  |-  H  =  ( Rs  T )
resspsr.u  |-  U  =  ( I mPwSer  H )
resspsr.b  |-  B  =  ( Base `  U
)
resspsr.p  |-  P  =  ( Ss  B )
resspsr.2  |-  ( ph  ->  T  e.  (SubRing `  R
) )
Assertion
Ref Expression
resspsrmul  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( X ( .r
`  U ) Y )  =  ( X ( .r `  P
) Y ) )

Proof of Theorem resspsrmul
Dummy variables  x  k  f  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldmpsr 17550 . . . . . . . . . 10  |-  Rel  dom mPwSer
2 resspsr.u . . . . . . . . . 10  |-  U  =  ( I mPwSer  H )
3 resspsr.b . . . . . . . . . 10  |-  B  =  ( Base `  U
)
41, 2, 3elbasov 14339 . . . . . . . . 9  |-  ( X  e.  B  ->  (
I  e.  _V  /\  H  e.  _V )
)
54ad2antrl 727 . . . . . . . 8  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( I  e.  _V  /\  H  e.  _V )
)
65simpld 459 . . . . . . 7  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  I  e.  _V )
7 eqid 2454 . . . . . . . 8  |-  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
87psrbaglefi 17563 . . . . . . 7  |-  ( ( I  e.  _V  /\  k  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin } )  ->  { y  e. 
{ f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }  |  y  oR  <_  k }  e.  Fin )
96, 8sylan 471 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  { y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }  |  y  oR  <_  k }  e.  Fin )
10 resspsr.2 . . . . . . . . 9  |-  ( ph  ->  T  e.  (SubRing `  R
) )
11 subrgsubg 16993 . . . . . . . . 9  |-  ( T  e.  (SubRing `  R
)  ->  T  e.  (SubGrp `  R ) )
1210, 11syl 16 . . . . . . . 8  |-  ( ph  ->  T  e.  (SubGrp `  R ) )
13 subgsubm 15821 . . . . . . . 8  |-  ( T  e.  (SubGrp `  R
)  ->  T  e.  (SubMnd `  R ) )
1412, 13syl 16 . . . . . . 7  |-  ( ph  ->  T  e.  (SubMnd `  R ) )
1514ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  T  e.  (SubMnd `  R ) )
1610ad3antrrr 729 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  T  e.  (SubRing `  R ) )
17 eqid 2454 . . . . . . . . . . . 12  |-  ( Base `  H )  =  (
Base `  H )
18 simprl 755 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  X  e.  B )
192, 17, 7, 3, 18psrelbas 17572 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  X : { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin } --> ( Base `  H ) )
2019adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  X : { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } --> ( Base `  H
) )
21 elrabi 3219 . . . . . . . . . 10  |-  ( x  e.  { y  e. 
{ f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }  |  y  oR  <_  k }  ->  x  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )
22 ffvelrn 5949 . . . . . . . . . 10  |-  ( ( X : { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin } --> ( Base `  H )  /\  x  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  ->  ( X `  x )  e.  ( Base `  H
) )
2320, 21, 22syl2an 477 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( X `  x )  e.  (
Base `  H )
)
24 resspsr.h . . . . . . . . . . 11  |-  H  =  ( Rs  T )
2524subrgbas 16996 . . . . . . . . . 10  |-  ( T  e.  (SubRing `  R
)  ->  T  =  ( Base `  H )
)
2616, 25syl 16 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  T  =  (
Base `  H )
)
2723, 26eleqtrrd 2545 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( X `  x )  e.  T
)
28 simprr 756 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  Y  e.  B )
292, 17, 7, 3, 28psrelbas 17572 . . . . . . . . . . 11  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  Y : { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin } --> ( Base `  H ) )
3029ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  Y : {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } --> ( Base `  H
) )
31 ssrab2 3544 . . . . . . . . . . 11  |-  { y  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  C_  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }
326ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  I  e.  _V )
33 simplr 754 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  k  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )
34 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k } )
35 eqid 2454 . . . . . . . . . . . . 13  |-  { y  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  =  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }
367, 35psrbagconcl 17565 . . . . . . . . . . . 12  |-  ( ( I  e.  _V  /\  k  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  /\  x  e.  { y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }  |  y  oR  <_  k } )  ->  ( k  oF  -  x
)  e.  { y  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k } )
3732, 33, 34, 36syl3anc 1219 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( k  oF  -  x )  e.  { y  e. 
{ f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }  |  y  oR  <_  k } )
3831, 37sseldi 3461 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( k  oF  -  x )  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin } )
3930, 38ffvelrnd 5952 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( Y `  ( k  oF  -  x ) )  e.  ( Base `  H
) )
4039, 26eleqtrrd 2545 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( Y `  ( k  oF  -  x ) )  e.  T )
41 eqid 2454 . . . . . . . . 9  |-  ( .r
`  R )  =  ( .r `  R
)
4241subrgmcl 16999 . . . . . . . 8  |-  ( ( T  e.  (SubRing `  R
)  /\  ( X `  x )  e.  T  /\  ( Y `  (
k  oF  -  x ) )  e.  T )  ->  (
( X `  x
) ( .r `  R ) ( Y `
 ( k  oF  -  x ) ) )  e.  T
)
4316, 27, 40, 42syl3anc 1219 . . . . . . 7  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( ( X `
 x ) ( .r `  R ) ( Y `  (
k  oF  -  x ) ) )  e.  T )
44 eqid 2454 . . . . . . 7  |-  ( x  e.  { y  e. 
{ f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }  |  y  oR  <_  k } 
|->  ( ( X `  x ) ( .r
`  R ) ( Y `  ( k  oF  -  x
) ) ) )  =  ( x  e. 
{ y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k }  |->  ( ( X `  x
) ( .r `  R ) ( Y `
 ( k  oF  -  x ) ) ) )
4543, 44fmptd 5975 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  ( x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k }  |->  ( ( X `  x
) ( .r `  R ) ( Y `
 ( k  oF  -  x ) ) ) ) : { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } --> T )
469, 15, 45, 24gsumsubm 15626 . . . . 5  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  ( R  gsumg  ( x  e.  { y  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  R
) ( Y `  ( k  oF  -  x ) ) ) ) )  =  ( H  gsumg  ( x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  R
) ( Y `  ( k  oF  -  x ) ) ) ) ) )
4724, 41ressmulr 14409 . . . . . . . . . 10  |-  ( T  e.  (SubRing `  R
)  ->  ( .r `  R )  =  ( .r `  H ) )
4810, 47syl 16 . . . . . . . . 9  |-  ( ph  ->  ( .r `  R
)  =  ( .r
`  H ) )
4948ad3antrrr 729 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( .r `  R )  =  ( .r `  H ) )
5049oveqd 6216 . . . . . . 7  |-  ( ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B
) )  /\  k  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  /\  x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k } )  ->  ( ( X `
 x ) ( .r `  R ) ( Y `  (
k  oF  -  x ) ) )  =  ( ( X `
 x ) ( .r `  H ) ( Y `  (
k  oF  -  x ) ) ) )
5150mpteq2dva 4485 . . . . . 6  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  ( x  e.  { y  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin }  |  y  oR  <_  k }  |->  ( ( X `  x
) ( .r `  R ) ( Y `
 ( k  oF  -  x ) ) ) )  =  ( x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  H
) ( Y `  ( k  oF  -  x ) ) ) ) )
5251oveq2d 6215 . . . . 5  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  ( H  gsumg  ( x  e.  { y  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  R
) ( Y `  ( k  oF  -  x ) ) ) ) )  =  ( H  gsumg  ( x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  H
) ( Y `  ( k  oF  -  x ) ) ) ) ) )
5346, 52eqtrd 2495 . . . 4  |-  ( ( ( ph  /\  ( X  e.  B  /\  Y  e.  B )
)  /\  k  e.  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } )  ->  ( R  gsumg  ( x  e.  { y  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  R
) ( Y `  ( k  oF  -  x ) ) ) ) )  =  ( H  gsumg  ( x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  H
) ( Y `  ( k  oF  -  x ) ) ) ) ) )
5453mpteq2dva 4485 . . 3  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( k  e.  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } 
|->  ( R  gsumg  ( x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  R
) ( Y `  ( k  oF  -  x ) ) ) ) ) )  =  ( k  e. 
{ f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }  |->  ( H 
gsumg  ( x  e.  { y  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  H
) ( Y `  ( k  oF  -  x ) ) ) ) ) ) )
55 resspsr.s . . . 4  |-  S  =  ( I mPwSer  R )
56 eqid 2454 . . . 4  |-  ( Base `  S )  =  (
Base `  S )
57 eqid 2454 . . . 4  |-  ( .r
`  S )  =  ( .r `  S
)
58 fvex 5808 . . . . . . . 8  |-  ( Base `  R )  e.  _V
5910, 25syl 16 . . . . . . . . 9  |-  ( ph  ->  T  =  ( Base `  H ) )
60 eqid 2454 . . . . . . . . . . 11  |-  ( Base `  R )  =  (
Base `  R )
6160subrgss 16988 . . . . . . . . . 10  |-  ( T  e.  (SubRing `  R
)  ->  T  C_  ( Base `  R ) )
6210, 61syl 16 . . . . . . . . 9  |-  ( ph  ->  T  C_  ( Base `  R ) )
6359, 62eqsstr3d 3498 . . . . . . . 8  |-  ( ph  ->  ( Base `  H
)  C_  ( Base `  R ) )
64 mapss 7364 . . . . . . . 8  |-  ( ( ( Base `  R
)  e.  _V  /\  ( Base `  H )  C_  ( Base `  R
) )  ->  (
( Base `  H )  ^m  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } )  C_  (
( Base `  R )  ^m  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin } ) )
6558, 63, 64sylancr 663 . . . . . . 7  |-  ( ph  ->  ( ( Base `  H
)  ^m  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin } ) 
C_  ( ( Base `  R )  ^m  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } ) )
6665adantr 465 . . . . . 6  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( ( Base `  H
)  ^m  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin } ) 
C_  ( ( Base `  R )  ^m  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } ) )
672, 17, 7, 3, 6psrbas 17570 . . . . . 6  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  B  =  ( ( Base `  H )  ^m  { f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } ) )
6855, 60, 7, 56, 6psrbas 17570 . . . . . 6  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( Base `  S )  =  ( ( Base `  R )  ^m  {
f  e.  ( NN0 
^m  I )  |  ( `' f " NN )  e.  Fin } ) )
6966, 67, 683sstr4d 3506 . . . . 5  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  B  C_  ( Base `  S
) )
7069, 18sseldd 3464 . . . 4  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  X  e.  ( Base `  S ) )
7169, 28sseldd 3464 . . . 4  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  Y  e.  ( Base `  S ) )
7255, 56, 41, 57, 7, 70, 71psrmulfval 17578 . . 3  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( X ( .r
`  S ) Y )  =  ( k  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  |->  ( R  gsumg  ( x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  R
) ( Y `  ( k  oF  -  x ) ) ) ) ) ) )
73 eqid 2454 . . . 4  |-  ( .r
`  H )  =  ( .r `  H
)
74 eqid 2454 . . . 4  |-  ( .r
`  U )  =  ( .r `  U
)
752, 3, 73, 74, 7, 18, 28psrmulfval 17578 . . 3  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( X ( .r
`  U ) Y )  =  ( k  e.  { f  e.  ( NN0  ^m  I
)  |  ( `' f " NN )  e.  Fin }  |->  ( H  gsumg  ( x  e.  {
y  e.  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  | 
y  oR  <_ 
k }  |->  ( ( X `  x ) ( .r `  H
) ( Y `  ( k  oF  -  x ) ) ) ) ) ) )
7654, 72, 753eqtr4rd 2506 . 2  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( X ( .r
`  U ) Y )  =  ( X ( .r `  S
) Y ) )
77 fvex 5808 . . . . 5  |-  ( Base `  U )  e.  _V
783, 77eqeltri 2538 . . . 4  |-  B  e. 
_V
79 resspsr.p . . . . 5  |-  P  =  ( Ss  B )
8079, 57ressmulr 14409 . . . 4  |-  ( B  e.  _V  ->  ( .r `  S )  =  ( .r `  P
) )
8178, 80mp1i 12 . . 3  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( .r `  S
)  =  ( .r
`  P ) )
8281oveqd 6216 . 2  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( X ( .r
`  S ) Y )  =  ( X ( .r `  P
) Y ) )
8376, 82eqtrd 2495 1  |-  ( (
ph  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( X ( .r
`  U ) Y )  =  ( X ( .r `  P
) Y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   {crab 2802   _Vcvv 3076    C_ wss 3435   class class class wbr 4399    |-> cmpt 4457   `'ccnv 4946   "cima 4950   -->wf 5521   ` cfv 5525  (class class class)co 6199    oFcof 6427    oRcofr 6428    ^m cmap 7323   Fincfn 7419    <_ cle 9529    - cmin 9705   NNcn 10432   NN0cn0 10689   Basecbs 14291   ↾s cress 14292   .rcmulr 14357    gsumg cgsu 14497  SubMndcsubmnd 15581  SubGrpcsubg 15793  SubRingcsubrg 16983   mPwSer cmps 17540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-of 6429  df-ofr 6430  df-om 6586  df-1st 6686  df-2nd 6687  df-supp 6800  df-recs 6941  df-rdg 6975  df-1o 7029  df-2o 7030  df-oadd 7033  df-er 7210  df-map 7325  df-pm 7326  df-ixp 7373  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-fsupp 7731  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-nn 10433  df-2 10490  df-3 10491  df-4 10492  df-5 10493  df-6 10494  df-7 10495  df-8 10496  df-9 10497  df-n0 10690  df-z 10757  df-uz 10972  df-fz 11554  df-seq 11923  df-struct 14293  df-ndx 14294  df-slot 14295  df-base 14296  df-sets 14297  df-ress 14298  df-plusg 14369  df-mulr 14370  df-sca 14372  df-vsca 14373  df-tset 14375  df-0g 14498  df-gsum 14499  df-mnd 15533  df-submnd 15583  df-grp 15663  df-minusg 15664  df-subg 15796  df-mgp 16713  df-rng 16769  df-subrg 16985  df-psr 17545
This theorem is referenced by:  subrgpsr  17614  ressmplmul  17660
  Copyright terms: Public domain W3C validator