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 𝑠 T
resspsr.u U = I mPwSer H
resspsr.b B = Base U
resspsr.p P = S 𝑠 B
resspsr.2 φ T SubRing R
Assertion resspsrbas φ B = Base P

Proof

Step Hyp Ref Expression
1 resspsr.s S = I mPwSer R
2 resspsr.h H = R 𝑠 T
3 resspsr.u U = I mPwSer H
4 resspsr.b B = Base U
5 resspsr.p P = S 𝑠 B
6 resspsr.2 φ T SubRing R
7 fvex Base R V
8 2 subrgbas T SubRing R T = Base H
9 6 8 syl φ T = Base H
10 eqid Base R = Base R
11 10 subrgss T SubRing R T Base R
12 6 11 syl φ T Base R
13 9 12 eqsstrrd φ Base H Base R
14 13 adantr φ I V Base H Base R
15 mapss Base R V Base H Base R Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
16 7 14 15 sylancr φ I V Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
17 eqid Base H = Base H
18 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
19 simpr φ I V I V
20 3 17 18 4 19 psrbas φ I V B = Base H f 0 I | f -1 Fin
21 eqid Base S = Base S
22 1 10 18 21 19 psrbas φ I V Base S = Base R f 0 I | f -1 Fin
23 16 20 22 3sstr4d φ I V B Base S
24 reldmpsr Rel dom mPwSer
25 24 ovprc1 ¬ I V I mPwSer H =
26 3 25 syl5eq ¬ I V U =
27 26 adantl φ ¬ I V U =
28 27 fveq2d φ ¬ I V Base U = Base
29 base0 = Base
30 28 4 29 3eqtr4g φ ¬ I V B =
31 0ss Base S
32 30 31 eqsstrdi φ ¬ I V B Base S
33 23 32 pm2.61dan φ B Base S
34 5 21 ressbas2 B Base S B = Base P
35 33 34 syl φ B = Base P