let A, B, C be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: B = the_foot_of_the_altitude (A,B,C)
A = B
proof
assume A10: A <> B ; :: thesis: 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; :: thesis: verum
end;
hence B = the_foot_of_the_altitude (A,B,C) by A9; :: thesis: verum
end;
suppose A13: A <> the_foot_of_the_altitude (A,B,C) ; :: thesis: B = the_foot_of_the_altitude (A,B,C)
A14: A <> B
proof
assume A = B ; :: thesis: contradiction
then A in Line (B,C) by EUCLID_4:41;
hence contradiction by A13, A1, Th37; :: thesis: verum
end;
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; :: thesis: verum
end;
end;