Step | Hyp | Ref
| Expression |
1 | | elinel2 4196 |
. . . . . . . . 9
β’ (π β (π β© π) β π β π) |
2 | | blres.2 |
. . . . . . . . . . 11
β’ πΆ = (π· βΎ (π Γ π)) |
3 | 2 | oveqi 7425 |
. . . . . . . . . 10
β’ (ππΆπ₯) = (π(π· βΎ (π Γ π))π₯) |
4 | | ovres 7577 |
. . . . . . . . . 10
β’ ((π β π β§ π₯ β π) β (π(π· βΎ (π Γ π))π₯) = (ππ·π₯)) |
5 | 3, 4 | eqtrid 2783 |
. . . . . . . . 9
β’ ((π β π β§ π₯ β π) β (ππΆπ₯) = (ππ·π₯)) |
6 | 1, 5 | sylan 579 |
. . . . . . . 8
β’ ((π β (π β© π) β§ π₯ β π) β (ππΆπ₯) = (ππ·π₯)) |
7 | 6 | breq1d 5158 |
. . . . . . 7
β’ ((π β (π β© π) β§ π₯ β π) β ((ππΆπ₯) < π
β (ππ·π₯) < π
)) |
8 | 7 | anbi2d 628 |
. . . . . 6
β’ ((π β (π β© π) β§ π₯ β π) β ((π₯ β π β§ (ππΆπ₯) < π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
9 | 8 | pm5.32da 578 |
. . . . 5
β’ (π β (π β© π) β ((π₯ β π β§ (π₯ β π β§ (ππΆπ₯) < π
)) β (π₯ β π β§ (π₯ β π β§ (ππ·π₯) < π
)))) |
10 | 9 | 3ad2ant2 1133 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β ((π₯ β π β§ (π₯ β π β§ (ππΆπ₯) < π
)) β (π₯ β π β§ (π₯ β π β§ (ππ·π₯) < π
)))) |
11 | | elin 3964 |
. . . . . . 7
β’ (π₯ β (π β© π) β (π₯ β π β§ π₯ β π)) |
12 | 11 | biancomi 462 |
. . . . . 6
β’ (π₯ β (π β© π) β (π₯ β π β§ π₯ β π)) |
13 | 12 | anbi1i 623 |
. . . . 5
β’ ((π₯ β (π β© π) β§ (ππΆπ₯) < π
) β ((π₯ β π β§ π₯ β π) β§ (ππΆπ₯) < π
)) |
14 | | anass 468 |
. . . . 5
β’ (((π₯ β π β§ π₯ β π) β§ (ππΆπ₯) < π
) β (π₯ β π β§ (π₯ β π β§ (ππΆπ₯) < π
))) |
15 | 13, 14 | bitri 275 |
. . . 4
β’ ((π₯ β (π β© π) β§ (ππΆπ₯) < π
) β (π₯ β π β§ (π₯ β π β§ (ππΆπ₯) < π
))) |
16 | | ancom 460 |
. . . 4
β’ (((π₯ β π β§ (ππ·π₯) < π
) β§ π₯ β π) β (π₯ β π β§ (π₯ β π β§ (ππ·π₯) < π
))) |
17 | 10, 15, 16 | 3bitr4g 314 |
. . 3
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β ((π₯ β (π β© π) β§ (ππΆπ₯) < π
) β ((π₯ β π β§ (ππ·π₯) < π
) β§ π₯ β π))) |
18 | | xmetres 24190 |
. . . . 5
β’ (π· β (βMetβπ) β (π· βΎ (π Γ π)) β (βMetβ(π β© π))) |
19 | 2, 18 | eqeltrid 2836 |
. . . 4
β’ (π· β (βMetβπ) β πΆ β (βMetβ(π β© π))) |
20 | | elbl 24214 |
. . . 4
β’ ((πΆ β (βMetβ(π β© π)) β§ π β (π β© π) β§ π
β β*) β (π₯ β (π(ballβπΆ)π
) β (π₯ β (π β© π) β§ (ππΆπ₯) < π
))) |
21 | 19, 20 | syl3an1 1162 |
. . 3
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β (π₯ β (π(ballβπΆ)π
) β (π₯ β (π β© π) β§ (ππΆπ₯) < π
))) |
22 | | elin 3964 |
. . . 4
β’ (π₯ β ((π(ballβπ·)π
) β© π) β (π₯ β (π(ballβπ·)π
) β§ π₯ β π)) |
23 | | elinel1 4195 |
. . . . . 6
β’ (π β (π β© π) β π β π) |
24 | | elbl 24214 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
25 | 23, 24 | syl3an2 1163 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
26 | 25 | anbi1d 629 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β ((π₯ β (π(ballβπ·)π
) β§ π₯ β π) β ((π₯ β π β§ (ππ·π₯) < π
) β§ π₯ β π))) |
27 | 22, 26 | bitrid 283 |
. . 3
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β (π₯ β ((π(ballβπ·)π
) β© π) β ((π₯ β π β§ (ππ·π₯) < π
) β§ π₯ β π))) |
28 | 17, 21, 27 | 3bitr4d 311 |
. 2
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β (π₯ β (π(ballβπΆ)π
) β π₯ β ((π(ballβπ·)π
) β© π))) |
29 | 28 | eqrdv 2729 |
1
β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β (π(ballβπΆ)π
) = ((π(ballβπ·)π
) β© π)) |