Metamath Proof Explorer

Theorem resspsrmul

Description: A restricted power series algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses resspsr.s 
|- S = ( I mPwSer R )
resspsr.h 
|- H = ( R |`s T )
resspsr.u 
|- U = ( I mPwSer H )
resspsr.b 
|- B = ( Base ` U )
resspsr.p 
|- P = ( S |`s B )
resspsr.2 
|- ( ph -> T e. ( SubRing ` R ) )
Assertion resspsrmul 
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` P ) Y ) )

Proof

Step Hyp Ref Expression
1 resspsr.s 
 |-  S = ( I mPwSer R )
2 resspsr.h 
 |-  H = ( R |`s T )
3 resspsr.u 
 |-  U = ( I mPwSer H )
4 resspsr.b 
 |-  B = ( Base ` U )
5 resspsr.p 
 |-  P = ( S |`s B )
6 resspsr.2 
 |-  ( ph -> T e. ( SubRing ` R ) )
7 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
8 7 psrbaglefi 
 |-  ( 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 )
9 8 adantl 
 |-  ( ( ( 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 subrgsubg 
 |-  ( T e. ( SubRing ` R ) -> T e. ( SubGrp ` R ) )
11 6 10 syl 
 |-  ( ph -> T e. ( SubGrp ` R ) )
12 subgsubm 
 |-  ( T e. ( SubGrp ` R ) -> T e. ( SubMnd ` R ) )
13 11 12 syl 
 |-  ( ph -> T e. ( SubMnd ` R ) )
14 13 ad2antrr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> T e. ( SubMnd ` R ) )
15 6 ad3antrrr 
 |-  ( ( ( ( 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 ) )
16 eqid 
 |-  ( Base ` H ) = ( Base ` H )
17 simprl 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X e. B )
18 3 16 7 4 17 psrelbas 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) )
19 18 adantr 
 |-  ( ( ( 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 ) )
20 elrabi 
 |-  ( 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 } )
21 ffvelcdm 
 |-  ( ( 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 ) )
22 19 20 21 syl2an 
 |-  ( ( ( ( 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 ) )
23 2 subrgbas 
 |-  ( T e. ( SubRing ` R ) -> T = ( Base ` H ) )
24 15 23 syl 
 |-  ( ( ( ( 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 ) )
25 22 24 eleqtrrd 
 |-  ( ( ( ( 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 )
26 simprr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
27 3 16 7 4 26 psrelbas 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> Y : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) )
28 27 ad2antrr 
 |-  ( ( ( ( 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 ) )
29 ssrab2 
 |-  { y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | y oR <_ k } C_ { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
30 simplr 
 |-  ( ( ( ( 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 } )
31 simpr 
 |-  ( ( ( ( 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 } )
32 eqid 
 |-  { 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 }
33 7 32 psrbagconcl 
 |-  ( ( 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 } )
34 30 31 33 syl2anc 
 |-  ( ( ( ( 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 } )
35 29 34 sselid 
 |-  ( ( ( ( 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 } )
36 28 35 ffvelcdmd 
 |-  ( ( ( ( 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 ) )
37 36 24 eleqtrrd 
 |-  ( ( ( ( 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 )
38 eqid 
 |-  ( .r ` R ) = ( .r ` R )
39 38 subrgmcl 
 |-  ( ( T e. ( SubRing ` R ) /\ ( X ` x ) e. T /\ ( Y ` ( k oF - x ) ) e. T ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. T )
40 15 25 37 39 syl3anc 
 |-  ( ( ( ( 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 )
41 40 fmpttd 
 |-  ( ( ( 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 )
42 9 14 41 2 gsumsubm 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( 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 gsum ( x e. { y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) )
43 2 38 ressmulr 
 |-  ( T e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` H ) )
44 6 43 syl 
 |-  ( ph -> ( .r ` R ) = ( .r ` H ) )
45 44 ad3antrrr 
 |-  ( ( ( ( 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 ) )
46 45 oveqd 
 |-  ( ( ( ( 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 ) ) ) )
47 46 mpteq2dva 
 |-  ( ( ( 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 ) ) ) ) )
48 47 oveq2d 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( H gsum ( 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 gsum ( x e. { y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | y oR <_ k } |-> ( ( X ` x ) ( .r ` H ) ( Y ` ( k oF - x ) ) ) ) ) )
49 42 48 eqtrd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( 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 gsum ( x e. { y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | y oR <_ k } |-> ( ( X ` x ) ( .r ` H ) ( Y ` ( k oF - x ) ) ) ) ) )
50 49 mpteq2dva 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( 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 gsum ( x e. { y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | y oR <_ k } |-> ( ( X ` x ) ( .r ` H ) ( Y ` ( k oF - x ) ) ) ) ) ) )
51 eqid 
 |-  ( Base ` S ) = ( Base ` S )
52 eqid 
 |-  ( .r ` S ) = ( .r ` S )
53 fvex 
 |-  ( Base ` R ) e. _V
54 6 23 syl 
 |-  ( ph -> T = ( Base ` H ) )
55 eqid 
 |-  ( Base ` R ) = ( Base ` R )
56 55 subrgss 
 |-  ( T e. ( SubRing ` R ) -> T C_ ( Base ` R ) )
57 6 56 syl 
 |-  ( ph -> T C_ ( Base ` R ) )
58 54 57 eqsstrrd 
 |-  ( ph -> ( Base ` H ) C_ ( Base ` R ) )
59 mapss 
 |-  ( ( ( 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 } ) )
60 53 58 59 sylancr 
 |-  ( 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 } ) )
61 60 adantr 
 |-  ( ( 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 } ) )
62 reldmpsr 
 |-  Rel dom mPwSer
63 62 3 4 elbasov 
 |-  ( X e. B -> ( I e. _V /\ H e. _V ) )
64 63 ad2antrl 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( I e. _V /\ H e. _V ) )
65 64 simpld 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> I e. _V )
66 3 16 7 4 65 psrbas 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> B = ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
67 1 55 7 51 65 psrbas 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( Base ` S ) = ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
68 61 66 67 3sstr4d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> B C_ ( Base ` S ) )
69 68 17 sseldd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X e. ( Base ` S ) )
70 68 26 sseldd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> Y e. ( Base ` S ) )
71 1 51 38 52 7 69 70 psrmulfval 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` S ) Y ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) )
72 eqid 
 |-  ( .r ` H ) = ( .r ` H )
73 eqid 
 |-  ( .r ` U ) = ( .r ` U )
74 3 4 72 73 7 17 26 psrmulfval 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( H gsum ( x e. { y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | y oR <_ k } |-> ( ( X ` x ) ( .r ` H ) ( Y ` ( k oF - x ) ) ) ) ) ) )
75 50 71 74 3eqtr4rd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` S ) Y ) )
76 4 fvexi 
 |-  B e. _V
77 5 52 ressmulr 
 |-  ( B e. _V -> ( .r ` S ) = ( .r ` P ) )
78 76 77 mp1i 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( .r ` S ) = ( .r ` P ) )
79 78 oveqd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` S ) Y ) = ( X ( .r ` P ) Y ) )
80 75 79 eqtrd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` U ) Y ) = ( X ( .r ` P ) Y ) )