Metamath Proof Explorer

Theorem caragensplit

Description: If E is in the set generated by the Caratheodory's method, then it splits any set A in two parts such that the sum of the outer measures of the two parts is equal to the outer measure of the whole set A . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caragensplit.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
caragensplit.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
caragensplit.x ⊢ 𝑋 = ∪ dom 𝑂
caragensplit.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
caragensplit.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
Assertion caragensplit ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 caragensplit.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 caragensplit.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 caragensplit.x ⊢ 𝑋 = ∪ dom 𝑂
4 caragensplit.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
5 caragensplit.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
6 1 3 unidmex ⊢ ( 𝜑 → 𝑋 ∈ V )
7 ssexg ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ V ) → 𝐴 ∈ V )
8 5 6 7 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ V )
9 elpwg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
10 8 9 syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
11 5 10 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝑋 )
12 3 pweqi ⊢ 𝒫 𝑋 = 𝒫 ∪ dom 𝑂
13 11 12 eleqtrdi ⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ∪ dom 𝑂 )
14 1 2 caragenel ⊢ ( 𝜑 → ( 𝐸 ∈ 𝑆 ↔ ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) ) )
15 4 14 mpbid ⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
16 15 simprd ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
17 ineq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∩ 𝐸 ) = ( 𝐴 ∩ 𝐸 ) )
18 17 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) = ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) )
19 difeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∖ 𝐸 ) = ( 𝐴 ∖ 𝐸 ) )
20 19 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) = ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) )
21 18 20 oveq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) )
22 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑂 ‘ 𝑎 ) = ( 𝑂 ‘ 𝐴 ) )
23 21 22 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ↔ ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝐴 ) ) )
24 23 rspcva ⊢ ( ( 𝐴 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝐴 ) )
25 13 16 24 syl2anc ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝐴 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝐴 ) )