Theorem psr1bas

Description: The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	psr1val.1	|- S = ( PwSer1 ` R )
	psr1bas2.b	|- B = ( Base ` S )
	psr1bas.k	|- K = ( Base ` R )
Assertion	psr1bas	|- B = ( K ^m ( NN0 ^m 1o ) )

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	|- S = ( PwSer1 ` R )
2		psr1bas2.b	|- B = ( Base ` S )
3		psr1bas.k	|- K = ( Base ` R )
4		eqid	|- ( 1o mPwSer R ) = ( 1o mPwSer R )
5		psr1baslem	|- ( NN0 ^m 1o ) = { f e. ( NN0 ^m 1o ) | ( `' f " NN ) e. Fin }
6	1 2 4	psr1bas2	|- B = ( Base ` ( 1o mPwSer R ) )
7		1on	|- 1o e. On
8	7	a1i	|- ( T. -> 1o e. On )
9	4 3 5 6 8	psrbas	|- ( T. -> B = ( K ^m ( NN0 ^m 1o ) ) )
10	9	mptru	|- B = ( K ^m ( NN0 ^m 1o ) )