Metamath Proof Explorer

Theorem caragenuncllem

Description: The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caragenuncllem.o 
|- ( ph -> O e. OutMeas )
caragenuncllem.s 
|- S = ( CaraGen ` O )
caragenuncllem.e 
|- ( ph -> E e. S )
caragenuncllem.f 
|- ( ph -> F e. S )
caragenuncllem.x 
|- X = U. dom O
caragenuncllem.a 
|- ( ph -> A C_ X )
Assertion caragenuncllem 
|- ( ph -> ( ( O ` ( A i^i ( E u. F ) ) ) +e ( O ` ( A \ ( E u. F ) ) ) ) = ( O ` A ) )

Proof

Step Hyp Ref Expression
1 caragenuncllem.o 
 |-  ( ph -> O e. OutMeas )
2 caragenuncllem.s 
 |-  S = ( CaraGen ` O )
3 caragenuncllem.e 
 |-  ( ph -> E e. S )
4 caragenuncllem.f 
 |-  ( ph -> F e. S )
5 caragenuncllem.x 
 |-  X = U. dom O
6 caragenuncllem.a 
 |-  ( ph -> A C_ X )
7 6 ssinss1d 
 |-  ( ph -> ( A i^i ( E u. F ) ) C_ X )
8 1 2 5 3 7 caragensplit 
 |-  ( ph -> ( ( O ` ( ( A i^i ( E u. F ) ) i^i E ) ) +e ( O ` ( ( A i^i ( E u. F ) ) \ E ) ) ) = ( O ` ( A i^i ( E u. F ) ) ) )
9 8 eqcomd 
 |-  ( ph -> ( O ` ( A i^i ( E u. F ) ) ) = ( ( O ` ( ( A i^i ( E u. F ) ) i^i E ) ) +e ( O ` ( ( A i^i ( E u. F ) ) \ E ) ) ) )
10 inass 
 |-  ( ( A i^i ( E u. F ) ) i^i E ) = ( A i^i ( ( E u. F ) i^i E ) )
11 incom 
 |-  ( ( E u. F ) i^i E ) = ( E i^i ( E u. F ) )
12 inabs 
 |-  ( E i^i ( E u. F ) ) = E
13 11 12 eqtri 
 |-  ( ( E u. F ) i^i E ) = E
14 13 ineq2i 
 |-  ( A i^i ( ( E u. F ) i^i E ) ) = ( A i^i E )
15 10 14 eqtri 
 |-  ( ( A i^i ( E u. F ) ) i^i E ) = ( A i^i E )
16 15 fveq2i 
 |-  ( O ` ( ( A i^i ( E u. F ) ) i^i E ) ) = ( O ` ( A i^i E ) )
17 incom 
 |-  ( ( A \ E ) i^i F ) = ( F i^i ( A \ E ) )
18 indifcom 
 |-  ( F i^i ( A \ E ) ) = ( A i^i ( F \ E ) )
19 17 18 eqtr2i 
 |-  ( A i^i ( F \ E ) ) = ( ( A \ E ) i^i F )
20 19 eqcomi 
 |-  ( ( A \ E ) i^i F ) = ( A i^i ( F \ E ) )
21 difundir 
 |-  ( ( E u. F ) \ E ) = ( ( E \ E ) u. ( F \ E ) )
22 difid 
 |-  ( E \ E ) = (/)
23 22 uneq1i 
 |-  ( ( E \ E ) u. ( F \ E ) ) = ( (/) u. ( F \ E ) )
24 0un 
 |-  ( (/) u. ( F \ E ) ) = ( F \ E )
25 21 23 24 3eqtrri 
 |-  ( F \ E ) = ( ( E u. F ) \ E )
26 25 ineq2i 
 |-  ( A i^i ( F \ E ) ) = ( A i^i ( ( E u. F ) \ E ) )
27 indif2 
 |-  ( A i^i ( ( E u. F ) \ E ) ) = ( ( A i^i ( E u. F ) ) \ E )
28 20 26 27 3eqtrri 
 |-  ( ( A i^i ( E u. F ) ) \ E ) = ( ( A \ E ) i^i F )
29 28 fveq2i 
 |-  ( O ` ( ( A i^i ( E u. F ) ) \ E ) ) = ( O ` ( ( A \ E ) i^i F ) )
30 16 29 oveq12i 
 |-  ( ( O ` ( ( A i^i ( E u. F ) ) i^i E ) ) +e ( O ` ( ( A i^i ( E u. F ) ) \ E ) ) ) = ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) )
31 30 a1i 
 |-  ( ph -> ( ( O ` ( ( A i^i ( E u. F ) ) i^i E ) ) +e ( O ` ( ( A i^i ( E u. F ) ) \ E ) ) ) = ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) ) )
32 eqidd 
 |-  ( ph -> ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) ) = ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) ) )
33 9 31 32 3eqtrd 
 |-  ( ph -> ( O ` ( A i^i ( E u. F ) ) ) = ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) ) )
