Metamath Proof Explorer


Theorem ressply1bas

Description: A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses ressply1.s S = Poly 1 R
ressply1.h H = R 𝑠 T
ressply1.u U = Poly 1 H
ressply1.b B = Base U
ressply1.2 φ T SubRing R
ressply1.p P = S 𝑠 B
Assertion ressply1bas φ B = Base P

Proof

Step Hyp Ref Expression
1 ressply1.s S = Poly 1 R
2 ressply1.h H = R 𝑠 T
3 ressply1.u U = Poly 1 H
4 ressply1.b B = Base U
5 ressply1.2 φ T SubRing R
6 ressply1.p P = S 𝑠 B
7 eqid PwSer 1 H = PwSer 1 H
8 eqid Base PwSer 1 H = Base PwSer 1 H
9 eqid Base S = Base S
10 1 2 3 4 5 7 8 9 ressply1bas2 φ B = Base PwSer 1 H Base S
11 inss2 Base PwSer 1 H Base S Base S
12 10 11 eqsstrdi φ B Base S
13 6 9 ressbas2 B Base S B = Base P
14 12 13 syl φ B = Base P