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 
|- ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. Prob )

Proof

Step Hyp Ref Expression
1 measdivcstALTV 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. ( measures ` S ) )
2 ovex 
 |-  ( ( M ` x ) /e ( M ` U. S ) ) e. _V
3 2 rgenw 
 |-  A. x e. S ( ( M ` x ) /e ( M ` U. S ) ) e. _V
4 dmmptg 
 |-  ( A. x e. S ( ( M ` x ) /e ( M ` U. S ) ) e. _V -> dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) = S )
5 3 4 ax-mp 
 |-  dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) = S
6 5 fveq2i 
 |-  ( measures ` dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ) = ( measures ` S )
7 1 6 eleqtrrdi 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. ( measures ` dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ) )
8 measbasedom 
 |-  ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. U. ran measures <-> ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. ( measures ` dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ) )
9 7 8 sylibr 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. U. ran measures )
10 5 unieqi 
 |-  U. dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) = U. S
11 10 fveq2i 
 |-  ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ` U. dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ) = ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ` U. S )
12 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
13 isrnsigau 
 |-  ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
14 13 simprd 
 |-  ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) )
15 14 simp1d 
 |-  ( S e. U. ran sigAlgebra -> U. S e. S )
16 12 15 syl 
 |-  ( M e. ( measures ` S ) -> U. S e. S )
17 id 
 |-  ( ( M ` U. S ) e. RR+ -> ( M ` U. S ) e. RR+ )
18 17 17 rpxdivcld 
 |-  ( ( M ` U. S ) e. RR+ -> ( ( M ` U. S ) /e ( M ` U. S ) ) e. RR+ )
19 16 18 anim12i 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( U. S e. S /\ ( ( M ` U. S ) /e ( M ` U. S ) ) e. RR+ ) )
20 fveq2 
 |-  ( x = U. S -> ( M ` x ) = ( M ` U. S ) )
21 20 oveq1d 
 |-  ( x = U. S -> ( ( M ` x ) /e ( M ` U. S ) ) = ( ( M ` U. S ) /e ( M ` U. S ) ) )
22 eqid 
 |-  ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) = ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) )
23 21 22 fvmptg 
 |-  ( ( U. S e. S /\ ( ( M ` U. S ) /e ( M ` U. S ) ) e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ` U. S ) = ( ( M ` U. S ) /e ( M ` U. S ) ) )
24 19 23 syl 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ` U. S ) = ( ( M ` U. S ) /e ( M ` U. S ) ) )
25 rpre 
 |-  ( ( M ` U. S ) e. RR+ -> ( M ` U. S ) e. RR )
26 rpne0 
 |-  ( ( M ` U. S ) e. RR+ -> ( M ` U. S ) =/= 0 )
27 xdivid 
 |-  ( ( ( M ` U. S ) e. RR /\ ( M ` U. S ) =/= 0 ) -> ( ( M ` U. S ) /e ( M ` U. S ) ) = 1 )
28 25 26 27 syl2anc 
 |-  ( ( M ` U. S ) e. RR+ -> ( ( M ` U. S ) /e ( M ` U. S ) ) = 1 )
29 28 adantl 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( M ` U. S ) /e ( M ` U. S ) ) = 1 )
30 24 29 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ` U. S ) = 1 )
31 11 30 syl5eq 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ` U. dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ) = 1 )
32 elprob 
 |-  ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. Prob <-> ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. U. ran measures /\ ( ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ` U. dom ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) ) = 1 ) )
33 9 31 32 sylanbrc 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e ( M ` U. S ) ) ) e. Prob )