Step |
Hyp |
Ref |
Expression |
1 |
|
mscl.x |
β’ π = ( Base β π ) |
2 |
|
mscl.d |
β’ π· = ( dist β π ) |
3 |
|
ovres |
β’ ( ( π΄ β π β§ π΅ β π ) β ( π΄ ( π· βΎ ( π Γ π ) ) π΅ ) = ( π΄ π· π΅ ) ) |
4 |
3
|
3adant1 |
β’ ( ( π β βMetSp β§ π΄ β π β§ π΅ β π ) β ( π΄ ( π· βΎ ( π Γ π ) ) π΅ ) = ( π΄ π· π΅ ) ) |
5 |
4
|
eqeq1d |
β’ ( ( π β βMetSp β§ π΄ β π β§ π΅ β π ) β ( ( π΄ ( π· βΎ ( π Γ π ) ) π΅ ) = 0 β ( π΄ π· π΅ ) = 0 ) ) |
6 |
1 2
|
xmsxmet2 |
β’ ( π β βMetSp β ( π· βΎ ( π Γ π ) ) β ( βMet β π ) ) |
7 |
|
xmeteq0 |
β’ ( ( ( π· βΎ ( π Γ π ) ) β ( βMet β π ) β§ π΄ β π β§ π΅ β π ) β ( ( π΄ ( π· βΎ ( π Γ π ) ) π΅ ) = 0 β π΄ = π΅ ) ) |
8 |
6 7
|
syl3an1 |
β’ ( ( π β βMetSp β§ π΄ β π β§ π΅ β π ) β ( ( π΄ ( π· βΎ ( π Γ π ) ) π΅ ) = 0 β π΄ = π΅ ) ) |
9 |
5 8
|
bitr3d |
β’ ( ( π β βMetSp β§ π΄ β π β§ π΅ β π ) β ( ( π΄ π· π΅ ) = 0 β π΄ = π΅ ) ) |