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 
|- ( ph -> O e. OutMeas )
caragensplit.s 
|- S = ( CaraGen ` O )
caragensplit.x 
|- X = U. dom O
caragensplit.e 
|- ( ph -> E e. S )
caragensplit.a 
|- ( ph -> A C_ X )
Assertion caragensplit 
|- ( ph -> ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) = ( O ` A ) )

Proof

Step Hyp Ref Expression
1 caragensplit.o 
 |-  ( ph -> O e. OutMeas )
2 caragensplit.s 
 |-  S = ( CaraGen ` O )
3 caragensplit.x 
 |-  X = U. dom O
4 caragensplit.e 
 |-  ( ph -> E e. S )
5 caragensplit.a 
 |-  ( ph -> A C_ X )
6 1 3 unidmex 
 |-  ( ph -> X e. _V )
7 ssexg 
 |-  ( ( A C_ X /\ X e. _V ) -> A e. _V )
8 5 6 7 syl2anc 
 |-  ( ph -> A e. _V )
9 elpwg 
 |-  ( A e. _V -> ( A e. ~P X <-> A C_ X ) )
10 8 9 syl 
 |-  ( ph -> ( A e. ~P X <-> A C_ X ) )
11 5 10 mpbird 
 |-  ( ph -> A e. ~P X )
12 3 pweqi 
 |-  ~P X = ~P U. dom O
13 11 12 eleqtrdi 
 |-  ( ph -> A e. ~P U. dom O )
14 1 2 caragenel 
 |-  ( ph -> ( E e. 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 ) ) ) )
15 4 14 mpbid 
 |-  ( 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 ) ) )
16 15 simprd 
 |-  ( ph -> A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
17 ineq1 
 |-  ( a = A -> ( a i^i E ) = ( A i^i E ) )
18 17 fveq2d 
 |-  ( a = A -> ( O ` ( a i^i E ) ) = ( O ` ( A i^i E ) ) )
19 difeq1 
 |-  ( a = A -> ( a \ E ) = ( A \ E ) )
20 19 fveq2d 
 |-  ( a = A -> ( O ` ( a \ E ) ) = ( O ` ( A \ E ) ) )
21 18 20 oveq12d 
 |-  ( a = A -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) )
22 fveq2 
 |-  ( a = A -> ( O ` a ) = ( O ` A ) )
23 21 22 eqeq12d 
 |-  ( a = A -> ( ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) <-> ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) = ( O ` A ) ) )
24 23 rspcva 
 |-  ( ( A e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) -> ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) = ( O ` A ) )
25 13 16 24 syl2anc 
 |-  ( ph -> ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) = ( O ` A ) )