rrvsum

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

	Ref	Expression
Hypotheses	rrvsum.1	$⊢ φ \to P \in Prob$
	rrvsum.2	$⊢ φ \to X : ℕ ⟶ {RndVar}_{ℝ} (P)$
	rrvsum.3	$⊢ (φ \land N \in ℕ) \to S = seq 1 (\circ_{f} +, X) (N)$
Assertion	rrvsum	$⊢ (φ \land N \in ℕ) \to S \in {RndVar}_{ℝ} (P)$

Proof

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

Metamath Proof Explorer

Theorem rrvsum

Proof