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 φ O OutMeas
caratheodory.s S = CaraGen O
Assertion caratheodory φ O S Meas

Proof

Step Hyp Ref Expression
1 caratheodory.o φ O OutMeas
2 caratheodory.s S = CaraGen O
3 1 2 caragensal φ S SAlg
4 eqid dom O = dom O
5 1 4 omef φ O : 𝒫 dom O 0 +∞
6 caragenval O OutMeas CaraGen O = e 𝒫 dom O | a 𝒫 dom O O a e + 𝑒 O a e = O a
7 1 6 syl φ CaraGen O = e 𝒫 dom O | a 𝒫 dom O O a e + 𝑒 O a e = O a
8 7 eqcomd φ e 𝒫 dom O | a 𝒫 dom O O a e + 𝑒 O a e = O a = CaraGen O
9 2 eqcomi CaraGen O = S
10 9 a1i φ CaraGen O = S
11 8 10 eqtr2d φ S = e 𝒫 dom O | a 𝒫 dom O O a e + 𝑒 O a e = O a
12 ssrab2 e 𝒫 dom O | a 𝒫 dom O O a e + 𝑒 O a e = O a 𝒫 dom O
13 11 12 eqsstrdi φ S 𝒫 dom O
14 5 13 fssresd φ O S : S 0 +∞
15 1 2 caragen0 φ S
16 fvres S O S = O
17 15 16 syl φ O S = O
18 1 ome0 φ O = 0
19 17 18 eqtrd φ O S = 0
20 simp1 φ e : S Disj n e n φ
21 simp2 φ e : S Disj n e n e : S
22 fveq2 n = m e n = e m
23 22 cbvdisjv Disj n e n Disj m e m
24 23 biimpi Disj n e n Disj m e m
25 24 3ad2ant3 φ e : S Disj n e n Disj m e m
26 1 3ad2ant1 φ e : S Disj m e m O OutMeas
27 simp2 φ e : S Disj m e m e : S
28 23 biimpri Disj m e m Disj n e n
29 28 3ad2ant3 φ e : S Disj m e m Disj n e n
30 fveq2 m = n e m = e n
31 30 cbviunv m = 1 j e m = n = 1 j e n
32 31 mpteq2i j m = 1 j e m = j n = 1 j e n
33 26 4 2 27 29 32 caratheodorylem2 φ e : S Disj m e m O n e n = sum^ n O e n
34 20 21 25 33 syl3anc φ e : S Disj n e n O n e n = sum^ n O e n
35 3 adantr φ e : S S SAlg
36 nnenom ω
37 endom ω ω
38 36 37 ax-mp ω
39 38 a1i φ e : S ω
40 ffvelrn e : S n e n S
41 40 adantll φ e : S n e n S
42 35 39 41 saliuncl φ e : S n e n S
43 fvres n e n S O S n e n = O n e n
44 42 43 syl φ e : S O S n e n = O n e n
45 44 3adant3 φ e : S Disj n e n O S n e n = O n e n
46 fvres e n S O S e n = O e n
47 41 46 syl φ e : S n O S e n = O e n
48 47 mpteq2dva φ e : S n O S e n = n O e n
49 48 fveq2d φ e : S sum^ n O S e n = sum^ n O e n
50 49 3adant3 φ e : S Disj n e n sum^ n O S e n = sum^ n O e n
51 34 45 50 3eqtr4d φ e : S Disj n e n O S n e n = sum^ n O S e n
52 3 14 19 51 ismeannd φ O S Meas