34 difun1 
 |-  ( A \ ( E u. F ) ) = ( ( A \ E ) \ F )
35 34 fveq2i 
 |-  ( O ` ( A \ ( E u. F ) ) ) = ( O ` ( ( A \ E ) \ F ) )
36 35 a1i 
 |-  ( ph -> ( O ` ( A \ ( E u. F ) ) ) = ( O ` ( ( A \ E ) \ F ) ) )
37 33 36 oveq12d 
 |-  ( ph -> ( ( O ` ( A i^i ( E u. F ) ) ) +e ( O ` ( A \ ( E u. F ) ) ) ) = ( ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) )
38 6 ssinss1d 
 |-  ( ph -> ( A i^i E ) C_ X )
39 1 5 38 omexrcl 
 |-  ( ph -> ( O ` ( A i^i E ) ) e. RR* )
40 1 5 38 omecl 
 |-  ( ph -> ( O ` ( A i^i E ) ) e. ( 0 [,] +oo ) )
41 40 xrge0nemnfd 
 |-  ( ph -> ( O ` ( A i^i E ) ) =/= -oo )
42 39 41 jca 
 |-  ( ph -> ( ( O ` ( A i^i E ) ) e. RR* /\ ( O ` ( A i^i E ) ) =/= -oo ) )
43 1 2 4 5 caragenelss 
 |-  ( ph -> F C_ X )
44 43 ssinss2d 
 |-  ( ph -> ( ( A \ E ) i^i F ) C_ X )
45 1 5 44 omexrcl 
 |-  ( ph -> ( O ` ( ( A \ E ) i^i F ) ) e. RR* )
46 1 5 44 omecl 
 |-  ( ph -> ( O ` ( ( A \ E ) i^i F ) ) e. ( 0 [,] +oo ) )
47 46 xrge0nemnfd 
 |-  ( ph -> ( O ` ( ( A \ E ) i^i F ) ) =/= -oo )
48 45 47 jca 
 |-  ( ph -> ( ( O ` ( ( A \ E ) i^i F ) ) e. RR* /\ ( O ` ( ( A \ E ) i^i F ) ) =/= -oo ) )
49 6 ssdifssd 
 |-  ( ph -> ( A \ E ) C_ X )
50 49 ssdifssd 
 |-  ( ph -> ( ( A \ E ) \ F ) C_ X )
51 1 5 50 omexrcl 
 |-  ( ph -> ( O ` ( ( A \ E ) \ F ) ) e. RR* )
52 1 5 50 omecl 
 |-  ( ph -> ( O ` ( ( A \ E ) \ F ) ) e. ( 0 [,] +oo ) )
53 52 xrge0nemnfd 
 |-  ( ph -> ( O ` ( ( A \ E ) \ F ) ) =/= -oo )
54 51 53 jca 
 |-  ( ph -> ( ( O ` ( ( A \ E ) \ F ) ) e. RR* /\ ( O ` ( ( A \ E ) \ F ) ) =/= -oo ) )
55 xaddass 
 |-  ( ( ( ( O ` ( A i^i E ) ) e. RR* /\ ( O ` ( A i^i E ) ) =/= -oo ) /\ ( ( O ` ( ( A \ E ) i^i F ) ) e. RR* /\ ( O ` ( ( A \ E ) i^i F ) ) =/= -oo ) /\ ( ( O ` ( ( A \ E ) \ F ) ) e. RR* /\ ( O ` ( ( A \ E ) \ F ) ) =/= -oo ) ) -> ( ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) = ( ( O ` ( A i^i E ) ) +e ( ( O ` ( ( A \ E ) i^i F ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) ) )
56 42 48 54 55 syl3anc 
 |-  ( ph -> ( ( ( O ` ( A i^i E ) ) +e ( O ` ( ( A \ E ) i^i F ) ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) = ( ( O ` ( A i^i E ) ) +e ( ( O ` ( ( A \ E ) i^i F ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) ) )
57 1 2 5 4 49 caragensplit 
 |-  ( ph -> ( ( O ` ( ( A \ E ) i^i F ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) = ( O ` ( A \ E ) ) )
58 57 oveq2d 
 |-  ( ph -> ( ( O ` ( A i^i E ) ) +e ( ( O ` ( ( A \ E ) i^i F ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) ) = ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) )
59 1 2 5 3 6 caragensplit 
 |-  ( ph -> ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) = ( O ` A ) )
60 58 59 eqtrd 
 |-  ( ph -> ( ( O ` ( A i^i E ) ) +e ( ( O ` ( ( A \ E ) i^i F ) ) +e ( O ` ( ( A \ E ) \ F ) ) ) ) = ( O ` A ) )
61 37 56 60 3eqtrd 
 |-  ( ph -> ( ( O ` ( A i^i ( E u. F ) ) ) +e ( O ` ( A \ ( E u. F ) ) ) ) = ( O ` A ) )