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	$⊢ φ \to O \in OutMeas$
	caratheodory.s	$⊢ S = CaraGen (O)$
Assertion	caratheodory	$⊢ φ \to {O ↾}_{S} \in Meas$

Proof

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

Metamath Proof Explorer

Theorem caratheodory

Proof