Metamath Proof Explorer

Theorem psrlinv

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 )
psrlinv.o 
|- .0. = ( 0g ` R )
psrlinv.p 
|- .+ = ( +g ` S )
Assertion psrlinv 
|- ( ph -> ( ( N o. X ) .+ X ) = ( D X. { .0. } ) )

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 psrlinv.o 
 |-  .0. = ( 0g ` R )
9 psrlinv.p 
 |-  .+ = ( +g ` S )
10 ovex 
 |-  ( NN0 ^m I ) e. _V
11 4 10 rabex2 
 |-  D e. _V
12 11 a1i 
 |-  ( ph -> D e. _V )
13 fvexd 
 |-  ( ( ph /\ x e. D ) -> ( N ` ( X ` x ) ) e. _V )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 1 14 4 6 7 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
16 15 ffvelrnda 
 |-  ( ( ph /\ x e. D ) -> ( X ` x ) e. ( Base ` R ) )
17 15 feqmptd 
 |-  ( ph -> X = ( x e. D |-> ( X ` x ) ) )
18 14 5 3 grpinvf1o 
 |-  ( ph -> N : ( Base ` R ) -1-1-onto-> ( Base ` R ) )
19 f1of 
 |-  ( N : ( Base ` R ) -1-1-onto-> ( Base ` R ) -> N : ( Base ` R ) --> ( Base ` R ) )
20 18 19 syl 
 |-  ( ph -> N : ( Base ` R ) --> ( Base ` R ) )
21 20 feqmptd 
 |-  ( ph -> N = ( y e. ( Base ` R ) |-> ( N ` y ) ) )
22 fveq2 
 |-  ( y = ( X ` x ) -> ( N ` y ) = ( N ` ( X ` x ) ) )
23 16 17 21 22 fmptco 
 |-  ( ph -> ( N o. X ) = ( x e. D |-> ( N ` ( X ` x ) ) ) )
24 12 13 16 23 17 offval2 
 |-  ( ph -> ( ( N o. X ) oF ( +g ` R ) X ) = ( x e. D |-> ( ( N ` ( X ` x ) ) ( +g ` R ) ( X ` x ) ) ) )
25 eqid 
 |-  ( +g ` R ) = ( +g ` R )
26 1 2 3 4 5 6 7 psrnegcl 
 |-  ( ph -> ( N o. X ) e. B )
27 1 6 25 9 26 7 psradd 
 |-  ( ph -> ( ( N o. X ) .+ X ) = ( ( N o. X ) oF ( +g ` R ) X ) )
28 fconstmpt 
 |-  ( D X. { .0. } ) = ( x e. D |-> .0. )
29 14 25 8 5 grplinv 
 |-  ( ( R e. Grp /\ ( X ` x ) e. ( Base ` R ) ) -> ( ( N ` ( X ` x ) ) ( +g ` R ) ( X ` x ) ) = .0. )
30 3 16 29 syl2an2r 
 |-  ( ( ph /\ x e. D ) -> ( ( N ` ( X ` x ) ) ( +g ` R ) ( X ` x ) ) = .0. )
31 30 mpteq2dva 
 |-  ( ph -> ( x e. D |-> ( ( N ` ( X ` x ) ) ( +g ` R ) ( X ` x ) ) ) = ( x e. D |-> .0. ) )
32 28 31 eqtr4id 
 |-  ( ph -> ( D X. { .0. } ) = ( x e. D |-> ( ( N ` ( X ` x ) ) ( +g ` R ) ( X ` x ) ) ) )
33 24 27 32 3eqtr4d 
 |-  ( ph -> ( ( N o. X ) .+ X ) = ( D X. { .0. } ) )