Step |
Hyp |
Ref |
Expression |
1 |
|
i1f1.1 |
⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) |
2 |
|
ovol0 |
⊢ ( vol* ‘ ∅ ) = 0 |
3 |
|
0mbl |
⊢ ∅ ∈ dom vol |
4 |
|
mblvol |
⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) ) |
5 |
3 4
|
ax-mp |
⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) |
6 |
|
itg10 |
⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = 0 |
7 |
2 5 6
|
3eqtr4ri |
⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = ( vol ‘ ∅ ) |
8 |
|
noel |
⊢ ¬ 𝑥 ∈ ∅ |
9 |
|
eleq2 |
⊢ ( 𝐴 = ∅ → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ∅ ) ) |
10 |
8 9
|
mtbiri |
⊢ ( 𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴 ) |
11 |
10
|
iffalsed |
⊢ ( 𝐴 = ∅ → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = 0 ) |
12 |
11
|
mpteq2dv |
⊢ ( 𝐴 = ∅ → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) ) |
13 |
|
fconstmpt |
⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 ) |
14 |
12 1 13
|
3eqtr4g |
⊢ ( 𝐴 = ∅ → 𝐹 = ( ℝ × { 0 } ) ) |
15 |
14
|
fveq2d |
⊢ ( 𝐴 = ∅ → ( ∫1 ‘ 𝐹 ) = ( ∫1 ‘ ( ℝ × { 0 } ) ) ) |
16 |
|
fveq2 |
⊢ ( 𝐴 = ∅ → ( vol ‘ 𝐴 ) = ( vol ‘ ∅ ) ) |
17 |
7 15 16
|
3eqtr4a |
⊢ ( 𝐴 = ∅ → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) |
18 |
17
|
a1i |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 = ∅ → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) ) |
19 |
|
n0 |
⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 ) |
20 |
1
|
i1f1 |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 ∈ dom ∫1 ) |
21 |
20
|
adantr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝐹 ∈ dom ∫1 ) |
22 |
|
itg1val |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) ) |
23 |
21 22
|
syl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ∫1 ‘ 𝐹 ) = Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) ) |
24 |
1
|
i1f1lem |
⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) ) |
25 |
24
|
simpli |
⊢ 𝐹 : ℝ ⟶ { 0 , 1 } |
26 |
|
frn |
⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } → ran 𝐹 ⊆ { 0 , 1 } ) |
27 |
25 26
|
ax-mp |
⊢ ran 𝐹 ⊆ { 0 , 1 } |
28 |
|
ssdif |
⊢ ( ran 𝐹 ⊆ { 0 , 1 } → ( ran 𝐹 ∖ { 0 } ) ⊆ ( { 0 , 1 } ∖ { 0 } ) ) |
29 |
27 28
|
ax-mp |
⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ( { 0 , 1 } ∖ { 0 } ) |
30 |
|
difprsnss |
⊢ ( { 0 , 1 } ∖ { 0 } ) ⊆ { 1 } |
31 |
29 30
|
sstri |
⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ { 1 } |
32 |
31
|
a1i |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ran 𝐹 ∖ { 0 } ) ⊆ { 1 } ) |
33 |
|
mblss |
⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ ) |
34 |
33
|
adantr |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐴 ⊆ ℝ ) |
35 |
34
|
sselda |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ ) |
36 |
|
eleq1w |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) |
37 |
36
|
ifbid |
⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) ) |
38 |
|
1ex |
⊢ 1 ∈ V |
39 |
|
c0ex |
⊢ 0 ∈ V |
40 |
38 39
|
ifex |
⊢ if ( 𝑦 ∈ 𝐴 , 1 , 0 ) ∈ V |
41 |
37 1 40
|
fvmpt |
⊢ ( 𝑦 ∈ ℝ → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) ) |
42 |
35 41
|
syl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) ) |
43 |
|
iftrue |
⊢ ( 𝑦 ∈ 𝐴 → if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 ) |
44 |
43
|
adantl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 ) |
45 |
42 44
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = 1 ) |
46 |
|
ffn |
⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } → 𝐹 Fn ℝ ) |
47 |
25 46
|
ax-mp |
⊢ 𝐹 Fn ℝ |
48 |
|
fnfvelrn |
⊢ ( ( 𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 ) |
49 |
47 35 48
|
sylancr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 ) |
50 |
45 49
|
eqeltrrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 1 ∈ ran 𝐹 ) |
51 |
|
ax-1ne0 |
⊢ 1 ≠ 0 |
52 |
|
eldifsn |
⊢ ( 1 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ ( 1 ∈ ran 𝐹 ∧ 1 ≠ 0 ) ) |
53 |
50 51 52
|
sylanblrc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 1 ∈ ( ran 𝐹 ∖ { 0 } ) ) |
54 |
53
|
snssd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → { 1 } ⊆ ( ran 𝐹 ∖ { 0 } ) ) |
55 |
32 54
|
eqssd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ran 𝐹 ∖ { 0 } ) = { 1 } ) |
56 |
55
|
sumeq1d |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) ) |
57 |
|
1re |
⊢ 1 ∈ ℝ |
58 |
24
|
simpri |
⊢ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) |
59 |
58
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) |
60 |
59
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) = ( vol ‘ 𝐴 ) ) |
61 |
60
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) = ( 1 · ( vol ‘ 𝐴 ) ) ) |
62 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( vol ‘ 𝐴 ) ∈ ℝ ) |
63 |
62
|
recnd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( vol ‘ 𝐴 ) ∈ ℂ ) |
64 |
63
|
mulid2d |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ 𝐴 ) ) = ( vol ‘ 𝐴 ) ) |
65 |
61 64
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) = ( vol ‘ 𝐴 ) ) |
66 |
65 63
|
eqeltrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) ∈ ℂ ) |
67 |
|
id |
⊢ ( 𝑧 = 1 → 𝑧 = 1 ) |
68 |
|
sneq |
⊢ ( 𝑧 = 1 → { 𝑧 } = { 1 } ) |
69 |
68
|
imaeq2d |
⊢ ( 𝑧 = 1 → ( ◡ 𝐹 “ { 𝑧 } ) = ( ◡ 𝐹 “ { 1 } ) ) |
70 |
69
|
fveq2d |
⊢ ( 𝑧 = 1 → ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) = ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) |
71 |
67 70
|
oveq12d |
⊢ ( 𝑧 = 1 → ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) ) |
72 |
71
|
sumsn |
⊢ ( ( 1 ∈ ℝ ∧ ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) ∈ ℂ ) → Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) ) |
73 |
57 66 72
|
sylancr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) ) |
74 |
73 65
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( vol ‘ 𝐴 ) ) |
75 |
56 74
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( vol ‘ 𝐴 ) ) |
76 |
23 75
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) |
77 |
76
|
ex |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝑦 ∈ 𝐴 → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) ) |
78 |
77
|
exlimdv |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∃ 𝑦 𝑦 ∈ 𝐴 → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) ) |
79 |
19 78
|
syl5bi |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 ≠ ∅ → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) ) |
80 |
18 79
|
pm2.61dne |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) |