This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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