Metamath Proof Explorer

Theorem probfinmeasbALTV

Description: Alternate version of probfinmeasb . (Contributed by Thierry Arnoux, 17-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion probfinmeasbALTV ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ Prob )

Proof

Step Hyp Ref Expression
1 measdivcstALTV ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ ( measures ‘ 𝑆 ) )
2 ovex ⊢ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ V
3 2 rgenw ⊢ ∀ 𝑥 ∈ 𝑆 ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ V
4 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ V → dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = 𝑆 )
5 3 4 ax-mp ⊢ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = 𝑆
6 5 fveq2i ⊢ ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ) = ( measures ‘ 𝑆 )
7 1 6 eleqtrrdi ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ) )
8 measbasedom ⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ ∪ ran measures ↔ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ ( measures ‘ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ) )
9 7 8 sylibr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ ∪ ran measures )
10 5 unieqi ⊢ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = ∪ 𝑆
11 10 fveq2i ⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ) = ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ‘ ∪ 𝑆 )
12 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
13 isrnsigau ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) ) )
14 13 simprd ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆 ) ) )
15 14 simp1d ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆 )
16 12 15 syl ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∪ 𝑆 ∈ 𝑆 )
17 id ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ )
18 17 17 rpxdivcld ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ℝ+ )
19 16 18 anim12i ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ∪ 𝑆 ∈ 𝑆 ∧ ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ℝ+ ) )
20 fveq2 ⊢ ( 𝑥 = ∪ 𝑆 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑆 ) )
21 20 oveq1d ⊢ ( 𝑥 = ∪ 𝑆 → ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) )
22 eqid ⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) )
23 21 22 fvmptg ⊢ ( ( ∪ 𝑆 ∈ 𝑆 ∧ ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ‘ ∪ 𝑆 ) = ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) )
24 19 23 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ‘ ∪ 𝑆 ) = ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) )
25 rpre ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ )
26 rpne0 ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( 𝑀 ‘ ∪ 𝑆 ) ≠ 0 )
27 xdivid ⊢ ( ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ ∧ ( 𝑀 ‘ ∪ 𝑆 ) ≠ 0 ) → ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = 1 )
28 25 26 27 syl2anc ⊢ ( ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ → ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = 1 )
29 28 adantl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑀 ‘ ∪ 𝑆 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) = 1 )
30 24 29 eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ‘ ∪ 𝑆 ) = 1 )
31 11 30 syl5eq ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ) = 1 )
32 elprob ⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ Prob ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ ∪ ran measures ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ‘ ∪ dom ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ) = 1 ) )
33 9 31 32 sylanbrc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑀 ‘ ∪ 𝑆 ) ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 ( 𝑀 ‘ ∪ 𝑆 ) ) ) ∈ Prob )