Theorem ressply1bas2

Description: The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (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 ‘ 𝑅 ) )
	ressply1bas2.w	⊢ 𝑊 = ( PwSer1 ‘ 𝐻 )
	ressply1bas2.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
	ressply1bas2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion	ressply1bas2	⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∩ 𝐾 ) )

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		ressply1bas2.w	⊢ 𝑊 = ( PwSer1 ‘ 𝐻 )
7		ressply1bas2.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
8		ressply1bas2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
9		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
10		eqid	⊢ ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
11	3 6 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
12		1on	⊢ 1o ∈ On
13	12	a1i	⊢ ( 𝜑 → 1o ∈ On )
14		eqid	⊢ ( 1o mPwSer 𝐻 ) = ( 1o mPwSer 𝐻 )
15	6 7 14	psr1bas2	⊢ 𝐶 = ( Base ‘ ( 1o mPwSer 𝐻 ) )
16		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
17	1 16 8	ply1bas	⊢ 𝐾 = ( Base ‘ ( 1o mPoly 𝑅 ) )
18	9 2 10 11 13 5 14 15 17	ressmplbas2	⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∩ 𝐾 ) )