Theorem psr0cl

Description: The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	psrgrp.s	|- S = ( I mPwSer R )
	psrgrp.i	|- ( ph -> I e. V )
	psrgrp.r	|- ( ph -> R e. Grp )
	psr0cl.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	psr0cl.o	|- .0. = ( 0g ` R )
	psr0cl.b	|- B = ( Base ` S )
Assertion	psr0cl	|- ( ph -> ( D X. { .0. } ) e. B )

Proof

Step	Hyp	Ref	Expression
1		psrgrp.s	|- S = ( I mPwSer R )
2		psrgrp.i	|- ( ph -> I e. V )
3		psrgrp.r	|- ( ph -> R e. Grp )
4		psr0cl.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5		psr0cl.o	|- .0. = ( 0g ` R )
6		psr0cl.b	|- B = ( Base ` S )
7		eqid	|- ( Base ` R ) = ( Base ` R )
8	7 5	grpidcl	|- ( R e. Grp -> .0. e. ( Base ` R ) )
9		fconst6g	|- ( .0. e. ( Base ` R ) -> ( D X. { .0. } ) : D --> ( Base ` R ) )
10	3 8 9	3syl	|- ( ph -> ( D X. { .0. } ) : D --> ( Base ` R ) )
11		fvex	|- ( Base ` R ) e. _V
12		ovex	|- ( NN0 ^m I ) e. _V
13	4 12	rabex2	|- D e. _V
14	11 13	elmap	|- ( ( D X. { .0. } ) e. ( ( Base ` R ) ^m D ) <-> ( D X. { .0. } ) : D --> ( Base ` R ) )
15	10 14	sylibr	|- ( ph -> ( D X. { .0. } ) e. ( ( Base ` R ) ^m D ) )
16	1 7 4 6 2	psrbas	|- ( ph -> B = ( ( Base ` R ) ^m D ) )
17	15 16	eleqtrrd	|- ( ph -> ( D X. { .0. } ) e. B )