Metamath Proof Explorer

Theorem psraddcl

Description: Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psraddcl.s 
|- S = ( I mPwSer R )
psraddcl.b 
|- B = ( Base ` S )
psraddcl.p 
|- .+ = ( +g ` S )
psraddcl.r 
|- ( ph -> R e. Grp )
psraddcl.x 
|- ( ph -> X e. B )
psraddcl.y 
|- ( ph -> Y e. B )
Assertion psraddcl 
|- ( ph -> ( X .+ Y ) e. B )

Proof

Step Hyp Ref Expression
1 psraddcl.s 
 |-  S = ( I mPwSer R )
2 psraddcl.b 
 |-  B = ( Base ` S )
3 psraddcl.p 
 |-  .+ = ( +g ` S )
4 psraddcl.r 
 |-  ( ph -> R e. Grp )
5 psraddcl.x 
 |-  ( ph -> X e. B )
6 psraddcl.y 
 |-  ( ph -> Y e. B )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( +g ` R ) = ( +g ` R )
9 7 8 grpcl 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
10 9 3expb 
 |-  ( ( R e. Grp /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
11 4 10 sylan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
12 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
13 1 7 12 2 5 psrelbas 
 |-  ( ph -> X : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
14 1 7 12 2 6 psrelbas 
 |-  ( ph -> Y : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
15 ovex 
 |-  ( NN0 ^m I ) e. _V
16 15 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
17 16 a1i 
 |-  ( ph -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
18 inidm 
 |-  ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } i^i { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
19 11 13 14 17 17 18 off 
 |-  ( ph -> ( X oF ( +g ` R ) Y ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
20 fvex 
 |-  ( Base ` R ) e. _V
21 20 16 elmap 
 |-  ( ( X oF ( +g ` R ) Y ) e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) <-> ( X oF ( +g ` R ) Y ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
22 19 21 sylibr 
 |-  ( ph -> ( X oF ( +g ` R ) Y ) e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
23 1 2 8 3 5 6 psradd 
 |-  ( ph -> ( X .+ Y ) = ( X oF ( +g ` R ) Y ) )
24 reldmpsr 
 |-  Rel dom mPwSer
25 24 1 2 elbasov 
 |-  ( X e. B -> ( I e. _V /\ R e. _V ) )
26 5 25 syl 
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
27 26 simpld 
 |-  ( ph -> I e. _V )
28 1 7 12 2 27 psrbas 
 |-  ( ph -> B = ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
29 22 23 28 3eltr4d 
 |-  ( ph -> ( X .+ Y ) e. B )