Metamath Proof Explorer

Theorem psrnegcl

Description: The negative function in 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 )
psrnegcl.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrnegcl.i 
|- N = ( invg ` R )
psrnegcl.b 
|- B = ( Base ` S )
psrnegcl.z 
|- ( ph -> X e. B )
Assertion psrnegcl 
|- ( ph -> ( N o. X ) 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 psrnegcl.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psrnegcl.i 
 |-  N = ( invg ` R )
6 psrnegcl.b 
 |-  B = ( Base ` S )
7 psrnegcl.z 
 |-  ( ph -> X e. B )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 5 3 grpinvf1o 
 |-  ( ph -> N : ( Base ` R ) -1-1-onto-> ( Base ` R ) )
10 f1of 
 |-  ( N : ( Base ` R ) -1-1-onto-> ( Base ` R ) -> N : ( Base ` R ) --> ( Base ` R ) )
11 9 10 syl 
 |-  ( ph -> N : ( Base ` R ) --> ( Base ` R ) )
12 1 8 4 6 7 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
13 fco 
 |-  ( ( N : ( Base ` R ) --> ( Base ` R ) /\ X : D --> ( Base ` R ) ) -> ( N o. X ) : D --> ( Base ` R ) )
14 11 12 13 syl2anc 
 |-  ( ph -> ( N o. X ) : D --> ( Base ` R ) )
15 fvex 
 |-  ( Base ` R ) e. _V
16 ovex 
 |-  ( NN0 ^m I ) e. _V
17 4 16 rabex2 
 |-  D e. _V
18 15 17 elmap 
 |-  ( ( N o. X ) e. ( ( Base ` R ) ^m D ) <-> ( N o. X ) : D --> ( Base ` R ) )
19 14 18 sylibr 
 |-  ( ph -> ( N o. X ) e. ( ( Base ` R ) ^m D ) )
20 1 8 4 6 2 psrbas 
 |-  ( ph -> B = ( ( Base ` R ) ^m D ) )
21 19 20 eleqtrrd 
 |-  ( ph -> ( N o. X ) e. B )