Metamath Proof Explorer

Theorem caratheodory

Description: Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caratheodory.o 
|- ( ph -> O e. OutMeas )
caratheodory.s 
|- S = ( CaraGen ` O )
Assertion caratheodory 
|- ( ph -> ( O |` S ) e. Meas )

Proof

Step Hyp Ref Expression
1 caratheodory.o 
 |-  ( ph -> O e. OutMeas )
2 caratheodory.s 
 |-  S = ( CaraGen ` O )
3 1 2 caragensal 
 |-  ( ph -> S e. SAlg )
4 eqid 
 |-  U. dom O = U. dom O
5 1 4 omef 
 |-  ( ph -> O : ~P U. dom O --> ( 0 [,] +oo ) )
6 caragenval 
 |-  ( O e. OutMeas -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
7 1 6 syl 
 |-  ( ph -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
8 7 eqcomd 
 |-  ( ph -> { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } = ( CaraGen ` O ) )
9 2 eqcomi 
 |-  ( CaraGen ` O ) = S
10 9 a1i 
 |-  ( ph -> ( CaraGen ` O ) = S )
11 8 10 eqtr2d 
 |-  ( ph -> S = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
12 ssrab2 
 |-  { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } C_ ~P U. dom O
13 11 12 eqsstrdi 
 |-  ( ph -> S C_ ~P U. dom O )
14 5 13 fssresd 
 |-  ( ph -> ( O |` S ) : S --> ( 0 [,] +oo ) )
15 1 2 caragen0 
 |-  ( ph -> (/) e. S )
16 fvres 
 |-  ( (/) e. S -> ( ( O |` S ) ` (/) ) = ( O ` (/) ) )
17 15 16 syl 
 |-  ( ph -> ( ( O |` S ) ` (/) ) = ( O ` (/) ) )
18 1 ome0 
 |-  ( ph -> ( O ` (/) ) = 0 )
19 17 18 eqtrd 
 |-  ( ph -> ( ( O |` S ) ` (/) ) = 0 )
20 simp1 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> ph )
21 simp2 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> e : NN --> S )
22 fveq2 
 |-  ( n = m -> ( e ` n ) = ( e ` m ) )
23 22 cbvdisjv 
 |-  ( Disj_ n e. NN ( e ` n ) <-> Disj_ m e. NN ( e ` m ) )
24 23 biimpi 
 |-  ( Disj_ n e. NN ( e ` n ) -> Disj_ m e. NN ( e ` m ) )
25 24 3ad2ant3 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> Disj_ m e. NN ( e ` m ) )
26 1 3ad2ant1 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ m e. NN ( e ` m ) ) -> O e. OutMeas )
27 simp2 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ m e. NN ( e ` m ) ) -> e : NN --> S )
28 23 biimpri 
 |-  ( Disj_ m e. NN ( e ` m ) -> Disj_ n e. NN ( e ` n ) )
29 28 3ad2ant3 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ m e. NN ( e ` m ) ) -> Disj_ n e. NN ( e ` n ) )
30 fveq2 
 |-  ( m = n -> ( e ` m ) = ( e ` n ) )
31 30 cbviunv 
 |-  U_ m e. ( 1 ... j ) ( e ` m ) = U_ n e. ( 1 ... j ) ( e ` n )
32 31 mpteq2i 
 |-  ( j e. NN |-> U_ m e. ( 1 ... j ) ( e ` m ) ) = ( j e. NN |-> U_ n e. ( 1 ... j ) ( e ` n ) )
33 26 4 2 27 29 32 caratheodorylem2 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ m e. NN ( e ` m ) ) -> ( O ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( e ` n ) ) ) ) )
34 20 21 25 33 syl3anc 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> ( O ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( e ` n ) ) ) ) )
35 3 adantr 
 |-  ( ( ph /\ e : NN --> S ) -> S e. SAlg )
36 nnenom 
 |-  NN ~~ _om
37 endom 
 |-  ( NN ~~ _om -> NN ~<_ _om )
38 36 37 ax-mp 
 |-  NN ~<_ _om
39 38 a1i 
 |-  ( ( ph /\ e : NN --> S ) -> NN ~<_ _om )
40 ffvelrn 
 |-  ( ( e : NN --> S /\ n e. NN ) -> ( e ` n ) e. S )
41 40 adantll 
 |-  ( ( ( ph /\ e : NN --> S ) /\ n e. NN ) -> ( e ` n ) e. S )
42 35 39 41 saliuncl 
 |-  ( ( ph /\ e : NN --> S ) -> U_ n e. NN ( e ` n ) e. S )
43 fvres 
 |-  ( U_ n e. NN ( e ` n ) e. S -> ( ( O |` S ) ` U_ n e. NN ( e ` n ) ) = ( O ` U_ n e. NN ( e ` n ) ) )
44 42 43 syl 
 |-  ( ( ph /\ e : NN --> S ) -> ( ( O |` S ) ` U_ n e. NN ( e ` n ) ) = ( O ` U_ n e. NN ( e ` n ) ) )
45 44 3adant3 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> ( ( O |` S ) ` U_ n e. NN ( e ` n ) ) = ( O ` U_ n e. NN ( e ` n ) ) )
46 fvres 
 |-  ( ( e ` n ) e. S -> ( ( O |` S ) ` ( e ` n ) ) = ( O ` ( e ` n ) ) )
47 41 46 syl 
 |-  ( ( ( ph /\ e : NN --> S ) /\ n e. NN ) -> ( ( O |` S ) ` ( e ` n ) ) = ( O ` ( e ` n ) ) )
48 47 mpteq2dva 
 |-  ( ( ph /\ e : NN --> S ) -> ( n e. NN |-> ( ( O |` S ) ` ( e ` n ) ) ) = ( n e. NN |-> ( O ` ( e ` n ) ) ) )
49 48 fveq2d 
 |-  ( ( ph /\ e : NN --> S ) -> ( sum^ ` ( n e. NN |-> ( ( O |` S ) ` ( e ` n ) ) ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( e ` n ) ) ) ) )
50 49 3adant3 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> ( sum^ ` ( n e. NN |-> ( ( O |` S ) ` ( e ` n ) ) ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( e ` n ) ) ) ) )
51 34 45 50 3eqtr4d 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> ( ( O |` S ) ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( ( O |` S ) ` ( e ` n ) ) ) ) )
52 3 14 19 51 ismeannd 
 |-  ( ph -> ( O |` S ) e. Meas )