Step | Hyp | Ref
| Expression |
1 | | metrel 13845 |
. . 3
β’ Rel
Met |
2 | | relelfvdm 5548 |
. . . 4
β’ ((Rel Met
β§ π· β
(Metβπ)) β π β dom
Met) |
3 | 2 | elexd 2751 |
. . 3
β’ ((Rel Met
β§ π· β
(Metβπ)) β π β V) |
4 | 1, 3 | mpan 424 |
. 2
β’ (π· β (Metβπ) β π β V) |
5 | | xmetrel 13846 |
. . . . 5
β’ Rel
βMet |
6 | | relelfvdm 5548 |
. . . . 5
β’ ((Rel
βMet β§ π· β
(βMetβπ))
β π β dom
βMet) |
7 | 5, 6 | mpan 424 |
. . . 4
β’ (π· β (βMetβπ) β π β dom βMet) |
8 | 7 | elexd 2751 |
. . 3
β’ (π· β (βMetβπ) β π β V) |
9 | 8 | adantr 276 |
. 2
β’ ((π· β (βMetβπ) β§ π·:(π Γ π)βΆβ) β π β V) |
10 | | simpllr 534 |
. . . . . . . . . . . 12
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π·:(π Γ π)βΆβ) |
11 | | simpr 110 |
. . . . . . . . . . . 12
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π§ β π) |
12 | | simplrl 535 |
. . . . . . . . . . . 12
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π₯ β π) |
13 | 10, 11, 12 | fovcdmd 6019 |
. . . . . . . . . . 11
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π§π·π₯) β β) |
14 | | simplrr 536 |
. . . . . . . . . . . 12
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β π¦ β π) |
15 | 10, 11, 14 | fovcdmd 6019 |
. . . . . . . . . . 11
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β (π§π·π¦) β β) |
16 | 13, 15 | rexaddd 9854 |
. . . . . . . . . 10
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) + (π§π·π¦))) |
17 | 16 | breq2d 4016 |
. . . . . . . . 9
β’ ((((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β§ π§ β π) β ((π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))) |
18 | 17 | ralbidva 2473 |
. . . . . . . 8
β’ (((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β (βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))) |
19 | 18 | anbi2d 464 |
. . . . . . 7
β’ (((π β V β§ π·:(π Γ π)βΆβ) β§ (π₯ β π β§ π¦ β π)) β ((((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))))) |
20 | 19 | 2ralbidva 2499 |
. . . . . 6
β’ ((π β V β§ π·:(π Γ π)βΆβ) β (βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))))) |
21 | | simpr 110 |
. . . . . . . 8
β’ ((π β V β§ π·:(π Γ π)βΆβ) β π·:(π Γ π)βΆβ) |
22 | | ressxr 8001 |
. . . . . . . 8
β’ β
β β* |
23 | | fss 5378 |
. . . . . . . 8
β’ ((π·:(π Γ π)βΆβ β§ β β
β*) β π·:(π Γ π)βΆβ*) |
24 | 21, 22, 23 | sylancl 413 |
. . . . . . 7
β’ ((π β V β§ π·:(π Γ π)βΆβ) β π·:(π Γ π)βΆβ*) |
25 | 24 | biantrurd 305 |
. . . . . 6
β’ ((π β V β§ π·:(π Γ π)βΆβ) β (βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
26 | 20, 25 | bitr3d 190 |
. . . . 5
β’ ((π β V β§ π·:(π Γ π)βΆβ) β (βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
27 | 26 | pm5.32da 452 |
. . . 4
β’ (π β V β ((π·:(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))) β (π·:(π Γ π)βΆβ β§ (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))))))) |
28 | | ancom 266 |
. . . 4
β’ ((π·:(π Γ π)βΆβ β§ (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))))) β ((π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) β§ π·:(π Γ π)βΆβ)) |
29 | 27, 28 | bitrdi 196 |
. . 3
β’ (π β V β ((π·:(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))) β ((π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) β§ π·:(π Γ π)βΆβ))) |
30 | | ismet 13847 |
. . 3
β’ (π β V β (π· β (Metβπ) β (π·:(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))))) |
31 | | isxmet 13848 |
. . . 4
β’ (π β V β (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
32 | 31 | anbi1d 465 |
. . 3
β’ (π β V β ((π· β (βMetβπ) β§ π·:(π Γ π)βΆβ) β ((π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) β§ π·:(π Γ π)βΆβ))) |
33 | 29, 30, 32 | 3bitr4d 220 |
. 2
β’ (π β V β (π· β (Metβπ) β (π· β (βMetβπ) β§ π·:(π Γ π)βΆβ))) |
34 | 4, 9, 33 | pm5.21nii 704 |
1
β’ (π· β (Metβπ) β (π· β (βMetβπ) β§ π·:(π Γ π)βΆβ)) |