Step |
Hyp |
Ref |
Expression |
1 |
|
vonvolmbllem.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
2 |
|
vonvolmbllem.b |
⊢ ( 𝜑 → 𝐵 ⊆ ℝ ) |
3 |
|
vonvolmbllem.e |
⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) |
4 |
|
vonvolmbllem.x |
⊢ ( 𝜑 → 𝑋 ⊆ ( ℝ ↑m { 𝐴 } ) ) |
5 |
|
vonvolmbllem.y |
⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓 |
6 |
|
nfcv |
⊢ Ⅎ 𝑓 𝑌 |
7 |
6 1 4 5
|
ssmapsn |
⊢ ( 𝜑 → 𝑋 = ( 𝑌 ↑m { 𝐴 } ) ) |
8 |
7
|
ineq1d |
⊢ ( 𝜑 → ( 𝑋 ∩ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑌 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) |
9 |
|
reex |
⊢ ℝ ∈ V |
10 |
9
|
a1i |
⊢ ( 𝜑 → ℝ ∈ V ) |
11 |
4
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) ) |
12 |
|
elmapi |
⊢ ( 𝑓 ∈ ( ℝ ↑m { 𝐴 } ) → 𝑓 : { 𝐴 } ⟶ ℝ ) |
13 |
11 12
|
syl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 : { 𝐴 } ⟶ ℝ ) |
14 |
13
|
frnd |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ran 𝑓 ⊆ ℝ ) |
15 |
14
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ ) |
16 |
|
iunss |
⊢ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ ↔ ∀ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ ) |
17 |
15 16
|
sylibr |
⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⊆ ℝ ) |
18 |
5 17
|
eqsstrid |
⊢ ( 𝜑 → 𝑌 ⊆ ℝ ) |
19 |
10 18
|
ssexd |
⊢ ( 𝜑 → 𝑌 ∈ V ) |
20 |
10 2
|
ssexd |
⊢ ( 𝜑 → 𝐵 ∈ V ) |
21 |
|
snex |
⊢ { 𝐴 } ∈ V |
22 |
21
|
a1i |
⊢ ( 𝜑 → { 𝐴 } ∈ V ) |
23 |
19 20 22
|
inmap |
⊢ ( 𝜑 → ( ( 𝑌 ↑m { 𝐴 } ) ∩ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑌 ∩ 𝐵 ) ↑m { 𝐴 } ) ) |
24 |
8 23
|
eqtrd |
⊢ ( 𝜑 → ( 𝑋 ∩ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑌 ∩ 𝐵 ) ↑m { 𝐴 } ) ) |
25 |
24
|
fveq2d |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌 ∩ 𝐵 ) ↑m { 𝐴 } ) ) ) |
26 |
18
|
ssinss1d |
⊢ ( 𝜑 → ( 𝑌 ∩ 𝐵 ) ⊆ ℝ ) |
27 |
1 26
|
ovnovol |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌 ∩ 𝐵 ) ↑m { 𝐴 } ) ) = ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) ) |
28 |
25 27
|
eqtrd |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) = ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) ) |
29 |
7
|
difeq1d |
⊢ ( 𝜑 → ( 𝑋 ∖ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑌 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) |
30 |
19 20 1
|
difmapsn |
⊢ ( 𝜑 → ( ( 𝑌 ↑m { 𝐴 } ) ∖ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑌 ∖ 𝐵 ) ↑m { 𝐴 } ) ) |
31 |
29 30
|
eqtrd |
⊢ ( 𝜑 → ( 𝑋 ∖ ( 𝐵 ↑m { 𝐴 } ) ) = ( ( 𝑌 ∖ 𝐵 ) ↑m { 𝐴 } ) ) |
32 |
31
|
fveq2d |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌 ∖ 𝐵 ) ↑m { 𝐴 } ) ) ) |
33 |
18
|
ssdifssd |
⊢ ( 𝜑 → ( 𝑌 ∖ 𝐵 ) ⊆ ℝ ) |
34 |
1 33
|
ovnovol |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( ( 𝑌 ∖ 𝐵 ) ↑m { 𝐴 } ) ) = ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) |
35 |
32 34
|
eqtrd |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) = ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) |
36 |
28 35
|
oveq12d |
⊢ ( 𝜑 → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) ) |
37 |
7
|
fveq2d |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ 𝑋 ) = ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑌 ↑m { 𝐴 } ) ) ) |
38 |
1 18
|
ovnovol |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑌 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝑌 ) ) |
39 |
19 18
|
elpwd |
⊢ ( 𝜑 → 𝑌 ∈ 𝒫 ℝ ) |
40 |
|
fveq2 |
⊢ ( 𝑦 = 𝑌 → ( vol* ‘ 𝑦 ) = ( vol* ‘ 𝑌 ) ) |
41 |
|
ineq1 |
⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∩ 𝐵 ) = ( 𝑌 ∩ 𝐵 ) ) |
42 |
41
|
fveq2d |
⊢ ( 𝑦 = 𝑌 → ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) = ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) ) |
43 |
|
difeq1 |
⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∖ 𝐵 ) = ( 𝑌 ∖ 𝐵 ) ) |
44 |
43
|
fveq2d |
⊢ ( 𝑦 = 𝑌 → ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) = ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) |
45 |
42 44
|
oveq12d |
⊢ ( 𝑦 = 𝑌 → ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) = ( ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) ) |
46 |
40 45
|
eqeq12d |
⊢ ( 𝑦 = 𝑌 → ( ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ↔ ( vol* ‘ 𝑌 ) = ( ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) ) ) |
47 |
46
|
rspcva |
⊢ ( ( 𝑌 ∈ 𝒫 ℝ ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑦 ∖ 𝐵 ) ) ) ) → ( vol* ‘ 𝑌 ) = ( ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) ) |
48 |
39 3 47
|
syl2anc |
⊢ ( 𝜑 → ( vol* ‘ 𝑌 ) = ( ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) ) |
49 |
37 38 48
|
3eqtrd |
⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ 𝑋 ) = ( ( vol* ‘ ( 𝑌 ∩ 𝐵 ) ) +𝑒 ( vol* ‘ ( 𝑌 ∖ 𝐵 ) ) ) ) |
50 |
36 49
|
eqtr4d |
⊢ ( 𝜑 → ( ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∩ ( 𝐵 ↑m { 𝐴 } ) ) ) +𝑒 ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝑋 ∖ ( 𝐵 ↑m { 𝐴 } ) ) ) ) = ( ( voln* ‘ { 𝐴 } ) ‘ 𝑋 ) ) |