probun

Description: The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016)

		Ref	Expression
	Assertion	probun	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to (A \cap B = \emptyset \to P (A \cup B) = P (A) + P (B))$

Proof

Step	Hyp	Ref	Expression
1		simpll1	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A = B) \land A \cap B = \emptyset) \to P \in Prob$
2		simplr	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A = B) \land A \cap B = \emptyset) \to A = B$
3		simpr	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A = B) \land A \cap B = \emptyset) \to A \cap B = \emptyset$
4		disj3	$⊢ A \cap B = \emptyset \leftrightarrow A = A ∖ B$
5	4	biimpi	$⊢ A \cap B = \emptyset \to A = A ∖ B$
6		difeq1	$⊢ A = B \to A ∖ B = B ∖ B$
7		difid	$⊢ B ∖ B = \emptyset$
8	6 7	eqtrdi	$⊢ A = B \to A ∖ B = \emptyset$
9	5 8	sylan9eqr	$⊢ (A = B \land A \cap B = \emptyset) \to A = \emptyset$
10		eqtr2	$⊢ (A = B \land A = \emptyset) \to B = \emptyset$
11	9 10	syldan	$⊢ (A = B \land A \cap B = \emptyset) \to B = \emptyset$
12	9 11	uneq12d	$⊢ (A = B \land A \cap B = \emptyset) \to A \cup B = \emptyset \cup \emptyset$
13		unidm	$⊢ \emptyset \cup \emptyset = \emptyset$
14	12 13	eqtrdi	$⊢ (A = B \land A \cap B = \emptyset) \to A \cup B = \emptyset$
15	14	fveq2d	$⊢ (A = B \land A \cap B = \emptyset) \to P (A \cup B) = P (\emptyset)$
16		probnul	$⊢ P \in Prob \to P (\emptyset) = 0$
17	15 16	sylan9eqr	$⊢ (P \in Prob \land (A = B \land A \cap B = \emptyset)) \to P (A \cup B) = 0$
18	9	fveq2d	$⊢ (A = B \land A \cap B = \emptyset) \to P (A) = P (\emptyset)$
19	18 16	sylan9eqr	$⊢ (P \in Prob \land (A = B \land A \cap B = \emptyset)) \to P (A) = 0$
20	11	fveq2d	$⊢ (A = B \land A \cap B = \emptyset) \to P (B) = P (\emptyset)$
21	20 16	sylan9eqr	$⊢ (P \in Prob \land (A = B \land A \cap B = \emptyset)) \to P (B) = 0$
22	19 21	oveq12d	$⊢ (P \in Prob \land (A = B \land A \cap B = \emptyset)) \to P (A) + P (B) = 0 + 0$
23		00id	$⊢ 0 + 0 = 0$
24	22 23	eqtrdi	$⊢ (P \in Prob \land (A = B \land A \cap B = \emptyset)) \to P (A) + P (B) = 0$
25	17 24	eqtr4d	$⊢ (P \in Prob \land (A = B \land A \cap B = \emptyset)) \to P (A \cup B) = P (A) + P (B)$
26	1 2 3 25	syl12anc	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A = B) \land A \cap B = \emptyset) \to P (A \cup B) = P (A) + P (B)$
27	26	ex	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A = B) \to (A \cap B = \emptyset \to P (A \cup B) = P (A) + P (B))$
28		3anass	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \leftrightarrow (P \in Prob \land (A \in dom P \land B \in dom P))$
29	28	anbi1i	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \leftrightarrow ((P \in Prob \land (A \in dom P \land B \in dom P)) \land A \neq B)$
30		df-3an	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \leftrightarrow ((P \in Prob \land (A \in dom P \land B \in dom P)) \land A \neq B)$
31	29 30	bitr4i	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \leftrightarrow (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B)$
32		simpl1	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P \in Prob$
33		prssi	$⊢ (A \in dom P \land B \in dom P) \to \{A, B\} \subseteq dom P$
34	33	3ad2ant2	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to \{A, B\} \subseteq dom P$
35	34	adantr	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to \{A, B\} \subseteq dom P$
36		prex	$⊢ \{A, B\} \in V$
37	36	elpw	$⊢ \{A, B\} \in 𝒫 dom P \leftrightarrow \{A, B\} \subseteq dom P$
38	35 37	sylibr	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to \{A, B\} \in 𝒫 dom P$
39		prct	$⊢ (A \in dom P \land B \in dom P) \to \{A, B\} ≼ ω$
40	39	3ad2ant2	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to \{A, B\} ≼ ω$
41	40	adantr	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to \{A, B\} ≼ ω$
42		simp2l	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to A \in dom P$
43		simp2r	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to B \in dom P$
44		simp3	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to A \neq B$
45		id	$⊢ x = A \to x = A$
46		id	$⊢ x = B \to x = B$
47	45 46	disjprg	$⊢ (A \in dom P \land B \in dom P \land A \neq B) \to (\underset{x \in \{A, B\}}{Disj} x \leftrightarrow A \cap B = \emptyset)$
48	42 43 44 47	syl3anc	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to (\underset{x \in \{A, B\}}{Disj} x \leftrightarrow A \cap B = \emptyset)$
49	48	biimpar	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to \underset{x \in \{A, B\}}{Disj} x$
50		probcun	$⊢ (P \in Prob \land \{A, B\} \in 𝒫 dom P \land (\{A, B\} ≼ ω \land \underset{x \in \{A, B\}}{Disj} x)) \to P (⋃ \{A, B\}) = \underset{x \in \{A, B\}}{\sum^{*}} P (x)$
51	32 38 41 49 50	syl112anc	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (⋃ \{A, B\}) = \underset{x \in \{A, B\}}{\sum^{*}} P (x)$
52		uniprg	$⊢ (A \in dom P \land B \in dom P) \to ⋃ \{A, B\} = A \cup B$
53	52	fveq2d	$⊢ (A \in dom P \land B \in dom P) \to P (⋃ \{A, B\}) = P (A \cup B)$
54	53	3ad2ant2	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to P (⋃ \{A, B\}) = P (A \cup B)$
55		fveq2	$⊢ x = A \to P (x) = P (A)$
56	55	adantl	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land x = A) \to P (x) = P (A)$
57		fveq2	$⊢ x = B \to P (x) = P (B)$
58	57	adantl	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land x = B) \to P (x) = P (B)$
59		unitssxrge0	$⊢ [0, 1] \subseteq [0, +∞]$
60		simp1	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to P \in Prob$
61		prob01	$⊢ (P \in Prob \land A \in dom P) \to P (A) \in [0, 1]$
62	60 42 61	syl2anc	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to P (A) \in [0, 1]$
63	59 62	sselid	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to P (A) \in [0, +∞]$
64		prob01	$⊢ (P \in Prob \land B \in dom P) \to P (B) \in [0, 1]$
65	60 43 64	syl2anc	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to P (B) \in [0, 1]$
66	59 65	sselid	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to P (B) \in [0, +∞]$
67	56 58 42 43 63 66 44	esumpr	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to \underset{x \in \{A, B\}}{\sum^{*}} P (x) = P (A) +_{𝑒} P (B)$
68	54 67	eqeq12d	$⊢ (P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \to (P (⋃ \{A, B\}) = \underset{x \in \{A, B\}}{\sum^{*}} P (x) \leftrightarrow P (A \cup B) = P (A) +_{𝑒} P (B))$
69	68	adantr	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to (P (⋃ \{A, B\}) = \underset{x \in \{A, B\}}{\sum^{*}} P (x) \leftrightarrow P (A \cup B) = P (A) +_{𝑒} P (B))$
70	51 69	mpbid	$⊢ ((P \in Prob \land (A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (A \cup B) = P (A) +_{𝑒} P (B)$
71	31 70	sylanb	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (A \cup B) = P (A) +_{𝑒} P (B)$
72		unitssre	$⊢ [0, 1] \subseteq ℝ$
73		simpll1	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P \in Prob$
74		simpll2	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to A \in dom P$
75	73 74 61	syl2anc	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (A) \in [0, 1]$
76	72 75	sselid	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (A) \in ℝ$
77		simpll3	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to B \in dom P$
78	73 77 64	syl2anc	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (B) \in [0, 1]$
79	72 78	sselid	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (B) \in ℝ$
80		rexadd	$⊢ (P (A) \in ℝ \land P (B) \in ℝ) \to P (A) +_{𝑒} P (B) = P (A) + P (B)$
81	76 79 80	syl2anc	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (A) +_{𝑒} P (B) = P (A) + P (B)$
82	71 81	eqtrd	$⊢ (((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \land A \cap B = \emptyset) \to P (A \cup B) = P (A) + P (B)$
83	82	ex	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land A \neq B) \to (A \cap B = \emptyset \to P (A \cup B) = P (A) + P (B))$
84	27 83	pm2.61dane	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to (A \cap B = \emptyset \to P (A \cup B) = P (A) + P (B))$

Metamath Proof Explorer

Theorem probun

Proof