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 ‘ 𝑃 ) )