Step | Hyp | Ref
| Expression |
1 | | elfvdm 6879 |
. . . . . 6
β’ (π· β (βMetβπ) β π β dom βMet) |
2 | | isxmet 23677 |
. . . . . 6
β’ (π β dom βMet β
(π· β
(βMetβπ) β
(π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π· β (βMetβπ) β (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
4 | 3 | ibi 266 |
. . . 4
β’ (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))))) |
5 | | simpl 483 |
. . . . 5
β’ ((((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β ((π₯π·π¦) = 0 β π₯ = π¦)) |
6 | 5 | 2ralimi 3126 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ₯ β π βπ¦ β π ((π₯π·π¦) = 0 β π₯ = π¦)) |
7 | 4, 6 | simpl2im 504 |
. . 3
β’ (π· β (βMetβπ) β βπ₯ β π βπ¦ β π ((π₯π·π¦) = 0 β π₯ = π¦)) |
8 | | oveq1 7364 |
. . . . . 6
β’ (π₯ = π΄ β (π₯π·π¦) = (π΄π·π¦)) |
9 | 8 | eqeq1d 2738 |
. . . . 5
β’ (π₯ = π΄ β ((π₯π·π¦) = 0 β (π΄π·π¦) = 0)) |
10 | | eqeq1 2740 |
. . . . 5
β’ (π₯ = π΄ β (π₯ = π¦ β π΄ = π¦)) |
11 | 9, 10 | bibi12d 345 |
. . . 4
β’ (π₯ = π΄ β (((π₯π·π¦) = 0 β π₯ = π¦) β ((π΄π·π¦) = 0 β π΄ = π¦))) |
12 | | oveq2 7365 |
. . . . . 6
β’ (π¦ = π΅ β (π΄π·π¦) = (π΄π·π΅)) |
13 | 12 | eqeq1d 2738 |
. . . . 5
β’ (π¦ = π΅ β ((π΄π·π¦) = 0 β (π΄π·π΅) = 0)) |
14 | | eqeq2 2748 |
. . . . 5
β’ (π¦ = π΅ β (π΄ = π¦ β π΄ = π΅)) |
15 | 13, 14 | bibi12d 345 |
. . . 4
β’ (π¦ = π΅ β (((π΄π·π¦) = 0 β π΄ = π¦) β ((π΄π·π΅) = 0 β π΄ = π΅))) |
16 | 11, 15 | rspc2v 3590 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π βπ¦ β π ((π₯π·π¦) = 0 β π₯ = π¦) β ((π΄π·π΅) = 0 β π΄ = π΅))) |
17 | 7, 16 | syl5com 31 |
. 2
β’ (π· β (βMetβπ) β ((π΄ β π β§ π΅ β π) β ((π΄π·π΅) = 0 β π΄ = π΅))) |
18 | 17 | 3impib 1116 |
1
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) = 0 β π΄ = π΅)) |