Metamath Proof Explorer

Theorem coinfliplem

Description: Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017)

Ref Expression
Hypotheses coinflip.h ⊢ 𝐻 ∈ V
coinflip.t ⊢ 𝑇 ∈ V
coinflip.th ⊢ 𝐻 ≠ 𝑇
coinflip.2 ⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
coinflip.3 ⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
Assertion coinfliplem 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 2 )

Proof

Step Hyp Ref Expression
1 coinflip.h ⊢ 𝐻 ∈ V
2 coinflip.t ⊢ 𝑇 ∈ V
3 coinflip.th ⊢ 𝐻 ≠ 𝑇
4 coinflip.2 ⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
5 coinflip.3 ⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
6 simpr ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } )
7 fvres ⊢ ( 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ 𝑥 ) = ( ♯ ‘ 𝑥 ) )
8 6 7 syl ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ 𝑥 ) = ( ♯ ‘ 𝑥 ) )
9 prfi ⊢ { 𝐻 , 𝑇 } ∈ Fin
10 6 elpwid ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → 𝑥 ⊆ { 𝐻 , 𝑇 } )
11 ssfi ⊢ ( ( { 𝐻 , 𝑇 } ∈ Fin ∧ 𝑥 ⊆ { 𝐻 , 𝑇 } ) → 𝑥 ∈ Fin )
12 9 10 11 sylancr ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → 𝑥 ∈ Fin )
13 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
14 12 13 syl ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
15 14 nn0red ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → ( ♯ ‘ 𝑥 ) ∈ ℝ )
16 8 15 eqeltrd ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ 𝑥 ) ∈ ℝ )
17 simpr ⊢ ( ( 𝐻 ∈ V ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
18 2re ⊢ 2 ∈ ℝ
19 18 a1i ⊢ ( ( 𝐻 ∈ V ∧ 𝑦 ∈ ℝ ) → 2 ∈ ℝ )
20 2ne0 ⊢ 2 ≠ 0
21 20 a1i ⊢ ( ( 𝐻 ∈ V ∧ 𝑦 ∈ ℝ ) → 2 ≠ 0 )
22 rexdiv ⊢ ( ( 𝑦 ∈ ℝ ∧ 2 ∈ ℝ ∧ 2 ≠ 0 ) → ( 𝑦 /𝑒 2 ) = ( 𝑦 / 2 ) )
23 17 19 21 22 syl3anc ⊢ ( ( 𝐻 ∈ V ∧ 𝑦 ∈ ℝ ) → ( 𝑦 /𝑒 2 ) = ( 𝑦 / 2 ) )
24 hashresfn ⊢ ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) Fn 𝒫 { 𝐻 , 𝑇 }
25 24 a1i ⊢ ( 𝐻 ∈ V → ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) Fn 𝒫 { 𝐻 , 𝑇 } )
26 pwfi ⊢ ( { 𝐻 , 𝑇 } ∈ Fin ↔ 𝒫 { 𝐻 , 𝑇 } ∈ Fin )
27 9 26 mpbi ⊢ 𝒫 { 𝐻 , 𝑇 } ∈ Fin
28 27 a1i ⊢ ( 𝐻 ∈ V → 𝒫 { 𝐻 , 𝑇 } ∈ Fin )
29 18 a1i ⊢ ( 𝐻 ∈ V → 2 ∈ ℝ )
30 16 23 25 28 29 ofcfeqd2 ⊢ ( 𝐻 ∈ V → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 2 ) = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) )
31 1 30 ax-mp ⊢ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 2 ) = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
32 4 31 eqtr4i ⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 2 )