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