Step |
Hyp |
Ref |
Expression |
1 |
|
ovnhoilem2.x |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
2 |
|
ovnhoilem2.n |
⊢ ( 𝜑 → 𝑋 ≠ ∅ ) |
3 |
|
ovnhoilem2.a |
⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ ) |
4 |
|
ovnhoilem2.b |
⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ ) |
5 |
|
ovnhoilem2.i |
⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) |
6 |
|
ovnhoilem2.l |
⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) |
7 |
|
ovnhoilem2.m |
⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } |
8 |
|
ovnhoilem2.f |
⊢ 𝐹 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
9 |
|
ovnhoilem2.s |
⊢ 𝑆 = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
10 |
7
|
eleq2i |
⊢ ( 𝑧 ∈ 𝑀 ↔ 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ) |
11 |
|
rabid |
⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ↔ ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) ) |
12 |
10 11
|
bitri |
⊢ ( 𝑧 ∈ 𝑀 ↔ ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) ) |
13 |
12
|
biimpi |
⊢ ( 𝑧 ∈ 𝑀 → ( 𝑧 ∈ ℝ* ∧ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) ) |
14 |
13
|
simprd |
⊢ ( 𝑧 ∈ 𝑀 → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) |
15 |
14
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) |
16 |
1
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑋 ∈ Fin ) |
17 |
3
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐴 : 𝑋 ⟶ ℝ ) |
18 |
4
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐵 : 𝑋 ⟶ ℝ ) |
19 |
|
elmapi |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑖 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) |
20 |
19
|
ffvelrnda |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ‘ 𝑛 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) |
21 |
|
elmapi |
⊢ ( ( 𝑖 ‘ 𝑛 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝑖 ‘ 𝑛 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) |
22 |
20 21
|
syl |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ‘ 𝑛 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) |
23 |
22
|
ffvelrnda |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) ) |
24 |
|
xp1st |
⊢ ( ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ ) |
25 |
23 24
|
syl |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ ) |
26 |
25
|
fmpttd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) |
27 |
|
reex |
⊢ ℝ ∈ V |
28 |
27
|
a1i |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ℝ ∈ V ) |
29 |
|
1nn |
⊢ 1 ∈ ℕ |
30 |
29
|
a1i |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 1 ∈ ℕ ) |
31 |
19 30
|
ffvelrnd |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑖 ‘ 1 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) |
32 |
|
elmapex |
⊢ ( ( 𝑖 ‘ 1 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( ( ℝ × ℝ ) ∈ V ∧ 𝑋 ∈ V ) ) |
33 |
32
|
simprd |
⊢ ( ( 𝑖 ‘ 1 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → 𝑋 ∈ V ) |
34 |
31 33
|
syl |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑋 ∈ V ) |
35 |
34
|
adantr |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ V ) |
36 |
|
elmapg |
⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ V ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) ) |
37 |
28 35 36
|
syl2anc |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) ) |
38 |
26 37
|
mpbird |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ) |
39 |
38
|
fmpttd |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
40 |
|
id |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) |
41 |
|
nnex |
⊢ ℕ ∈ V |
42 |
41
|
mptex |
⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V |
43 |
42
|
a1i |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) |
44 |
8
|
fvmpt2 |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
45 |
40 43 44
|
syl2anc |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
46 |
45
|
feq1d |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐹 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ↔ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) ) |
47 |
39 46
|
mpbird |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝐹 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
48 |
47
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐹 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
49 |
|
xp2nd |
⊢ ( ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ ) |
50 |
23 49
|
syl |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ ) |
51 |
50
|
fmpttd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) |
52 |
|
elmapg |
⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ V ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) ) |
53 |
28 35 52
|
syl2anc |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ↔ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) ) |
54 |
51 53
|
mpbird |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ ( ℝ ↑m 𝑋 ) ) |
55 |
54
|
fmpttd |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
56 |
41
|
mptex |
⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V |
57 |
56
|
a1i |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) |
58 |
9
|
fvmpt2 |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) → ( 𝑆 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
59 |
40 57 58
|
syl2anc |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑆 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
60 |
59
|
feq1d |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝑆 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ↔ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) ) |
61 |
55 60
|
mpbird |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑆 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
62 |
61
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝑆 ‘ 𝑖 ) : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
63 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) |
64 |
5
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |
65 |
|
fveq2 |
⊢ ( 𝑗 = 𝑛 → ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ 𝑛 ) ) |
66 |
65
|
fveq1d |
⊢ ( 𝑗 = 𝑛 → ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) = ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) |
67 |
66
|
fveq2d |
⊢ ( 𝑗 = 𝑛 → ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
68 |
66
|
fveq2d |
⊢ ( 𝑗 = 𝑛 → ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
69 |
67 68
|
oveq12d |
⊢ ( 𝑗 = 𝑛 → ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ( ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) ) |
70 |
69
|
ixpeq2dv |
⊢ ( 𝑗 = 𝑛 → X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) ) |
71 |
70
|
cbviunv |
⊢ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
72 |
71
|
a1i |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) ) |
73 |
19
|
ffvelrnda |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑖 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ) |
74 |
|
elmapi |
⊢ ( ( 𝑖 ‘ 𝑗 ) ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) → ( 𝑖 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) |
75 |
73 74
|
syl |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑖 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) |
76 |
75
|
adantr |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑖 ‘ 𝑗 ) : 𝑋 ⟶ ( ℝ × ℝ ) ) |
77 |
|
simpr |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 ) |
78 |
76 77
|
fvovco |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) |
79 |
78
|
ixpeq2dva |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) |
80 |
79
|
iuneq2dv |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) |
81 |
|
simpl |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) |
82 |
42
|
a1i |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ∈ V ) |
83 |
81 82 44
|
syl2anc |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
84 |
83
|
fveq1d |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) ) |
85 |
|
simpr |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ ) |
86 |
|
mptexg |
⊢ ( 𝑋 ∈ V → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) |
87 |
34 86
|
syl |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) |
88 |
87
|
adantr |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) |
89 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
90 |
89
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
91 |
85 88 90
|
syl2anc |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
92 |
84 91
|
eqtrd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
93 |
92
|
fveq1d |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
94 |
93
|
adantr |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
95 |
|
eqidd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
96 |
|
simpr |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → 𝑙 = 𝑘 ) |
97 |
96
|
fveq2d |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) = ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) |
98 |
97
|
fveq2d |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
99 |
|
simpr |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 ) |
100 |
|
fvexd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ∈ V ) |
101 |
95 98 99 100
|
fvmptd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
102 |
101
|
adantlr |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
103 |
94 102
|
eqtrd |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
104 |
59
|
fveq1d |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) ) |
105 |
104
|
adantr |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) ) |
106 |
|
mptexg |
⊢ ( 𝑋 ∈ V → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) |
107 |
34 106
|
syl |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) |
108 |
107
|
adantr |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) |
109 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
110 |
109
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
111 |
85 108 110
|
syl2anc |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
112 |
105 111
|
eqtrd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
113 |
112
|
fveq1d |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
114 |
113
|
adantr |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
115 |
|
eqidd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
116 |
|
2fveq3 |
⊢ ( 𝑙 = 𝑘 → ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
117 |
116
|
adantl |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑙 = 𝑘 ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
118 |
|
fvexd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ∈ V ) |
119 |
115 117 99 118
|
fvmptd |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
120 |
119
|
adantlr |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
121 |
114 120
|
eqtrd |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
122 |
103 121
|
oveq12d |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = ( ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) ) |
123 |
122
|
ixpeq2dva |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) ) |
124 |
123
|
iuneq2dv |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑘 ) ) ) ) |
125 |
72 80 124
|
3eqtr4d |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
126 |
125
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
127 |
126
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
128 |
64 127
|
sseq12d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) ) ) |
129 |
63 128
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
130 |
129
|
3adant3r |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) [,) ( ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ‘ 𝑘 ) ) ) |
131 |
6 16 17 18 48 62 130
|
hoidmvle |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) ) |
132 |
|
simpl |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋 ) → 𝑛 = 𝑗 ) |
133 |
132
|
fveq2d |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋 ) → ( 𝑖 ‘ 𝑛 ) = ( 𝑖 ‘ 𝑗 ) ) |
134 |
133
|
fveq1d |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋 ) → ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) = ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) |
135 |
134
|
fveq2d |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) |
136 |
135
|
mpteq2dva |
⊢ ( 𝑛 = 𝑗 → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) |
137 |
136
|
fveq1d |
⊢ ( 𝑛 = 𝑗 → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
138 |
137
|
adantr |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
139 |
|
eqidd |
⊢ ( 𝑘 ∈ 𝑋 → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) |
140 |
|
2fveq3 |
⊢ ( 𝑙 = 𝑘 → ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
141 |
140
|
adantl |
⊢ ( ( 𝑘 ∈ 𝑋 ∧ 𝑙 = 𝑘 ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
142 |
|
id |
⊢ ( 𝑘 ∈ 𝑋 → 𝑘 ∈ 𝑋 ) |
143 |
|
fvexd |
⊢ ( 𝑘 ∈ 𝑋 → ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ∈ V ) |
144 |
139 141 142 143
|
fvmptd |
⊢ ( 𝑘 ∈ 𝑋 → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
145 |
144
|
adantl |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
146 |
138 145
|
eqtrd |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
147 |
134
|
fveq2d |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) |
148 |
147
|
mpteq2dva |
⊢ ( 𝑛 = 𝑗 → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) |
149 |
148
|
fveq1d |
⊢ ( 𝑛 = 𝑗 → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
150 |
149
|
adantr |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) |
151 |
|
eqidd |
⊢ ( 𝑘 ∈ 𝑋 → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) |
152 |
|
2fveq3 |
⊢ ( 𝑙 = 𝑘 → ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
153 |
152
|
adantl |
⊢ ( ( 𝑘 ∈ 𝑋 ∧ 𝑙 = 𝑘 ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
154 |
|
fvexd |
⊢ ( 𝑘 ∈ 𝑋 → ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ∈ V ) |
155 |
151 153 142 154
|
fvmptd |
⊢ ( 𝑘 ∈ 𝑋 → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
156 |
155
|
adantl |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
157 |
150 156
|
eqtrd |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
158 |
146 157
|
oveq12d |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) = ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) |
159 |
158
|
fveq2d |
⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) |
160 |
159
|
prodeq2dv |
⊢ ( 𝑛 = 𝑗 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) |
161 |
160
|
cbvmptv |
⊢ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) |
162 |
161
|
a1i |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) ) |
163 |
78
|
eqcomd |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) |
164 |
163
|
fveq2d |
⊢ ( ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) |
165 |
164
|
prodeq2dv |
⊢ ( ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) |
166 |
165
|
mpteq2dva |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) [,) ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) |
167 |
162 166
|
eqtrd |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) |
168 |
167
|
fveq2d |
⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) |
169 |
168
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) |
170 |
92
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
171 |
112
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) |
172 |
170 171
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) = ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ( 𝐿 ‘ 𝑋 ) ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) ) |
173 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin ) |
174 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ≠ ∅ ) |
175 |
23
|
adantlll |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ∈ ( ℝ × ℝ ) ) |
176 |
175 24
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ ) |
177 |
176
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) |
178 |
175 49
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ∈ ℝ ) |
179 |
178
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) : 𝑋 ⟶ ℝ ) |
180 |
6 173 174 177 179
|
hoidmvn0val |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ( 𝐿 ‘ 𝑋 ) ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) |
181 |
172 180
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) |
182 |
181
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) |
183 |
182
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) ) |
184 |
183
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) [,) ( ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ‘ 𝑘 ) ) ) ) ) ) |
185 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) |
186 |
169 184 185
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) = 𝑧 ) |
187 |
186
|
3adant3l |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑛 ) ( 𝐿 ‘ 𝑋 ) ( ( 𝑆 ‘ 𝑖 ) ‘ 𝑛 ) ) ) ) = 𝑧 ) |
188 |
131 187
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) |
189 |
188
|
3exp |
⊢ ( 𝜑 → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) ) ) |
190 |
189
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) ) ) |
191 |
190
|
rexlimdv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) ) |
192 |
15 191
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) |
193 |
192
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑀 ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) |
194 |
|
ssrab2 |
⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ* |
195 |
7 194
|
eqsstri |
⊢ 𝑀 ⊆ ℝ* |
196 |
195
|
a1i |
⊢ ( 𝜑 → 𝑀 ⊆ ℝ* ) |
197 |
|
icossxr |
⊢ ( 0 [,) +∞ ) ⊆ ℝ* |
198 |
6 1 3 4
|
hoidmvcl |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ( 0 [,) +∞ ) ) |
199 |
197 198
|
sseldi |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ℝ* ) |
200 |
|
infxrgelb |
⊢ ( ( 𝑀 ⊆ ℝ* ∧ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ℝ* ) → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ inf ( 𝑀 , ℝ* , < ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) ) |
201 |
196 199 200
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ inf ( 𝑀 , ℝ* , < ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ 𝑧 ) ) |
202 |
193 201
|
mpbird |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ inf ( 𝑀 , ℝ* , < ) ) |
203 |
5
|
a1i |
⊢ ( 𝜑 → 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |
204 |
|
nfv |
⊢ Ⅎ 𝑘 𝜑 |
205 |
3
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ ) |
206 |
4
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) |
207 |
206
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) |
208 |
204 205 207
|
hoissrrn2 |
⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) ) |
209 |
203 208
|
eqsstrd |
⊢ ( 𝜑 → 𝐼 ⊆ ( ℝ ↑m 𝑋 ) ) |
210 |
1 2 209 7
|
ovnn0val |
⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = inf ( 𝑀 , ℝ* , < ) ) |
211 |
210
|
eqcomd |
⊢ ( 𝜑 → inf ( 𝑀 , ℝ* , < ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ) |
212 |
202 211
|
breqtrd |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ) |