let A, B, C be Point of (TOP-REAL 2); ( B <> C & |((B - A),(B - C))| = 0 implies B = the_foot_of_the_altitude (A,B,C) )
assume that
A1:
B <> C
and
A2:
|((B - A),(B - C))| = 0
; B = the_foot_of_the_altitude (A,B,C)
set p = the_foot_of_the_altitude (A,B,C);
consider P being Point of (TOP-REAL 2) such that
A3:
the_foot_of_the_altitude (A,B,C) = P
and
A4:
(the_altitude (A,B,C)) /\ (Line (B,C)) = {P}
by A1, Def2;
consider L1, L2 being Element of line_of_REAL 2 such that
A5:
the_altitude (A,B,C) = L1
and
A6:
L2 = Line (B,C)
and
A7:
A in L1
and
A8:
L1 _|_ L2
by A1, Def1;
per cases
( A = the_foot_of_the_altitude (A,B,C) or A <> the_foot_of_the_altitude (A,B,C) )
;
suppose A9:
A = the_foot_of_the_altitude (
A,
B,
C)
;
B = the_foot_of_the_altitude (A,B,C)
A = B
proof
assume A10:
A <> B
;
contradiction
reconsider rA =
A,
rB =
B,
rC =
C as
Element of
REAL 2
by EUCLID:22;
reconsider LBA =
Line (
rB,
rA),
LBC =
Line (
rB,
rC) as
Element of
line_of_REAL 2
by EUCLIDLP:47;
A11:
Line (
B,
A)
= Line (
rB,
rA)
by EUCLID12:4;
then
(
A in LBA &
B in LBA )
by EUCLID_4:41;
then A12:
L1 meets LBA
by A7, XBOOLE_0:def 4;
(
A <> B &
B <> C &
|((B - A),(B - C))| = 0 &
LBA = Line (
B,
A) &
LBC = Line (
B,
C) )
by A1, A2, A10, EUCLID12:4;
then
(
LBA _|_ LBC &
L1 _|_ LBC &
LBA c= REAL 2 &
L1 c= REAL 2 &
LBC c= REAL 2 )
by A6, A8, Th9;
then
LBA = L1
by EUCLIDLP:111, EUCLID12:16, A12, EUCLIDLP:71;
then
(
B in L1 &
B in L2 )
by A6, A11, EUCLID_4:41;
then
B in {P}
by A4, A5, A6, XBOOLE_0:def 4;
hence
contradiction
by A10, A9, A3, TARSKI:def 1;
verum
end; hence
B = the_foot_of_the_altitude (
A,
B,
C)
by A9;
verum end; suppose A13:
A <> the_foot_of_the_altitude (
A,
B,
C)
;
B = the_foot_of_the_altitude (A,B,C)A14:
A <> B
reconsider rA =
A,
rB =
B,
rC =
C as
Element of
REAL 2
by EUCLID:22;
reconsider LBA =
Line (
rB,
rA),
LBC =
Line (
rB,
rC) as
Element of
line_of_REAL 2
by EUCLIDLP:47;
A15:
Line (
B,
A)
= Line (
rB,
rA)
by EUCLID12:4;
then
(
A in LBA &
B in LBA )
by EUCLID_4:41;
then A16:
L1 meets LBA
by A7, XBOOLE_0:def 4;
(
A <> B &
B <> C &
|((B - A),(B - C))| = 0 &
LBA = Line (
B,
A) &
LBC = Line (
B,
C) )
by A1, A2, A14, EUCLID12:4;
then
(
LBA _|_ LBC &
L1 _|_ LBC &
LBA c= REAL 2 &
L1 c= REAL 2 &
LBC c= REAL 2 )
by A6, A8, Th9;
then
LBA = L1
by EUCLIDLP:111, EUCLID12:16, A16, EUCLIDLP:71;
then
(
B in L1 &
B in L2 )
by A6, A15, EUCLID_4:41;
then
B in {P}
by A4, A5, A6, XBOOLE_0:def 4;
hence
B = the_foot_of_the_altitude (
A,
B,
C)
by A3, TARSKI:def 1;
verum end; end;