Metamath Proof Explorer

Theorem resspsrbas

Description: A restricted power series algebra has the same base set. (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 resspsrbas 
|- ( ph -> B = ( Base ` P ) )

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 fvex 
 |-  ( Base ` R ) e. _V
8 2 subrgbas 
 |-  ( T e. ( SubRing ` R ) -> T = ( Base ` H ) )
9 6 8 syl 
 |-  ( ph -> T = ( Base ` H ) )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 10 subrgss 
 |-  ( T e. ( SubRing ` R ) -> T C_ ( Base ` R ) )
12 6 11 syl 
 |-  ( ph -> T C_ ( Base ` R ) )
13 9 12 eqsstrrd 
 |-  ( ph -> ( Base ` H ) C_ ( Base ` R ) )
14 13 adantr 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` H ) C_ ( Base ` R ) )
15 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 } ) )
16 7 14 15 sylancr 
 |-  ( ( ph /\ I e. _V ) -> ( ( 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 } ) )
17 eqid 
 |-  ( Base ` H ) = ( Base ` H )
18 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
19 simpr 
 |-  ( ( ph /\ I e. _V ) -> I e. _V )
20 3 17 18 4 19 psrbas 
 |-  ( ( ph /\ I e. _V ) -> B = ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
21 eqid 
 |-  ( Base ` S ) = ( Base ` S )
22 1 10 18 21 19 psrbas 
 |-  ( ( ph /\ I e. _V ) -> ( Base ` S ) = ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
23 16 20 22 3sstr4d 
 |-  ( ( ph /\ I e. _V ) -> B C_ ( Base ` S ) )
24 reldmpsr 
 |-  Rel dom mPwSer
25 24 ovprc1 
 |-  ( -. I e. _V -> ( I mPwSer H ) = (/) )
26 3 25 syl5eq 
 |-  ( -. I e. _V -> U = (/) )
27 26 adantl 
 |-  ( ( ph /\ -. I e. _V ) -> U = (/) )
28 27 fveq2d 
 |-  ( ( ph /\ -. I e. _V ) -> ( Base ` U ) = ( Base ` (/) ) )
29 base0 
 |-  (/) = ( Base ` (/) )
30 28 4 29 3eqtr4g 
 |-  ( ( ph /\ -. I e. _V ) -> B = (/) )
31 0ss 
 |-  (/) C_ ( Base ` S )
32 30 31 eqsstrdi 
 |-  ( ( ph /\ -. I e. _V ) -> B C_ ( Base ` S ) )
33 23 32 pm2.61dan 
 |-  ( ph -> B C_ ( Base ` S ) )
34 5 21 ressbas2 
 |-  ( B C_ ( Base ` S ) -> B = ( Base ` P ) )
35 33 34 syl 
 |-  ( ph -> B = ( Base ` P ) )