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	$⊢ S = {Poly}_{1} (R)$
		ressply1.h	$⊢ H = R ↾_{𝑠} T$
		ressply1.u	$⊢ U = {Poly}_{1} (H)$
		ressply1.b	$⊢ B = {Base}_{U}$
		ressply1.2	$⊢ φ \to T \in SubRing (R)$
		ressply1bas2.w	$⊢ W = {PwSer}_{1} (H)$
		ressply1bas2.c	$⊢ C = {Base}_{W}$
		ressply1bas2.k	$⊢ K = {Base}_{S}$
	Assertion	ressply1bas2	$⊢ φ \to B = C \cap K$

Proof

Step	Hyp	Ref	Expression
1		ressply1.s	$⊢ S = {Poly}_{1} (R)$
2		ressply1.h	$⊢ H = R ↾_{𝑠} T$
3		ressply1.u	$⊢ U = {Poly}_{1} (H)$
4		ressply1.b	$⊢ B = {Base}_{U}$
5		ressply1.2	$⊢ φ \to T \in SubRing (R)$
6		ressply1bas2.w	$⊢ W = {PwSer}_{1} (H)$
7		ressply1bas2.c	$⊢ C = {Base}_{W}$
8		ressply1bas2.k	$⊢ K = {Base}_{S}$
9		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
10		eqid	$⊢ 1_{𝑜} mPoly H = 1_{𝑜} mPoly H$
11	3 4	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly H)}$
12		1on	$⊢ 1_{𝑜} \in On$
13	12	a1i	$⊢ φ \to 1_{𝑜} \in On$
14		eqid	$⊢ 1_{𝑜} mPwSer H = 1_{𝑜} mPwSer H$
15	6 7 14	psr1bas2	$⊢ C = {Base}_{(1_{𝑜} mPwSer H)}$
16	1 8	ply1bas	$⊢ K = {Base}_{(1_{𝑜} mPoly R)}$
17	9 2 10 11 13 5 14 15 16	ressmplbas2	$⊢ φ \to B = C \cap K$