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 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
rrvsum.2 ⊢ ( 𝜑 → 𝑋 : ℕ ⟶ ( rRndVar ‘ 𝑃 ) )
rrvsum.3 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑆 = ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑁 ) )
Assertion rrvsum ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑆 ∈ ( rRndVar ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 rrvsum.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
2 rrvsum.2 ⊢ ( 𝜑 → 𝑋 : ℕ ⟶ ( rRndVar ‘ 𝑃 ) )
3 rrvsum.3 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑆 = ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑁 ) )
4 fveq2 ⊢ ( 𝑘 = 1 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) = ( seq 1 ( ∘f + , 𝑋 ) ‘ 1 ) )
5 4 eleq1d ⊢ ( 𝑘 = 1 → ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( seq 1 ( ∘f + , 𝑋 ) ‘ 1 ) ∈ ( rRndVar ‘ 𝑃 ) ) )
6 5 imbi2d ⊢ ( 𝑘 = 1 → ( ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ) ↔ ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 1 ) ∈ ( rRndVar ‘ 𝑃 ) ) ) )
7 fveq2 ⊢ ( 𝑘 = 𝑛 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) = ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) )
8 7 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) )
9 8 imbi2d ⊢ ( 𝑘 = 𝑛 → ( ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ) ↔ ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) ) )
10 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) = ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) )
11 10 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) ) )
12 11 imbi2d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ) ↔ ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) ) ) )
13 fveq2 ⊢ ( 𝑘 = 𝑁 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) = ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑁 ) )
14 13 eleq1d ⊢ ( 𝑘 = 𝑁 → ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ↔ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑁 ) ∈ ( rRndVar ‘ 𝑃 ) ) )
15 14 imbi2d ⊢ ( 𝑘 = 𝑁 → ( ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑘 ) ∈ ( rRndVar ‘ 𝑃 ) ) ↔ ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑁 ) ∈ ( rRndVar ‘ 𝑃 ) ) ) )
16 1z ⊢ 1 ∈ ℤ
17 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( ∘f + , 𝑋 ) ‘ 1 ) = ( 𝑋 ‘ 1 ) )
18 16 17 ax-mp ⊢ ( seq 1 ( ∘f + , 𝑋 ) ‘ 1 ) = ( 𝑋 ‘ 1 )
19 1nn ⊢ 1 ∈ ℕ
20 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝑋 ‘ 1 ) ∈ ( rRndVar ‘ 𝑃 ) )
21 19 20 mpan2 ⊢ ( 𝜑 → ( 𝑋 ‘ 1 ) ∈ ( rRndVar ‘ 𝑃 ) )
22 18 21 eqeltrid ⊢ ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 1 ) ∈ ( rRndVar ‘ 𝑃 ) )
23 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∘f + ( 𝑋 ‘ ( 𝑛 + 1 ) ) ) )
24 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
25 23 24 eleq2s ⊢ ( 𝑛 ∈ ℕ → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∘f + ( 𝑋 ‘ ( 𝑛 + 1 ) ) ) )
26 25 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∘f + ( 𝑋 ‘ ( 𝑛 + 1 ) ) ) )
27 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) → 𝑃 ∈ Prob )
28 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) )
29 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
30 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝑋 ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) )
31 29 30 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) → ( 𝑋 ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) )
33 27 28 32 rrvadd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) → ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∘f + ( 𝑋 ‘ ( 𝑛 + 1 ) ) ) ∈ ( rRndVar ‘ 𝑃 ) )
34 26 33 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) )
35 34 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) ) )
36 35 expcom ⊢ ( 𝑛 ∈ ℕ → ( 𝜑 → ( ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) ) ) )
37 36 a2d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑛 ) ∈ ( rRndVar ‘ 𝑃 ) ) → ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ ( 𝑛 + 1 ) ) ∈ ( rRndVar ‘ 𝑃 ) ) ) )
38 6 9 12 15 22 37 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝜑 → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑁 ) ∈ ( rRndVar ‘ 𝑃 ) ) )
39 38 impcom ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( ∘f + , 𝑋 ) ‘ 𝑁 ) ∈ ( rRndVar ‘ 𝑃 ) )
40 3 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑆 ∈ ( rRndVar ‘ 𝑃 ) )