Step | Hyp | Ref
| Expression |
1 | | ovolval5lem3.q |
. . . . 5
β’ π = {π§ β β* β£
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π)))} |
2 | 1 | ssrab3 4041 |
. . . 4
β’ π β
β* |
3 | | infxrcl 13258 |
. . . 4
β’ (π β β*
β inf(π,
β*, < ) β β*) |
4 | 2, 3 | mp1i 13 |
. . 3
β’ (β€
β inf(π,
β*, < ) β β*) |
5 | | ovolval5lem3.m |
. . . . 5
β’ π = {π¦ β β* β£
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))} |
6 | 5 | ssrab3 4041 |
. . . 4
β’ π β
β* |
7 | | infxrcl 13258 |
. . . 4
β’ (π β β*
β inf(π,
β*, < ) β β*) |
8 | 6, 7 | mp1i 13 |
. . 3
β’ (β€
β inf(π,
β*, < ) β β*) |
9 | 2 | a1i 11 |
. . . 4
β’ (β€
β π β
β*) |
10 | 6 | a1i 11 |
. . . 4
β’ (β€
β π β
β*) |
11 | 5 | reqabi 3428 |
. . . . . . 7
β’ (π¦ β π β (π¦ β β* β§
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π))))) |
12 | 11 | simprbi 498 |
. . . . . 6
β’ (π¦ β π β βπ β ((β Γ β)
βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) |
13 | | coeq2 5815 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((,) β π) = ((,) β π)) |
14 | 13 | rneqd 5894 |
. . . . . . . . . . . . . 14
β’ (π = π β ran ((,) β π) = ran ((,) β π)) |
15 | 14 | unieqd 4880 |
. . . . . . . . . . . . 13
β’ (π = π β βͺ ran ((,)
β π) = βͺ ran ((,) β π)) |
16 | 15 | sseq2d 3977 |
. . . . . . . . . . . 12
β’ (π = π β (π΄ β βͺ ran
((,) β π) β
π΄ β βͺ ran ((,) β π))) |
17 | | coeq2 5815 |
. . . . . . . . . . . . . 14
β’ (π = π β ((vol β (,)) β π) = ((vol β (,)) β
π)) |
18 | 17 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π = π β
(Ξ£^β((vol β (,)) β π)) =
(Ξ£^β((vol β (,)) β π))) |
19 | 18 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = π β (π§ =
(Ξ£^β((vol β (,)) β π)) β π§ =
(Ξ£^β((vol β (,)) β π)))) |
20 | 16, 19 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = π β ((π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π))) β (π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π))))) |
21 | 20 | cbvrexvw 3225 |
. . . . . . . . . 10
β’
(βπ β
((β Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π))) β βπ β ((β Γ
β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π)))) |
22 | 21 | rabbii 3412 |
. . . . . . . . 9
β’ {π§ β β*
β£ βπ β
((β Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π)))} = {π§ β β* β£
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π)))} |
23 | 1, 22 | eqtr4i 2764 |
. . . . . . . 8
β’ π = {π§ β β* β£
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π)))} |
24 | | simp3r 1203 |
. . . . . . . 8
β’ ((π€ β β+
β§ π β ((β
Γ β) βm β) β§ (π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) β π¦ =
(Ξ£^β((vol β [,)) β π))) |
25 | | eqid 2733 |
. . . . . . . 8
β’
(Ξ£^β((vol β (,)) β
(π β β β¦
β¨((1st β(πβπ)) β (π€ / (2βπ))), (2nd β(πβπ))β©))) =
(Ξ£^β((vol β (,)) β (π β β β¦
β¨((1st β(πβπ)) β (π€ / (2βπ))), (2nd β(πβπ))β©))) |
26 | | elmapi 8790 |
. . . . . . . . 9
β’ (π β ((β Γ
β) βm β) β π:ββΆ(β Γ
β)) |
27 | 26 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π€ β β+
β§ π β ((β
Γ β) βm β) β§ (π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) β π:ββΆ(β Γ
β)) |
28 | | simp3l 1202 |
. . . . . . . 8
β’ ((π€ β β+
β§ π β ((β
Γ β) βm β) β§ (π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) β π΄ β βͺ ran
([,) β π)) |
29 | | simp1 1137 |
. . . . . . . 8
β’ ((π€ β β+
β§ π β ((β
Γ β) βm β) β§ (π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) β π€ β β+) |
30 | | 2fveq3 6848 |
. . . . . . . . . . 11
β’ (π = π β (1st β(πβπ)) = (1st β(πβπ))) |
31 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π = π β (2βπ) = (2βπ)) |
32 | 31 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = π β (π€ / (2βπ)) = (π€ / (2βπ))) |
33 | 30, 32 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π = π β ((1st β(πβπ)) β (π€ / (2βπ))) = ((1st β(πβπ)) β (π€ / (2βπ)))) |
34 | | 2fveq3 6848 |
. . . . . . . . . 10
β’ (π = π β (2nd β(πβπ)) = (2nd β(πβπ))) |
35 | 33, 34 | opeq12d 4839 |
. . . . . . . . 9
β’ (π = π β β¨((1st β(πβπ)) β (π€ / (2βπ))), (2nd β(πβπ))β© = β¨((1st
β(πβπ)) β (π€ / (2βπ))), (2nd β(πβπ))β©) |
36 | 35 | cbvmptv 5219 |
. . . . . . . 8
β’ (π β β β¦
β¨((1st β(πβπ)) β (π€ / (2βπ))), (2nd β(πβπ))β©) = (π β β β¦
β¨((1st β(πβπ)) β (π€ / (2βπ))), (2nd β(πβπ))β©) |
37 | 23, 24, 25, 27, 28, 29, 36 | ovolval5lem2 44980 |
. . . . . . 7
β’ ((π€ β β+
β§ π β ((β
Γ β) βm β) β§ (π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) β βπ§ β π π§ β€ (π¦ +π π€)) |
38 | 37 | rexlimdv3a 3153 |
. . . . . 6
β’ (π€ β β+
β (βπ β
((β Γ β) βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π))) β βπ§ β π π§ β€ (π¦ +π π€))) |
39 | 12, 38 | mpan9 508 |
. . . . 5
β’ ((π¦ β π β§ π€ β β+) β
βπ§ β π π§ β€ (π¦ +π π€)) |
40 | 39 | 3adant1 1131 |
. . . 4
β’
((β€ β§ π¦
β π β§ π€ β β+)
β βπ§ β
π π§ β€ (π¦ +π π€)) |
41 | 9, 10, 40 | infleinf 43693 |
. . 3
β’ (β€
β inf(π,
β*, < ) β€ inf(π, β*, <
)) |
42 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π§ = π¦ β (π§ =
(Ξ£^β((vol β (,)) β π)) β π¦ =
(Ξ£^β((vol β (,)) β π)))) |
43 | 42 | anbi2d 630 |
. . . . . . . . 9
β’ (π§ = π¦ β ((π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π))) β (π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π))))) |
44 | 43 | rexbidv 3172 |
. . . . . . . 8
β’ (π§ = π¦ β (βπ β ((β Γ β)
βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π))) β βπ β ((β Γ
β) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π))))) |
45 | 44 | cbvrabv 3416 |
. . . . . . 7
β’ {π§ β β*
β£ βπ β
((β Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π)))} = {π¦ β β* β£
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π)))} |
46 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β ((β Γ
β) βm β) β§ π΄ β βͺ ran
((,) β π)) β
π΄ β βͺ ran ((,) β π)) |
47 | | ioossico 13361 |
. . . . . . . . . . . . . . . . . . 19
β’
((1st β(πβπ))(,)(2nd β(πβπ))) β ((1st β(πβπ))[,)(2nd β(πβπ))) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β ((β Γ
β) βm β) β§ π β β) β ((1st
β(πβπ))(,)(2nd
β(πβπ))) β ((1st
β(πβπ))[,)(2nd
β(πβπ)))) |
49 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β ((β Γ
β) βm β) β§ π β β) β π:ββΆ(β Γ
β)) |
50 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β ((β Γ
β) βm β) β§ π β β) β π β β) |
51 | 49, 50 | fvovco 43501 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β ((β Γ
β) βm β) β§ π β β) β (((,) β π)βπ) = ((1st β(πβπ))(,)(2nd β(πβπ)))) |
52 | 49, 50 | fvovco 43501 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β ((β Γ
β) βm β) β§ π β β) β (([,) β π)βπ) = ((1st β(πβπ))[,)(2nd β(πβπ)))) |
53 | 48, 51, 52 | 3sstr4d 3992 |
. . . . . . . . . . . . . . . . 17
β’ ((π β ((β Γ
β) βm β) β§ π β β) β (((,) β π)βπ) β (([,) β π)βπ)) |
54 | 53 | ralrimiva 3140 |
. . . . . . . . . . . . . . . 16
β’ (π β ((β Γ
β) βm β) β βπ β β (((,) β π)βπ) β (([,) β π)βπ)) |
55 | | ss2iun 4973 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
β (((,) β π)βπ) β (([,) β π)βπ) β βͺ
π β β (((,)
β π)βπ) β βͺ π β β (([,) β π)βπ)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((β Γ
β) βm β) β βͺ
π β β (((,)
β π)βπ) β βͺ π β β (([,) β π)βπ)) |
57 | | ioof 13370 |
. . . . . . . . . . . . . . . . . . 19
β’
(,):(β* Γ β*)βΆπ«
β |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((β Γ
β) βm β) β (,):(β* Γ
β*)βΆπ« β) |
59 | | rexpssxrxp 11205 |
. . . . . . . . . . . . . . . . . . 19
β’ (β
Γ β) β (β* Γ
β*) |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((β Γ
β) βm β) β (β Γ β) β
(β* Γ β*)) |
61 | 58, 60, 26 | fcoss 43518 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β Γ
β) βm β) β ((,) β π):ββΆπ«
β) |
62 | 61 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’ (π β ((β Γ
β) βm β) β ((,) β π) Fn β) |
63 | | fniunfv 7195 |
. . . . . . . . . . . . . . . 16
β’ (((,)
β π) Fn β
β βͺ π β β (((,) β π)βπ) = βͺ ran ((,)
β π)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((β Γ
β) βm β) β βͺ
π β β (((,)
β π)βπ) = βͺ
ran ((,) β π)) |
65 | | icof 43527 |
. . . . . . . . . . . . . . . . . . 19
β’
[,):(β* Γ β*)βΆπ«
β* |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((β Γ
β) βm β) β [,):(β* Γ
β*)βΆπ« β*) |
67 | 66, 60, 26 | fcoss 43518 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β Γ
β) βm β) β ([,) β π):ββΆπ«
β*) |
68 | 67 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’ (π β ((β Γ
β) βm β) β ([,) β π) Fn β) |
69 | | fniunfv 7195 |
. . . . . . . . . . . . . . . 16
β’ (([,)
β π) Fn β
β βͺ π β β (([,) β π)βπ) = βͺ ran ([,)
β π)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((β Γ
β) βm β) β βͺ
π β β (([,)
β π)βπ) = βͺ
ran ([,) β π)) |
71 | 56, 64, 70 | 3sstr3d 3991 |
. . . . . . . . . . . . . 14
β’ (π β ((β Γ
β) βm β) β βͺ ran
((,) β π) β
βͺ ran ([,) β π)) |
72 | 71 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β ((β Γ
β) βm β) β§ π΄ β βͺ ran
((,) β π)) β
βͺ ran ((,) β π) β βͺ ran
([,) β π)) |
73 | 46, 72 | sstrd 3955 |
. . . . . . . . . . . 12
β’ ((π β ((β Γ
β) βm β) β§ π΄ β βͺ ran
((,) β π)) β
π΄ β βͺ ran ([,) β π)) |
74 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β ((β Γ
β) βm β) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β π¦ =
(Ξ£^β((vol β (,)) β π))) |
75 | 26 | voliooicof 44323 |
. . . . . . . . . . . . . . 15
β’ (π β ((β Γ
β) βm β) β ((vol β (,)) β π) = ((vol β [,)) β
π)) |
76 | 75 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (π β ((β Γ
β) βm β) β
(Ξ£^β((vol β (,)) β π)) =
(Ξ£^β((vol β [,)) β π))) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β ((β Γ
β) βm β) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β
(Ξ£^β((vol β (,)) β π)) =
(Ξ£^β((vol β [,)) β π))) |
78 | 74, 77 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β ((β Γ
β) βm β) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β π¦ =
(Ξ£^β((vol β [,)) β π))) |
79 | 73, 78 | anim12dan 620 |
. . . . . . . . . . 11
β’ ((π β ((β Γ
β) βm β) β§ (π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π)))) β (π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) |
80 | 79 | ex 414 |
. . . . . . . . . 10
β’ (π β ((β Γ
β) βm β) β ((π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β (π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π))))) |
81 | 80 | reximia 3081 |
. . . . . . . . 9
β’
(βπ β
((β Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β βπ β ((β Γ
β) βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))) |
82 | 81 | a1i 11 |
. . . . . . . 8
β’ (π¦ β β*
β (βπ β
((β Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β βπ β ((β Γ
β) βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π))))) |
83 | 82 | ss2rabi 4035 |
. . . . . . 7
β’ {π¦ β β*
β£ βπ β
((β Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π)))} β {π¦ β β* β£
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))} |
84 | 45, 83 | eqsstri 3979 |
. . . . . 6
β’ {π§ β β*
β£ βπ β
((β Γ β) βm β)(π΄ β βͺ ran
((,) β π) β§ π§ =
(Ξ£^β((vol β (,)) β π)))} β {π¦ β β* β£
βπ β ((β
Γ β) βm β)(π΄ β βͺ ran
([,) β π) β§ π¦ =
(Ξ£^β((vol β [,)) β π)))} |
85 | 84, 1, 5 | 3sstr4i 3988 |
. . . . 5
β’ π β π |
86 | | infxrss 13264 |
. . . . 5
β’ ((π β π β§ π β β*) β
inf(π, β*,
< ) β€ inf(π,
β*, < )) |
87 | 85, 6, 86 | mp2an 691 |
. . . 4
β’ inf(π, β*, < )
β€ inf(π,
β*, < ) |
88 | 87 | a1i 11 |
. . 3
β’ (β€
β inf(π,
β*, < ) β€ inf(π, β*, <
)) |
89 | 4, 8, 41, 88 | xrletrid 13080 |
. 2
β’ (β€
β inf(π,
β*, < ) = inf(π, β*, <
)) |
90 | 89 | mptru 1549 |
1
β’ inf(π, β*, < ) =
inf(π, β*,
< ) |