Step | Hyp | Ref
| Expression |
1 | | totbndbnd 36743 |
. 2
β’ (π· β (TotBndβπ) β π· β (Bndβπ)) |
2 | | simpr 485 |
. . . . . 6
β’ ((π β§ π· β (Bndβπ)) β π· β (Bndβπ)) |
3 | | equivbnd2.7 |
. . . . . . 7
β’ πΆ = (π βΎ (π Γ π)) |
4 | | equivbnd2.1 |
. . . . . . . . 9
β’ (π β π β (Metβπ)) |
5 | 4 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π· β (Bndβπ)) β π β (Metβπ)) |
6 | | equivbnd2.2 |
. . . . . . . . 9
β’ (π β π β (Metβπ)) |
7 | | equivbnd2.8 |
. . . . . . . . . 10
β’ π· = (π βΎ (π Γ π)) |
8 | 7 | bnd2lem 36745 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ π· β (Bndβπ)) β π β π) |
9 | 6, 8 | sylan 580 |
. . . . . . . 8
β’ ((π β§ π· β (Bndβπ)) β π β π) |
10 | | metres2 23876 |
. . . . . . . 8
β’ ((π β (Metβπ) β§ π β π) β (π βΎ (π Γ π)) β (Metβπ)) |
11 | 5, 9, 10 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π· β (Bndβπ)) β (π βΎ (π Γ π)) β (Metβπ)) |
12 | 3, 11 | eqeltrid 2837 |
. . . . . 6
β’ ((π β§ π· β (Bndβπ)) β πΆ β (Metβπ)) |
13 | | equivbnd2.4 |
. . . . . . 7
β’ (π β π β
β+) |
14 | 13 | adantr 481 |
. . . . . 6
β’ ((π β§ π· β (Bndβπ)) β π β
β+) |
15 | 9 | sselda 3982 |
. . . . . . . . 9
β’ (((π β§ π· β (Bndβπ)) β§ π₯ β π) β π₯ β π) |
16 | 9 | sselda 3982 |
. . . . . . . . 9
β’ (((π β§ π· β (Bndβπ)) β§ π¦ β π) β π¦ β π) |
17 | 15, 16 | anim12dan 619 |
. . . . . . . 8
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯ β π β§ π¦ β π)) |
18 | | equivbnd2.6 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π Β· (π₯ππ¦))) |
19 | 18 | adantlr 713 |
. . . . . . . 8
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π Β· (π₯ππ¦))) |
20 | 17, 19 | syldan 591 |
. . . . . . 7
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π Β· (π₯ππ¦))) |
21 | 3 | oveqi 7424 |
. . . . . . . . 9
β’ (π₯πΆπ¦) = (π₯(π βΎ (π Γ π))π¦) |
22 | | ovres 7575 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π) β (π₯(π βΎ (π Γ π))π¦) = (π₯ππ¦)) |
23 | 21, 22 | eqtrid 2784 |
. . . . . . . 8
β’ ((π₯ β π β§ π¦ β π) β (π₯πΆπ¦) = (π₯ππ¦)) |
24 | 23 | adantl 482 |
. . . . . . 7
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) = (π₯ππ¦)) |
25 | 7 | oveqi 7424 |
. . . . . . . . . 10
β’ (π₯π·π¦) = (π₯(π βΎ (π Γ π))π¦) |
26 | | ovres 7575 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π) β (π₯(π βΎ (π Γ π))π¦) = (π₯ππ¦)) |
27 | 25, 26 | eqtrid 2784 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π) β (π₯π·π¦) = (π₯ππ¦)) |
28 | 27 | adantl 482 |
. . . . . . . 8
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) = (π₯ππ¦)) |
29 | 28 | oveq2d 7427 |
. . . . . . 7
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π Β· (π₯π·π¦)) = (π Β· (π₯ππ¦))) |
30 | 20, 24, 29 | 3brtr4d 5180 |
. . . . . 6
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) |
31 | 2, 12, 14, 30 | equivbnd 36744 |
. . . . 5
β’ ((π β§ π· β (Bndβπ)) β πΆ β (Bndβπ)) |
32 | | equivbnd2.9 |
. . . . . 6
β’ (π β (πΆ β (TotBndβπ) β πΆ β (Bndβπ))) |
33 | 32 | biimpar 478 |
. . . . 5
β’ ((π β§ πΆ β (Bndβπ)) β πΆ β (TotBndβπ)) |
34 | 31, 33 | syldan 591 |
. . . 4
β’ ((π β§ π· β (Bndβπ)) β πΆ β (TotBndβπ)) |
35 | | bndmet 36735 |
. . . . 5
β’ (π· β (Bndβπ) β π· β (Metβπ)) |
36 | 35 | adantl 482 |
. . . 4
β’ ((π β§ π· β (Bndβπ)) β π· β (Metβπ)) |
37 | | equivbnd2.3 |
. . . . 5
β’ (π β π
β
β+) |
38 | 37 | adantr 481 |
. . . 4
β’ ((π β§ π· β (Bndβπ)) β π
β
β+) |
39 | | equivbnd2.5 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π
Β· (π₯ππ¦))) |
40 | 39 | adantlr 713 |
. . . . . 6
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π
Β· (π₯ππ¦))) |
41 | 17, 40 | syldan 591 |
. . . . 5
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π
Β· (π₯ππ¦))) |
42 | 24 | oveq2d 7427 |
. . . . 5
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π
Β· (π₯πΆπ¦)) = (π
Β· (π₯ππ¦))) |
43 | 41, 28, 42 | 3brtr4d 5180 |
. . . 4
β’ (((π β§ π· β (Bndβπ)) β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β€ (π
Β· (π₯πΆπ¦))) |
44 | 34, 36, 38, 43 | equivtotbnd 36732 |
. . 3
β’ ((π β§ π· β (Bndβπ)) β π· β (TotBndβπ)) |
45 | 44 | ex 413 |
. 2
β’ (π β (π· β (Bndβπ) β π· β (TotBndβπ))) |
46 | 1, 45 | impbid2 225 |
1
β’ (π β (π· β (TotBndβπ) β π· β (Bndβπ))) |