Step | Hyp | Ref
| Expression |
1 | | sblpnf.s |
. . 3
β’ (π β π β {β, β}) |
2 | | elpri 4650 |
. . 3
β’ (π β {β, β}
β (π = β β¨
π =
β)) |
3 | | sblpnf.d |
. . . . 5
β’ π· = ((abs β β )
βΎ (π Γ π)) |
4 | | eqid 2733 |
. . . . . . 7
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
5 | 4 | remet 24298 |
. . . . . 6
β’ ((abs
β β ) βΎ (β Γ β)) β
(Metββ) |
6 | | xpeq12 5701 |
. . . . . . . . 9
β’ ((π = β β§ π = β) β (π Γ π) = (β Γ
β)) |
7 | 6 | anidms 568 |
. . . . . . . 8
β’ (π = β β (π Γ π) = (β Γ
β)) |
8 | 7 | reseq2d 5980 |
. . . . . . 7
β’ (π = β β ((abs β
β ) βΎ (π
Γ π)) = ((abs β
β ) βΎ (β Γ β))) |
9 | | fveq2 6889 |
. . . . . . 7
β’ (π = β β
(Metβπ) =
(Metββ)) |
10 | 8, 9 | eleq12d 2828 |
. . . . . 6
β’ (π = β β (((abs β
β ) βΎ (π
Γ π)) β
(Metβπ) β ((abs
β β ) βΎ (β Γ β)) β
(Metββ))) |
11 | 5, 10 | mpbiri 258 |
. . . . 5
β’ (π = β β ((abs β
β ) βΎ (π
Γ π)) β
(Metβπ)) |
12 | 3, 11 | eqeltrid 2838 |
. . . 4
β’ (π = β β π· β (Metβπ)) |
13 | | relco 6105 |
. . . . . . . . 9
β’ Rel (abs
β β ) |
14 | | resdm 6025 |
. . . . . . . . 9
β’ (Rel (abs
β β ) β ((abs β β ) βΎ dom (abs β
β )) = (abs β β )) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . 8
β’ ((abs
β β ) βΎ dom (abs β β )) = (abs β β
) |
16 | | absf 15281 |
. . . . . . . . . . . 12
β’
abs:ββΆβ |
17 | | ax-resscn 11164 |
. . . . . . . . . . . 12
β’ β
β β |
18 | | fss 6732 |
. . . . . . . . . . . 12
β’
((abs:ββΆβ β§ β β β) β
abs:ββΆβ) |
19 | 16, 17, 18 | mp2an 691 |
. . . . . . . . . . 11
β’
abs:ββΆβ |
20 | | subf 11459 |
. . . . . . . . . . 11
β’ β
:(β Γ β)βΆβ |
21 | | fco 6739 |
. . . . . . . . . . 11
β’
((abs:ββΆβ β§ β :(β Γ
β)βΆβ) β (abs β β ):(β Γ
β)βΆβ) |
22 | 19, 20, 21 | mp2an 691 |
. . . . . . . . . 10
β’ (abs
β β ):(β Γ β)βΆβ |
23 | 22 | fdmi 6727 |
. . . . . . . . 9
β’ dom (abs
β β ) = (β Γ β) |
24 | 23 | reseq2i 5977 |
. . . . . . . 8
β’ ((abs
β β ) βΎ dom (abs β β )) = ((abs β β )
βΎ (β Γ β)) |
25 | 15, 24 | eqtr3i 2763 |
. . . . . . 7
β’ (abs
β β ) = ((abs β β ) βΎ (β Γ
β)) |
26 | | cnmet 24280 |
. . . . . . 7
β’ (abs
β β ) β (Metββ) |
27 | 25, 26 | eqeltrri 2831 |
. . . . . 6
β’ ((abs
β β ) βΎ (β Γ β)) β
(Metββ) |
28 | | xpeq12 5701 |
. . . . . . . . 9
β’ ((π = β β§ π = β) β (π Γ π) = (β Γ
β)) |
29 | 28 | anidms 568 |
. . . . . . . 8
β’ (π = β β (π Γ π) = (β Γ
β)) |
30 | 29 | reseq2d 5980 |
. . . . . . 7
β’ (π = β β ((abs β
β ) βΎ (π
Γ π)) = ((abs β
β ) βΎ (β Γ β))) |
31 | | fveq2 6889 |
. . . . . . 7
β’ (π = β β
(Metβπ) =
(Metββ)) |
32 | 30, 31 | eleq12d 2828 |
. . . . . 6
β’ (π = β β (((abs β
β ) βΎ (π
Γ π)) β
(Metβπ) β ((abs
β β ) βΎ (β Γ β)) β
(Metββ))) |
33 | 27, 32 | mpbiri 258 |
. . . . 5
β’ (π = β β ((abs β
β ) βΎ (π
Γ π)) β
(Metβπ)) |
34 | 3, 33 | eqeltrid 2838 |
. . . 4
β’ (π = β β π· β (Metβπ)) |
35 | 12, 34 | jaoi 856 |
. . 3
β’ ((π = β β¨ π = β) β π· β (Metβπ)) |
36 | 1, 2, 35 | 3syl 18 |
. 2
β’ (π β π· β (Metβπ)) |
37 | | blpnf 23895 |
. 2
β’ ((π· β (Metβπ) β§ π β π) β (π(ballβπ·)+β) = π) |
38 | 36, 37 | sylan 581 |
1
β’ ((π β§ π β π) β (π(ballβπ·)+β) = π) |