Step |
Hyp |
Ref |
Expression |
1 |
|
caragendifcl.o |
|- ( ph -> O e. OutMeas ) |
2 |
|
caragendifcl.s |
|- S = ( CaraGen ` O ) |
3 |
|
caragendifcl.e |
|- ( ph -> E e. S ) |
4 |
|
eqid |
|- U. dom O = U. dom O |
5 |
2
|
caragenss |
|- ( O e. OutMeas -> S C_ dom O ) |
6 |
1 5
|
syl |
|- ( ph -> S C_ dom O ) |
7 |
6
|
unissd |
|- ( ph -> U. S C_ U. dom O ) |
8 |
7
|
ssdifssd |
|- ( ph -> ( U. S \ E ) C_ U. dom O ) |
9 |
2
|
fvexi |
|- S e. _V |
10 |
9
|
uniex |
|- U. S e. _V |
11 |
|
difexg |
|- ( U. S e. _V -> ( U. S \ E ) e. _V ) |
12 |
10 11
|
ax-mp |
|- ( U. S \ E ) e. _V |
13 |
12
|
a1i |
|- ( ph -> ( U. S \ E ) e. _V ) |
14 |
|
elpwg |
|- ( ( U. S \ E ) e. _V -> ( ( U. S \ E ) e. ~P U. dom O <-> ( U. S \ E ) C_ U. dom O ) ) |
15 |
13 14
|
syl |
|- ( ph -> ( ( U. S \ E ) e. ~P U. dom O <-> ( U. S \ E ) C_ U. dom O ) ) |
16 |
8 15
|
mpbird |
|- ( ph -> ( U. S \ E ) e. ~P U. dom O ) |
17 |
|
elpwi |
|- ( a e. ~P U. dom O -> a C_ U. dom O ) |
18 |
17
|
adantl |
|- ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. dom O ) |
19 |
1 2
|
caragenuni |
|- ( ph -> U. S = U. dom O ) |
20 |
19
|
eqcomd |
|- ( ph -> U. dom O = U. S ) |
21 |
20
|
adantr |
|- ( ( ph /\ a e. ~P U. dom O ) -> U. dom O = U. S ) |
22 |
18 21
|
sseqtrd |
|- ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. S ) |
23 |
|
difin2 |
|- ( a C_ U. S -> ( a \ E ) = ( ( U. S \ E ) i^i a ) ) |
24 |
22 23
|
syl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ E ) = ( ( U. S \ E ) i^i a ) ) |
25 |
|
incom |
|- ( ( U. S \ E ) i^i a ) = ( a i^i ( U. S \ E ) ) |
26 |
25
|
a1i |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( U. S \ E ) i^i a ) = ( a i^i ( U. S \ E ) ) ) |
27 |
24 26
|
eqtr2d |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i ( U. S \ E ) ) = ( a \ E ) ) |
28 |
27
|
fveq2d |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i ( U. S \ E ) ) ) = ( O ` ( a \ E ) ) ) |
29 |
22
|
ssdifd |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ E ) C_ ( U. S \ E ) ) |
30 |
|
sscon |
|- ( ( a \ E ) C_ ( U. S \ E ) -> ( a \ ( U. S \ E ) ) C_ ( a \ ( a \ E ) ) ) |
31 |
29 30
|
syl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( U. S \ E ) ) C_ ( a \ ( a \ E ) ) ) |
32 |
|
dfin4 |
|- ( a i^i E ) = ( a \ ( a \ E ) ) |
33 |
32
|
a1i |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i E ) = ( a \ ( a \ E ) ) ) |
34 |
|
eqimss2 |
|- ( ( a i^i E ) = ( a \ ( a \ E ) ) -> ( a \ ( a \ E ) ) C_ ( a i^i E ) ) |
35 |
33 34
|
syl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( a \ E ) ) C_ ( a i^i E ) ) |
36 |
31 35
|
sstrd |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( U. S \ E ) ) C_ ( a i^i E ) ) |
37 |
|
elinel1 |
|- ( x e. ( a i^i E ) -> x e. a ) |
38 |
|
elinel2 |
|- ( x e. ( a i^i E ) -> x e. E ) |
39 |
|
elndif |
|- ( x e. E -> -. x e. ( U. S \ E ) ) |
40 |
38 39
|
syl |
|- ( x e. ( a i^i E ) -> -. x e. ( U. S \ E ) ) |
41 |
37 40
|
eldifd |
|- ( x e. ( a i^i E ) -> x e. ( a \ ( U. S \ E ) ) ) |
42 |
41
|
ssriv |
|- ( a i^i E ) C_ ( a \ ( U. S \ E ) ) |
43 |
42
|
a1i |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i E ) C_ ( a \ ( U. S \ E ) ) ) |
44 |
36 43
|
eqssd |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ ( U. S \ E ) ) = ( a i^i E ) ) |
45 |
44
|
fveq2d |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ ( U. S \ E ) ) ) = ( O ` ( a i^i E ) ) ) |
46 |
28 45
|
oveq12d |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i ( U. S \ E ) ) ) +e ( O ` ( a \ ( U. S \ E ) ) ) ) = ( ( O ` ( a \ E ) ) +e ( O ` ( a i^i E ) ) ) ) |
47 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
48 |
1
|
adantr |
|- ( ( ph /\ a e. ~P U. dom O ) -> O e. OutMeas ) |
49 |
18
|
ssdifssd |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ E ) C_ U. dom O ) |
50 |
48 4 49
|
omecl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ E ) ) e. ( 0 [,] +oo ) ) |
51 |
47 50
|
sselid |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ E ) ) e. RR* ) |
52 |
|
ssinss1 |
|- ( a C_ U. dom O -> ( a i^i E ) C_ U. dom O ) |
53 |
17 52
|
syl |
|- ( a e. ~P U. dom O -> ( a i^i E ) C_ U. dom O ) |
54 |
53
|
adantl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i E ) C_ U. dom O ) |
55 |
48 4 54
|
omecl |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i E ) ) e. ( 0 [,] +oo ) ) |
56 |
47 55
|
sselid |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i E ) ) e. RR* ) |
57 |
51 56
|
xaddcomd |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a \ E ) ) +e ( O ` ( a i^i E ) ) ) = ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) ) |
58 |
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 ) ) ) ) |
59 |
3 58
|
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 ) ) ) |
60 |
59
|
simprd |
|- ( ph -> A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) |
61 |
60
|
r19.21bi |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) |
62 |
46 57 61
|
3eqtrd |
|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i ( U. S \ E ) ) ) +e ( O ` ( a \ ( U. S \ E ) ) ) ) = ( O ` a ) ) |
63 |
1 4 2 16 62
|
carageneld |
|- ( ph -> ( U. S \ E ) e. S ) |