Theorem psr0lid

Description: The zero element of the ring of power series is a left identity. (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 )
	psr0lid.p	|- .+ = ( +g ` S )
	psr0lid.x	|- ( ph -> X e. B )
Assertion	psr0lid	|- ( ph -> ( ( D X. { .0. } ) .+ X ) = X )

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		psr0lid.p	|- .+ = ( +g ` S )
8		psr0lid.x	|- ( ph -> X e. B )
9		eqid	|- ( +g ` R ) = ( +g ` R )
10	1 2 3 4 5 6	psr0cl	|- ( ph -> ( D X. { .0. } ) e. B )
11	1 6 9 7 10 8	psradd	|- ( ph -> ( ( D X. { .0. } ) .+ X ) = ( ( D X. { .0. } ) oF ( +g ` R ) X ) )
12		ovex	|- ( NN0 ^m I ) e. _V
13	4 12	rabex2	|- D e. _V
14	13	a1i	|- ( ph -> D e. _V )
15		eqid	|- ( Base ` R ) = ( Base ` R )
16	1 15 4 6 8	psrelbas	|- ( ph -> X : D --> ( Base ` R ) )
17	5	fvexi	|- .0. e. _V
18	17	a1i	|- ( ph -> .0. e. _V )
19	15 9 5	grplid	|- ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( .0. ( +g ` R ) x ) = x )
20	3 19	sylan	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( .0. ( +g ` R ) x ) = x )
21	14 16 18 20	caofid0l	|- ( ph -> ( ( D X. { .0. } ) oF ( +g ` R ) X ) = X )
22	11 21	eqtrd	|- ( ph -> ( ( D X. { .0. } ) .+ X ) = X )