Step | Hyp | Ref
| Expression |
1 | | ovolicc2.m |
. . . . . 6
β’ π = {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)((π΄[,]π΅) β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, <
))} |
2 | 1 | elovolm 24855 |
. . . . 5
β’ (π§ β π β βπ β (( β€ β© (β Γ
β)) βm β)((π΄[,]π΅) β βͺ ran
((,) β π) β§ π§ = sup(ran seq1( + , ((abs
β β ) β π)), β*, <
))) |
3 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
(π΄[,]π΅) β βͺ ran
((,) β π)) |
4 | | unieq 4877 |
. . . . . . . . . . . . . 14
β’ (π’ = ran ((,) β π) β βͺ π’ =
βͺ ran ((,) β π)) |
5 | 4 | sseq2d 3977 |
. . . . . . . . . . . . 13
β’ (π’ = ran ((,) β π) β ((π΄[,]π΅) β βͺ π’ β (π΄[,]π΅) β βͺ ran
((,) β π))) |
6 | | pweq 4575 |
. . . . . . . . . . . . . . 15
β’ (π’ = ran ((,) β π) β π« π’ = π« ran ((,) β
π)) |
7 | 6 | ineq1d 4172 |
. . . . . . . . . . . . . 14
β’ (π’ = ran ((,) β π) β (π« π’ β© Fin) = (π« ran
((,) β π) β©
Fin)) |
8 | 7 | rexeqdv 3313 |
. . . . . . . . . . . . 13
β’ (π’ = ran ((,) β π) β (βπ£ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π£ β βπ£ β (π« ran ((,)
β π) β© Fin)(π΄[,]π΅) β βͺ π£)) |
9 | 5, 8 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π’ = ran ((,) β π) β (((π΄[,]π΅) β βͺ π’ β βπ£ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π£) β ((π΄[,]π΅) β βͺ ran
((,) β π) β
βπ£ β (π«
ran ((,) β π) β©
Fin)(π΄[,]π΅) β βͺ π£))) |
10 | | ovolicc.1 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β β) |
11 | | ovolicc.2 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β β) |
12 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(topGenβran (,)) = (topGenβran (,)) |
13 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
((topGenβran (,)) βΎt (π΄[,]π΅)) = ((topGenβran (,))
βΎt (π΄[,]π΅)) |
14 | 12, 13 | icccmp 24204 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΅ β β) β
((topGenβran (,)) βΎt (π΄[,]π΅)) β Comp) |
15 | 10, 11, 14 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β ((topGenβran (,))
βΎt (π΄[,]π΅)) β Comp) |
16 | | retop 24141 |
. . . . . . . . . . . . . . 15
β’
(topGenβran (,)) β Top |
17 | | iccssre 13352 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
18 | 10, 11, 17 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄[,]π΅) β β) |
19 | | uniretop 24142 |
. . . . . . . . . . . . . . . 16
β’ β =
βͺ (topGenβran (,)) |
20 | 19 | cmpsub 22767 |
. . . . . . . . . . . . . . 15
β’
(((topGenβran (,)) β Top β§ (π΄[,]π΅) β β) β
(((topGenβran (,)) βΎt (π΄[,]π΅)) β Comp β βπ’ β π«
(topGenβran (,))((π΄[,]π΅) β βͺ π’ β βπ£ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π£))) |
21 | 16, 18, 20 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β (((topGenβran (,))
βΎt (π΄[,]π΅)) β Comp β βπ’ β π«
(topGenβran (,))((π΄[,]π΅) β βͺ π’ β βπ£ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π£))) |
22 | 15, 21 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β βπ’ β π« (topGenβran
(,))((π΄[,]π΅) β βͺ π’ β βπ£ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π£)) |
23 | 22 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
βπ’ β π«
(topGenβran (,))((π΄[,]π΅) β βͺ π’ β βπ£ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π£)) |
24 | | ioof 13370 |
. . . . . . . . . . . . . . . . . . 19
β’
(,):(β* Γ β*)βΆπ«
β |
25 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . 19
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ (,) Fn
(β* Γ β*) |
27 | | dffn3 6682 |
. . . . . . . . . . . . . . . . . 18
β’ ((,) Fn
(β* Γ β*) β
(,):(β* Γ β*)βΆran
(,)) |
28 | 26, 27 | mpbi 229 |
. . . . . . . . . . . . . . . . 17
β’
(,):(β* Γ β*)βΆran
(,) |
29 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β π β (( β€ β© (β Γ
β)) βm β)) |
30 | | elovolmlem 24854 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (( β€ β© (β
Γ β)) βm β) β π:ββΆ( β€ β© (β Γ
β))) |
31 | 29, 30 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β π:ββΆ( β€ β© (β Γ
β))) |
32 | | inss2 4190 |
. . . . . . . . . . . . . . . . . . 19
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
33 | | rexpssxrxp 11205 |
. . . . . . . . . . . . . . . . . . 19
β’ (β
Γ β) β (β* Γ
β*) |
34 | 32, 33 | sstri 3954 |
. . . . . . . . . . . . . . . . . 18
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
35 | | fss 6686 |
. . . . . . . . . . . . . . . . . 18
β’ ((π:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β π:ββΆ(β* Γ
β*)) |
36 | 31, 34, 35 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β π:ββΆ(β* Γ
β*)) |
37 | | fco 6693 |
. . . . . . . . . . . . . . . . 17
β’
(((,):(β* Γ β*)βΆran (,)
β§ π:ββΆ(β* Γ
β*)) β ((,) β π):ββΆran (,)) |
38 | 28, 36, 37 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β ((,) β π):ββΆran (,)) |
39 | 38 | adantrr 716 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
((,) β π):ββΆran (,)) |
40 | 39 | frnd 6677 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
ran ((,) β π) β
ran (,)) |
41 | | retopbas 24140 |
. . . . . . . . . . . . . . 15
β’ ran (,)
β TopBases |
42 | | bastg 22332 |
. . . . . . . . . . . . . . 15
β’ (ran (,)
β TopBases β ran (,) β (topGenβran (,))) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ran (,)
β (topGenβran (,)) |
44 | 40, 43 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
ran ((,) β π) β
(topGenβran (,))) |
45 | | fvex 6856 |
. . . . . . . . . . . . . 14
β’
(topGenβran (,)) β V |
46 | 45 | elpw2 5303 |
. . . . . . . . . . . . 13
β’ (ran ((,)
β π) β π«
(topGenβran (,)) β ran ((,) β π) β (topGenβran
(,))) |
47 | 44, 46 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
ran ((,) β π) β
π« (topGenβran (,))) |
48 | 9, 23, 47 | rspcdva 3581 |
. . . . . . . . . . 11
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
((π΄[,]π΅) β βͺ ran
((,) β π) β
βπ£ β (π«
ran ((,) β π) β©
Fin)(π΄[,]π΅) β βͺ π£)) |
49 | 3, 48 | mpd 15 |
. . . . . . . . . 10
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
βπ£ β (π«
ran ((,) β π) β©
Fin)(π΄[,]π΅) β βͺ π£) |
50 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β π£ β (π« ran ((,) β π) β© Fin)) |
51 | | elin 3927 |
. . . . . . . . . . . . . . . 16
β’ (π£ β (π« ran ((,)
β π) β© Fin)
β (π£ β π«
ran ((,) β π) β§
π£ β
Fin)) |
52 | 50, 51 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β (π£ β π« ran ((,) β π) β§ π£ β Fin)) |
53 | 52 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β π£ β Fin) |
54 | 52 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β π£ β π« ran ((,) β π)) |
55 | 54 | elpwid 4570 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β π£ β ran ((,) β π)) |
56 | 55 | sseld 3944 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β (π‘ β π£ β π‘ β ran ((,) β π))) |
57 | 38 | ffnd 6670 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β ((,) β π) Fn β) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β ((,) β π) Fn β) |
59 | | fvelrnb 6904 |
. . . . . . . . . . . . . . . . 17
β’ (((,)
β π) Fn β
β (π‘ β ran ((,)
β π) β
βπ β β
(((,) β π)βπ) = π‘)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β (π‘ β ran ((,) β π) β βπ β β (((,) β π)βπ) = π‘)) |
61 | 56, 60 | sylibd 238 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β (π‘ β π£ β βπ β β (((,) β π)βπ) = π‘)) |
62 | 61 | ralrimiv 3139 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β βπ‘ β π£ βπ β β (((,) β π)βπ) = π‘) |
63 | | fveqeq2 6852 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ‘) β ((((,) β π)βπ) = π‘ β (((,) β π)β(πβπ‘)) = π‘)) |
64 | 63 | ac6sfi 9234 |
. . . . . . . . . . . . . 14
β’ ((π£ β Fin β§ βπ‘ β π£ βπ β β (((,) β π)βπ) = π‘) β βπ(π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘)) |
65 | 53, 62, 64 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β βπ(π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘)) |
66 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β π΄ β β) |
67 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β π΅ β β) |
68 | | ovolicc.3 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β€ π΅) |
69 | 68 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β π΄ β€ π΅) |
70 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ seq1( + ,
((abs β β ) β π)) = seq1( + , ((abs β β )
β π)) |
71 | 31 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β π:ββΆ( β€ β© (β Γ
β))) |
72 | | simprll 778 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β π£ β (π« ran ((,) β π) β© Fin)) |
73 | | simprlr 779 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β (π΄[,]π΅) β βͺ π£) |
74 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β π:π£βΆβ) |
75 | | simprrr 781 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘) |
76 | | 2fveq3 6848 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π₯ β (((,) β π)β(πβπ‘)) = (((,) β π)β(πβπ₯))) |
77 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π₯ β π‘ = π₯) |
78 | 76, 77 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = π₯ β ((((,) β π)β(πβπ‘)) = π‘ β (((,) β π)β(πβπ₯)) = π₯)) |
79 | 78 | rspccva 3579 |
. . . . . . . . . . . . . . . . 17
β’
((βπ‘ β
π£ (((,) β π)β(πβπ‘)) = π‘ β§ π₯ β π£) β (((,) β π)β(πβπ₯)) = π₯) |
80 | 75, 79 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β§ π₯ β π£) β (((,) β π)β(πβπ₯)) = π₯) |
81 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ {π’ β π£ β£ (π’ β© (π΄[,]π΅)) β β
} = {π’ β π£ β£ (π’ β© (π΄[,]π΅)) β β
} |
82 | 66, 67, 69, 70, 71, 72, 73, 74, 80, 81 | ovolicc2lem5 24901 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ ((π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£) β§ (π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘))) β (π΅ β π΄) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < )) |
83 | 82 | expr 458 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β ((π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘) β (π΅ β π΄) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < ))) |
84 | 83 | exlimdv 1937 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β (βπ(π:π£βΆβ β§ βπ‘ β π£ (((,) β π)β(πβπ‘)) = π‘) β (π΅ β π΄) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < ))) |
85 | 65, 84 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β§ π β (( β€ β© (β Γ
β)) βm β)) β§ (π£ β (π« ran ((,) β π) β© Fin) β§ (π΄[,]π΅) β βͺ π£)) β (π΅ β π΄) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < )) |
86 | 85 | rexlimdvaa 3150 |
. . . . . . . . . . 11
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β (βπ£ β (π« ran ((,) β π) β© Fin)(π΄[,]π΅) β βͺ π£ β (π΅ β π΄) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < ))) |
87 | 86 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
(βπ£ β (π«
ran ((,) β π) β©
Fin)(π΄[,]π΅) β βͺ π£ β (π΅ β π΄) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < ))) |
88 | 49, 87 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
(π΅ β π΄) β€ sup(ran seq1( + , ((abs
β β ) β π)), β*, <
)) |
89 | | breq2 5110 |
. . . . . . . . 9
β’ (π§ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ) β
((π΅ β π΄) β€ π§ β (π΅ β π΄) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < ))) |
90 | 88, 89 | syl5ibrcom 247 |
. . . . . . . 8
β’ ((π β§ (π β (( β€ β© (β Γ
β)) βm β) β§ (π΄[,]π΅) β βͺ ran
((,) β π))) β
(π§ = sup(ran seq1( + ,
((abs β β ) β π)), β*, < ) β (π΅ β π΄) β€ π§)) |
91 | 90 | expr 458 |
. . . . . . 7
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β ((π΄[,]π΅) β βͺ ran
((,) β π) β
(π§ = sup(ran seq1( + ,
((abs β β ) β π)), β*, < ) β (π΅ β π΄) β€ π§))) |
92 | 91 | impd 412 |
. . . . . 6
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β (((π΄[,]π΅) β βͺ ran
((,) β π) β§ π§ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
(π΅ β π΄) β€ π§)) |
93 | 92 | rexlimdva 3149 |
. . . . 5
β’ (π β (βπ β (( β€ β© (β Γ
β)) βm β)((π΄[,]π΅) β βͺ ran
((,) β π) β§ π§ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
(π΅ β π΄) β€ π§)) |
94 | 2, 93 | biimtrid 241 |
. . . 4
β’ (π β (π§ β π β (π΅ β π΄) β€ π§)) |
95 | 94 | ralrimiv 3139 |
. . 3
β’ (π β βπ§ β π (π΅ β π΄) β€ π§) |
96 | 1 | ssrab3 4041 |
. . . 4
β’ π β
β* |
97 | 11, 10 | resubcld 11588 |
. . . . 5
β’ (π β (π΅ β π΄) β β) |
98 | 97 | rexrd 11210 |
. . . 4
β’ (π β (π΅ β π΄) β
β*) |
99 | | infxrgelb 13260 |
. . . 4
β’ ((π β β*
β§ (π΅ β π΄) β β*)
β ((π΅ β π΄) β€ inf(π, β*, < ) β
βπ§ β π (π΅ β π΄) β€ π§)) |
100 | 96, 98, 99 | sylancr 588 |
. . 3
β’ (π β ((π΅ β π΄) β€ inf(π, β*, < ) β
βπ§ β π (π΅ β π΄) β€ π§)) |
101 | 95, 100 | mpbird 257 |
. 2
β’ (π β (π΅ β π΄) β€ inf(π, β*, <
)) |
102 | 1 | ovolval 24853 |
. . 3
β’ ((π΄[,]π΅) β β β (vol*β(π΄[,]π΅)) = inf(π, β*, <
)) |
103 | 18, 102 | syl 17 |
. 2
β’ (π β (vol*β(π΄[,]π΅)) = inf(π, β*, <
)) |
104 | 101, 103 | breqtrrd 5134 |
1
β’ (π β (π΅ β π΄) β€ (vol*β(π΄[,]π΅))) |