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 ) )