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 φ P Prob
rrvsum.2 φ X : RndVar P
rrvsum.3 φ N S = seq 1 f + X N
Assertion rrvsum φ N S RndVar P

Proof

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