Theorem cndprobin

Description: An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Assertion	cndprobin	⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) = ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cndprobval	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
2	1	oveq1d	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) = ( ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) · ( 𝑃 ‘ 𝐵 ) ) )
3	2	adantr	⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) = ( ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) · ( 𝑃 ‘ 𝐵 ) ) )
4		unitsscn	⊢ ( 0 [,] 1 ) ⊆ ℂ
5		simp1	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → 𝑃 ∈ Prob )
6		domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
7		inelsiga	⊢ ( ( dom 𝑃 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝐴 ∩ 𝐵 ) ∈ dom 𝑃 )
8	6 7	syl3an1	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝐴 ∩ 𝐵 ) ∈ dom 𝑃 )
9		prob01	⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∩ 𝐵 ) ∈ dom 𝑃 ) → ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] 1 ) )
10	5 8 9	syl2anc	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] 1 ) )
11	4 10	sseldi	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℂ )
12	11	adantr	⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℂ )
13		prob01	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
14	13	3adant2	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
15	4 14	sseldi	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐵 ) ∈ ℂ )
16	15	adantr	⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ∈ ℂ )
17		simpr	⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ≠ 0 )
18	12 16 17	divcan1d	⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) · ( 𝑃 ‘ 𝐵 ) ) = ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) )
19	3 18	eqtrd	⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) = ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) )