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

Metamath Proof Explorer

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	⊢ 𝑆 = ( Poly₁ ‘ 𝑅 )
		ressply1.h	⊢ 𝐻 = ( 𝑅 ↾_s 𝑇 )
		ressply1.u	⊢ 𝑈 = ( Poly₁ ‘ 𝐻 )
		ressply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
		ressply1.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
		ressply1bas2.w	⊢ 𝑊 = ( PwSer₁ ‘ 𝐻 )
		ressply1bas2.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
		ressply1bas2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	Assertion	ressply1bas2	⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∩ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply1.s	⊢ 𝑆 = ( Poly₁ ‘ 𝑅 )
2		ressply1.h	⊢ 𝐻 = ( 𝑅 ↾_s 𝑇 )
3		ressply1.u	⊢ 𝑈 = ( Poly₁ ‘ 𝐻 )
4		ressply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressply1.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		ressply1bas2.w	⊢ 𝑊 = ( PwSer₁ ‘ 𝐻 )
7		ressply1bas2.c	⊢ 𝐶 = ( Base ‘ 𝑊 )
8		ressply1bas2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
9		eqid	⊢ ( 1_o mPoly 𝑅 ) = ( 1_o mPoly 𝑅 )
10		eqid	⊢ ( 1_o mPoly 𝐻 ) = ( 1_o mPoly 𝐻 )
11	3 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1_o mPoly 𝐻 ) )
12		1on	⊢ 1_o ∈ On
13	12	a1i	⊢ ( 𝜑 → 1_o ∈ On )
14		eqid	⊢ ( 1_o mPwSer 𝐻 ) = ( 1_o mPwSer 𝐻 )
15	6 7 14	psr1bas2	⊢ 𝐶 = ( Base ‘ ( 1_o mPwSer 𝐻 ) )
16	1 8	ply1bas	⊢ 𝐾 = ( Base ‘ ( 1_o mPoly 𝑅 ) )
17	9 2 10 11 13 5 14 15 16	ressmplbas2	⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∩ 𝐾 ) )