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 𝑆 = ( Poly1𝑅 )
ressply1.h 𝐻 = ( 𝑅s 𝑇 )
ressply1.u 𝑈 = ( Poly1𝐻 )
ressply1.b 𝐵 = ( Base ‘ 𝑈 )
ressply1.2 ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
ressply1.p 𝑃 = ( 𝑆s 𝐵 )
Assertion ressply1bas ( 𝜑𝐵 = ( Base ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ressply1.s 𝑆 = ( Poly1𝑅 )
2 ressply1.h 𝐻 = ( 𝑅s 𝑇 )
3 ressply1.u 𝑈 = ( Poly1𝐻 )
4 ressply1.b 𝐵 = ( Base ‘ 𝑈 )
5 ressply1.2 ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6 ressply1.p 𝑃 = ( 𝑆s 𝐵 )
7 eqid ( PwSer1𝐻 ) = ( PwSer1𝐻 )
8 eqid ( Base ‘ ( PwSer1𝐻 ) ) = ( Base ‘ ( PwSer1𝐻 ) )
9 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 1 2 3 4 5 7 8 9 ressply1bas2 ( 𝜑𝐵 = ( ( Base ‘ ( PwSer1𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) )
11 inss2 ( ( Base ‘ ( PwSer1𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) ⊆ ( Base ‘ 𝑆 )
12 10 11 eqsstrdi ( 𝜑𝐵 ⊆ ( Base ‘ 𝑆 ) )
13 6 9 ressbas2 ( 𝐵 ⊆ ( Base ‘ 𝑆 ) → 𝐵 = ( Base ‘ 𝑃 ) )
14 12 13 syl ( 𝜑𝐵 = ( Base ‘ 𝑃 ) )