Step | Hyp | Ref
| Expression |
1 | | ovolval3.a |
. . 3
β’ (π β π΄ β β) |
2 | | eqid 2733 |
. . 3
β’ {π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))} = {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))} |
3 | 1, 2 | ovolval2 45360 |
. 2
β’ (π β (vol*βπ΄) = inf({π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))}, β*, <
)) |
4 | | ovolval3.m |
. . . . 5
β’ π = {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π)))} |
5 | | reex 11201 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ β
β V |
6 | 5, 5 | xpex 7740 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β
Γ β) β V |
7 | | inss2 4230 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
8 | | mapss 8883 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β Γ β) β V β§ ( β€ β© (β Γ
β)) β (β Γ β)) β (( β€ β© (β
Γ β)) βm β) β ((β Γ
β) βm β)) |
9 | 6, 7, 8 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (( β€
β© (β Γ β)) βm β) β ((β
Γ β) βm β) |
10 | 9 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (( β€ β© (β
Γ β)) βm β) β π β ((β Γ β)
βm β)) |
11 | | elmapi 8843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((β Γ
β) βm β) β π:ββΆ(β Γ
β)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (( β€ β© (β
Γ β)) βm β) β π:ββΆ(β Γ
β)) |
13 | 12 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (πβπ) β (β Γ
β)) |
14 | | 1st2nd2 8014 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ) β (β Γ β) β
(πβπ) = β¨(1st β(πβπ)), (2nd β(πβπ))β©) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (πβπ) = β¨(1st β(πβπ)), (2nd β(πβπ))β©) |
16 | 15 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((,)β(πβπ)) = ((,)ββ¨(1st
β(πβπ)), (2nd
β(πβπ))β©)) |
17 | | df-ov 7412 |
. . . . . . . . . . . . . . . . . 18
β’
((1st β(πβπ))(,)(2nd β(πβπ))) = ((,)ββ¨(1st
β(πβπ)), (2nd
β(πβπ))β©) |
18 | 17 | eqcomi 2742 |
. . . . . . . . . . . . . . . . 17
β’
((,)ββ¨(1st β(πβπ)), (2nd β(πβπ))β©) = ((1st β(πβπ))(,)(2nd β(πβπ))) |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β
((,)ββ¨(1st β(πβπ)), (2nd β(πβπ))β©) = ((1st β(πβπ))(,)(2nd β(πβπ)))) |
20 | 16, 19 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((,)β(πβπ)) = ((1st β(πβπ))(,)(2nd β(πβπ)))) |
21 | 20 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β
(volβ((,)β(πβπ))) = (volβ((1st
β(πβπ))(,)(2nd
β(πβπ))))) |
22 | | xp1st 8007 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β (β Γ β) β
(1st β(πβπ)) β β) |
23 | 13, 22 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (1st
β(πβπ)) β
β) |
24 | | xp2nd 8008 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β (β Γ β) β
(2nd β(πβπ)) β β) |
25 | 13, 24 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (2nd
β(πβπ)) β
β) |
26 | | elmapi 8843 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (( β€ β© (β
Γ β)) βm β) β π:ββΆ( β€ β© (β Γ
β))) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β π:ββΆ( β€ β© (β Γ
β))) |
28 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β π β β) |
29 | | ovolfcl 24983 |
. . . . . . . . . . . . . . . . 17
β’ ((π:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((1st
β(πβπ)) β β β§
(2nd β(πβπ)) β β β§ (1st
β(πβπ)) β€ (2nd
β(πβπ)))) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((1st
β(πβπ)) β β β§
(2nd β(πβπ)) β β β§ (1st
β(πβπ)) β€ (2nd
β(πβπ)))) |
31 | 30 | simp3d 1145 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (1st
β(πβπ)) β€ (2nd
β(πβπ))) |
32 | | volioo 25086 |
. . . . . . . . . . . . . . 15
β’
(((1st β(πβπ)) β β β§ (2nd
β(πβπ)) β β β§
(1st β(πβπ)) β€ (2nd β(πβπ))) β (volβ((1st
β(πβπ))(,)(2nd
β(πβπ)))) = ((2nd
β(πβπ)) β (1st
β(πβπ)))) |
33 | 23, 25, 31, 32 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β
(volβ((1st β(πβπ))(,)(2nd β(πβπ)))) = ((2nd β(πβπ)) β (1st β(πβπ)))) |
34 | 21, 33 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β
(volβ((,)β(πβπ))) = ((2nd β(πβπ)) β (1st β(πβπ)))) |
35 | | ioof 13424 |
. . . . . . . . . . . . . . . 16
β’
(,):(β* Γ β*)βΆπ«
β |
36 | | ffun 6721 |
. . . . . . . . . . . . . . . 16
β’
((,):(β* Γ β*)βΆπ«
β β Fun (,)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ Fun
(,) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β Fun
(,)) |
39 | | rexpssxrxp 11259 |
. . . . . . . . . . . . . . . 16
β’ (β
Γ β) β (β* Γ
β*) |
40 | 39, 13 | sselid 3981 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (πβπ) β (β* Γ
β*)) |
41 | 35 | fdmi 6730 |
. . . . . . . . . . . . . . . . 17
β’ dom (,) =
(β* Γ β*) |
42 | 41 | eqcomi 2742 |
. . . . . . . . . . . . . . . 16
β’
(β* Γ β*) = dom
(,) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (β*
Γ β*) = dom (,)) |
44 | 40, 43 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (πβπ) β dom (,)) |
45 | | fvco 6990 |
. . . . . . . . . . . . . 14
β’ ((Fun (,)
β§ (πβπ) β dom (,)) β ((vol
β (,))β(πβπ)) = (volβ((,)β(πβπ)))) |
46 | 38, 44, 45 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((vol β
(,))β(πβπ)) =
(volβ((,)β(πβπ)))) |
47 | 15 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((abs β β
)β(πβπ)) = ((abs β β
)ββ¨(1st β(πβπ)), (2nd β(πβπ))β©)) |
48 | | df-ov 7412 |
. . . . . . . . . . . . . . . 16
β’
((1st β(πβπ))(abs β β )(2nd
β(πβπ))) = ((abs β β
)ββ¨(1st β(πβπ)), (2nd β(πβπ))β©) |
49 | 48 | eqcomi 2742 |
. . . . . . . . . . . . . . 15
β’ ((abs
β β )ββ¨(1st β(πβπ)), (2nd β(πβπ))β©) = ((1st β(πβπ))(abs β β )(2nd
β(πβπ))) |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((abs β β
)ββ¨(1st β(πβπ)), (2nd β(πβπ))β©) = ((1st β(πβπ))(abs β β )(2nd
β(πβπ)))) |
51 | 23 | recnd 11242 |
. . . . . . . . . . . . . . . 16
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (1st
β(πβπ)) β
β) |
52 | 25 | recnd 11242 |
. . . . . . . . . . . . . . . 16
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β (2nd
β(πβπ)) β
β) |
53 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (abs
β β ) = (abs β β ) |
54 | 53 | cnmetdval 24287 |
. . . . . . . . . . . . . . . 16
β’
(((1st β(πβπ)) β β β§ (2nd
β(πβπ)) β β) β
((1st β(πβπ))(abs β β )(2nd
β(πβπ))) =
(absβ((1st β(πβπ)) β (2nd β(πβπ))))) |
55 | 51, 52, 54 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((1st
β(πβπ))(abs β β
)(2nd β(πβπ))) = (absβ((1st
β(πβπ)) β (2nd
β(πβπ))))) |
56 | | abssub 15273 |
. . . . . . . . . . . . . . . 16
β’
(((1st β(πβπ)) β β β§ (2nd
β(πβπ)) β β) β
(absβ((1st β(πβπ)) β (2nd β(πβπ)))) = (absβ((2nd
β(πβπ)) β (1st
β(πβπ))))) |
57 | 51, 52, 56 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β
(absβ((1st β(πβπ)) β (2nd β(πβπ)))) = (absβ((2nd
β(πβπ)) β (1st
β(πβπ))))) |
58 | 23, 25, 31 | abssubge0d 15378 |
. . . . . . . . . . . . . . 15
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β
(absβ((2nd β(πβπ)) β (1st β(πβπ)))) = ((2nd β(πβπ)) β (1st β(πβπ)))) |
59 | 55, 57, 58 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((1st
β(πβπ))(abs β β
)(2nd β(πβπ))) = ((2nd β(πβπ)) β (1st β(πβπ)))) |
60 | 47, 50, 59 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((abs β β
)β(πβπ)) = ((2nd
β(πβπ)) β (1st
β(πβπ)))) |
61 | 34, 46, 60 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’ ((π β (( β€ β© (β
Γ β)) βm β) β§ π β β) β ((vol β
(,))β(πβπ)) = ((abs β β
)β(πβπ))) |
62 | 61 | mpteq2dva 5249 |
. . . . . . . . . . 11
β’ (π β (( β€ β© (β
Γ β)) βm β) β (π β β β¦ ((vol β
(,))β(πβπ))) = (π β β β¦ ((abs β β
)β(πβπ)))) |
63 | | volioof 44703 |
. . . . . . . . . . . . 13
β’ (vol
β (,)):(β* Γ
β*)βΆ(0[,]+β) |
64 | 63 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β (vol β
(,)):(β* Γ
β*)βΆ(0[,]+β)) |
65 | 39 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (( β€ β© (β
Γ β)) βm β) β (β Γ β)
β (β* Γ β*)) |
66 | 12, 65 | fssd 6736 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β π:ββΆ(β* Γ
β*)) |
67 | | fcompt 7131 |
. . . . . . . . . . . 12
β’ (((vol
β (,)):(β* Γ
β*)βΆ(0[,]+β) β§ π:ββΆ(β* Γ
β*)) β ((vol β (,)) β π) = (π β β β¦ ((vol β
(,))β(πβπ)))) |
68 | 64, 66, 67 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (( β€ β© (β
Γ β)) βm β) β ((vol β (,)) β
π) = (π β β β¦ ((vol β
(,))β(πβπ)))) |
69 | | absf 15284 |
. . . . . . . . . . . . . 14
β’
abs:ββΆβ |
70 | | subf 11462 |
. . . . . . . . . . . . . 14
β’ β
:(β Γ β)βΆβ |
71 | | fco 6742 |
. . . . . . . . . . . . . 14
β’
((abs:ββΆβ β§ β :(β Γ
β)βΆβ) β (abs β β ):(β Γ
β)βΆβ) |
72 | 69, 70, 71 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (abs
β β ):(β Γ β)βΆβ |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β (abs β β
):(β Γ β)βΆβ) |
74 | | rr2sscn2 44076 |
. . . . . . . . . . . . . 14
β’ (β
Γ β) β (β Γ β) |
75 | 74 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (( β€ β© (β
Γ β)) βm β) β (β Γ β)
β (β Γ β)) |
76 | 12, 75 | fssd 6736 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β π:ββΆ(β Γ
β)) |
77 | | fcompt 7131 |
. . . . . . . . . . . 12
β’ (((abs
β β ):(β Γ β)βΆβ β§ π:ββΆ(β Γ
β)) β ((abs β β ) β π) = (π β β β¦ ((abs β β
)β(πβπ)))) |
78 | 73, 76, 77 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (( β€ β© (β
Γ β)) βm β) β ((abs β β )
β π) = (π β β β¦ ((abs
β β )β(πβπ)))) |
79 | 62, 68, 78 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ (π β (( β€ β© (β
Γ β)) βm β) β ((vol β (,)) β
π) = ((abs β β
) β π)) |
80 | 79 | fveq2d 6896 |
. . . . . . . . 9
β’ (π β (( β€ β© (β
Γ β)) βm β) β
(Ξ£^β((vol β (,)) β π)) =
(Ξ£^β((abs β β ) β π))) |
81 | 80 | eqeq2d 2744 |
. . . . . . . 8
β’ (π β (( β€ β© (β
Γ β)) βm β) β (π¦ =
(Ξ£^β((vol β (,)) β π)) β π¦ =
(Ξ£^β((abs β β ) β π)))) |
82 | 81 | anbi2d 630 |
. . . . . . 7
β’ (π β (( β€ β© (β
Γ β)) βm β) β ((π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β (π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π))))) |
83 | 82 | rexbiia 3093 |
. . . . . 6
β’
(βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π))) β βπ β (( β€ β© (β
Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))) |
84 | 83 | rabbii 3439 |
. . . . 5
β’ {π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ =
(Ξ£^β((vol β (,)) β π)))} = {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))} |
85 | 4, 84 | eqtr2i 2762 |
. . . 4
β’ {π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))} = π |
86 | 85 | infeq1i 9473 |
. . 3
β’
inf({π¦ β
β* β£ βπ β (( β€ β© (β Γ
β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))}, β*, <
) = inf(π,
β*, < ) |
87 | 86 | a1i 11 |
. 2
β’ (π β inf({π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))}, β*, <
) = inf(π,
β*, < )) |
88 | 3, 87 | eqtrd 2773 |
1
β’ (π β (vol*βπ΄) = inf(π, β*, <
)) |