Metamath Proof Explorer

Theorem rrvsum

Description: An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017)

Ref Expression
Hypotheses rrvsum.1 
|- ( ph -> P e. Prob )
rrvsum.2 
|- ( ph -> X : NN --> ( rRndVar ` P ) )
rrvsum.3 
|- ( ( ph /\ N e. NN ) -> S = ( seq 1 ( oF + , X ) ` N ) )
Assertion rrvsum 
|- ( ( ph /\ N e. NN ) -> S e. ( rRndVar ` P ) )

Proof

Step Hyp Ref Expression
1 rrvsum.1 
 |-  ( ph -> P e. Prob )
2 rrvsum.2 
 |-  ( ph -> X : NN --> ( rRndVar ` P ) )
3 rrvsum.3 
 |-  ( ( ph /\ N e. NN ) -> S = ( seq 1 ( oF + , X ) ` N ) )
4 fveq2 
 |-  ( k = 1 -> ( seq 1 ( oF + , X ) ` k ) = ( seq 1 ( oF + , X ) ` 1 ) )
5 4 eleq1d 
 |-  ( k = 1 -> ( ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) <-> ( seq 1 ( oF + , X ) ` 1 ) e. ( rRndVar ` P ) ) )
6 5 imbi2d 
 |-  ( k = 1 -> ( ( ph -> ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) ) <-> ( ph -> ( seq 1 ( oF + , X ) ` 1 ) e. ( rRndVar ` P ) ) ) )
7 fveq2 
 |-  ( k = n -> ( seq 1 ( oF + , X ) ` k ) = ( seq 1 ( oF + , X ) ` n ) )
8 7 eleq1d 
 |-  ( k = n -> ( ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) <-> ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) )
9 8 imbi2d 
 |-  ( k = n -> ( ( ph -> ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) ) <-> ( ph -> ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) ) )
10 fveq2 
 |-  ( k = ( n + 1 ) -> ( seq 1 ( oF + , X ) ` k ) = ( seq 1 ( oF + , X ) ` ( n + 1 ) ) )
11 10 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) <-> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) e. ( rRndVar ` P ) ) )
12 11 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) ) <-> ( ph -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) e. ( rRndVar ` P ) ) ) )
13 fveq2 
 |-  ( k = N -> ( seq 1 ( oF + , X ) ` k ) = ( seq 1 ( oF + , X ) ` N ) )
14 13 eleq1d 
 |-  ( k = N -> ( ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) <-> ( seq 1 ( oF + , X ) ` N ) e. ( rRndVar ` P ) ) )
15 14 imbi2d 
 |-  ( k = N -> ( ( ph -> ( seq 1 ( oF + , X ) ` k ) e. ( rRndVar ` P ) ) <-> ( ph -> ( seq 1 ( oF + , X ) ` N ) e. ( rRndVar ` P ) ) ) )
16 1z 
 |-  1 e. ZZ
17 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( oF + , X ) ` 1 ) = ( X ` 1 ) )
18 16 17 ax-mp 
 |-  ( seq 1 ( oF + , X ) ` 1 ) = ( X ` 1 )
19 1nn 
 |-  1 e. NN
20 2 ffvelrnda 
 |-  ( ( ph /\ 1 e. NN ) -> ( X ` 1 ) e. ( rRndVar ` P ) )
21 19 20 mpan2 
 |-  ( ph -> ( X ` 1 ) e. ( rRndVar ` P ) )
22 18 21 eqeltrid 
 |-  ( ph -> ( seq 1 ( oF + , X ) ` 1 ) e. ( rRndVar ` P ) )
23 seqp1 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) = ( ( seq 1 ( oF + , X ) ` n ) oF + ( X ` ( n + 1 ) ) ) )
24 nnuz 
 |-  NN = ( ZZ>= ` 1 )
25 23 24 eleq2s 
 |-  ( n e. NN -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) = ( ( seq 1 ( oF + , X ) ` n ) oF + ( X ` ( n + 1 ) ) ) )
26 25 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) = ( ( seq 1 ( oF + , X ) ` n ) oF + ( X ` ( n + 1 ) ) ) )
27 1 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) -> P e. Prob )
28 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) -> ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) )
29 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
30 2 ffvelrnda 
 |-  ( ( ph /\ ( n + 1 ) e. NN ) -> ( X ` ( n + 1 ) ) e. ( rRndVar ` P ) )
31 29 30 sylan2 
 |-  ( ( ph /\ n e. NN ) -> ( X ` ( n + 1 ) ) e. ( rRndVar ` P ) )
32 31 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) -> ( X ` ( n + 1 ) ) e. ( rRndVar ` P ) )
33 27 28 32 rrvadd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) -> ( ( seq 1 ( oF + , X ) ` n ) oF + ( X ` ( n + 1 ) ) ) e. ( rRndVar ` P ) )
34 26 33 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) e. ( rRndVar ` P ) )
35 34 ex 
 |-  ( ( ph /\ n e. NN ) -> ( ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) e. ( rRndVar ` P ) ) )
36 35 expcom 
 |-  ( n e. NN -> ( ph -> ( ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) e. ( rRndVar ` P ) ) ) )
37 36 a2d 
 |-  ( n e. NN -> ( ( ph -> ( seq 1 ( oF + , X ) ` n ) e. ( rRndVar ` P ) ) -> ( ph -> ( seq 1 ( oF + , X ) ` ( n + 1 ) ) e. ( rRndVar ` P ) ) ) )
38 6 9 12 15 22 37 nnind 
 |-  ( N e. NN -> ( ph -> ( seq 1 ( oF + , X ) ` N ) e. ( rRndVar ` P ) ) )
39 38 impcom 
 |-  ( ( ph /\ N e. NN ) -> ( seq 1 ( oF + , X ) ` N ) e. ( rRndVar ` P ) )
40 3 39 eqeltrd 
 |-  ( ( ph /\ N e. NN ) -> S e. ( rRndVar ` P ) )