Theorem psrneg

Description: The negative function 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 )
	psrneg.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	psrneg.i	|- N = ( invg ` R )
	psrneg.b	|- B = ( Base ` S )
	psrneg.m	|- M = ( invg ` S )
	psrneg.x	|- ( ph -> X e. B )
Assertion	psrneg	|- ( ph -> ( M ` X ) = ( N o. 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		psrneg.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5		psrneg.i	|- N = ( invg ` R )
6		psrneg.b	|- B = ( Base ` S )
7		psrneg.m	|- M = ( invg ` S )
8		psrneg.x	|- ( ph -> X e. B )
9		eqid	|- ( 0g ` R ) = ( 0g ` R )
10		eqid	|- ( +g ` S ) = ( +g ` S )
11	1 2 3 4 5 6 8 9 10	psrlinv	|- ( ph -> ( ( N o. X ) ( +g ` S ) X ) = ( D X. { ( 0g ` R ) } ) )
12		eqid	|- ( 0g ` S ) = ( 0g ` S )
13	1 2 3 4 9 12	psr0	|- ( ph -> ( 0g ` S ) = ( D X. { ( 0g ` R ) } ) )
14	11 13	eqtr4d	|- ( ph -> ( ( N o. X ) ( +g ` S ) X ) = ( 0g ` S ) )
15	1 2 3	psrgrp	|- ( ph -> S e. Grp )
16	1 2 3 4 5 6 8	psrnegcl	|- ( ph -> ( N o. X ) e. B )
17	6 10 12 7	grpinvid2	|- ( ( S e. Grp /\ X e. B /\ ( N o. X ) e. B ) -> ( ( M ` X ) = ( N o. X ) <-> ( ( N o. X ) ( +g ` S ) X ) = ( 0g ` S ) ) )
18	15 8 16 17	syl3anc	|- ( ph -> ( ( M ` X ) = ( N o. X ) <-> ( ( N o. X ) ( +g ` S ) X ) = ( 0g ` S ) ) )
19	14 18	mpbird	|- ( ph -> ( M ` X ) = ( N o. X ) )