Metamath Proof Explorer


Theorem ressmplbas

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

Ref Expression
Hypotheses ressmpl.s 𝑆 = ( 𝐼 mPoly 𝑅 )
ressmpl.h 𝐻 = ( 𝑅s 𝑇 )
ressmpl.u 𝑈 = ( 𝐼 mPoly 𝐻 )
ressmpl.b 𝐵 = ( Base ‘ 𝑈 )
ressmpl.1 ( 𝜑𝐼𝑉 )
ressmpl.2 ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
ressmpl.p 𝑃 = ( 𝑆s 𝐵 )
Assertion ressmplbas ( 𝜑𝐵 = ( Base ‘ 𝑃 ) )

Proof

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