This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )