Step | Hyp | Ref
| Expression |
1 | | elfvdm 6922 |
. . . 4
β’ (π· β (βMetβπ) β π β dom βMet) |
2 | 1 | adantr 480 |
. . 3
β’ ((π· β (βMetβπ) β§ π
β π) β π β dom βMet) |
3 | | simpr 484 |
. . 3
β’ ((π· β (βMetβπ) β§ π
β π) β π
β π) |
4 | 2, 3 | ssexd 5317 |
. 2
β’ ((π· β (βMetβπ) β§ π
β π) β π
β V) |
5 | | xmetf 24190 |
. . . 4
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
6 | 5 | adantr 480 |
. . 3
β’ ((π· β (βMetβπ) β§ π
β π) β π·:(π Γ π)βΆβ*) |
7 | | xpss12 5684 |
. . . 4
β’ ((π
β π β§ π
β π) β (π
Γ π
) β (π Γ π)) |
8 | 3, 7 | sylancom 587 |
. . 3
β’ ((π· β (βMetβπ) β§ π
β π) β (π
Γ π
) β (π Γ π)) |
9 | 6, 8 | fssresd 6752 |
. 2
β’ ((π· β (βMetβπ) β§ π
β π) β (π· βΎ (π
Γ π
)):(π
Γ π
)βΆβ*) |
10 | | ovres 7570 |
. . . . 5
β’ ((π₯ β π
β§ π¦ β π
) β (π₯(π· βΎ (π
Γ π
))π¦) = (π₯π·π¦)) |
11 | 10 | adantl 481 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β (π₯(π· βΎ (π
Γ π
))π¦) = (π₯π·π¦)) |
12 | 11 | eqeq1d 2728 |
. . 3
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β ((π₯(π· βΎ (π
Γ π
))π¦) = 0 β (π₯π·π¦) = 0)) |
13 | | simpll 764 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β π· β (βMetβπ)) |
14 | | simplr 766 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β π
β π) |
15 | | simprl 768 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β π₯ β π
) |
16 | 14, 15 | sseldd 3978 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β π₯ β π) |
17 | | simprr 770 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β π¦ β π
) |
18 | 14, 17 | sseldd 3978 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β π¦ β π) |
19 | | xmeteq0 24199 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β π β§ π¦ β π) β ((π₯π·π¦) = 0 β π₯ = π¦)) |
20 | 13, 16, 18, 19 | syl3anc 1368 |
. . 3
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β ((π₯π·π¦) = 0 β π₯ = π¦)) |
21 | 12, 20 | bitrd 279 |
. 2
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
)) β ((π₯(π· βΎ (π
Γ π
))π¦) = 0 β π₯ = π¦)) |
22 | | simpll 764 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π· β (βMetβπ)) |
23 | | simplr 766 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π
β π) |
24 | | simpr3 1193 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π§ β π
) |
25 | 23, 24 | sseldd 3978 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π§ β π) |
26 | 16 | 3adantr3 1168 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π₯ β π) |
27 | 18 | 3adantr3 1168 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π¦ β π) |
28 | | xmettri2 24201 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π§ β π β§ π₯ β π β§ π¦ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
29 | 22, 25, 26, 27, 28 | syl13anc 1369 |
. . 3
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
30 | 11 | 3adantr3 1168 |
. . 3
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β (π₯(π· βΎ (π
Γ π
))π¦) = (π₯π·π¦)) |
31 | | simpr1 1191 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π₯ β π
) |
32 | 24, 31 | ovresd 7571 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β (π§(π· βΎ (π
Γ π
))π₯) = (π§π·π₯)) |
33 | | simpr2 1192 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β π¦ β π
) |
34 | 24, 33 | ovresd 7571 |
. . . 4
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β (π§(π· βΎ (π
Γ π
))π¦) = (π§π·π¦)) |
35 | 32, 34 | oveq12d 7423 |
. . 3
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β ((π§(π· βΎ (π
Γ π
))π₯) +π (π§(π· βΎ (π
Γ π
))π¦)) = ((π§π·π₯) +π (π§π·π¦))) |
36 | 29, 30, 35 | 3brtr4d 5173 |
. 2
β’ (((π· β (βMetβπ) β§ π
β π) β§ (π₯ β π
β§ π¦ β π
β§ π§ β π
)) β (π₯(π· βΎ (π
Γ π
))π¦) β€ ((π§(π· βΎ (π
Γ π
))π₯) +π (π§(π· βΎ (π
Γ π
))π¦))) |
37 | 4, 9, 21, 36 | isxmetd 24187 |
1
β’ ((π· β (βMetβπ) β§ π
β π) β (π· βΎ (π
Γ π
)) β (βMetβπ
)) |