let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies ( p in Triangle (p1,p2,p3) iff ( tricord1 (p1,p2,p3,p) >= 0 & tricord2 (p1,p2,p3,p) >= 0 & tricord3 (p1,p2,p3,p) >= 0 & ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) ) ) )
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; :: thesis: ( p in Triangle (p1,p2,p3) iff ( tricord1 (p1,p2,p3,p) >= 0 & tricord2 (p1,p2,p3,p) >= 0 & tricord3 (p1,p2,p3,p) >= 0 & ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) ) )
A2: for p0 being Point of (TOP-REAL 2) holds
( p0 in Triangle (p1,p2,p3) iff ( p0 in LSeg (p1,p2) or p0 in LSeg (p2,p3) or p0 in LSeg (p3,p1) ) )
proof
let p0 be Point of (TOP-REAL 2); :: thesis: ( p0 in Triangle (p1,p2,p3) iff ( p0 in LSeg (p1,p2) or p0 in LSeg (p2,p3) or p0 in LSeg (p3,p1) ) )
( p0 in Triangle (p1,p2,p3) iff ( p0 in (LSeg (p1,p2)) \/ (LSeg (p2,p3)) or p0 in LSeg (p3,p1) ) ) by XBOOLE_0:def 3;
hence ( p0 in Triangle (p1,p2,p3) iff ( p0 in LSeg (p1,p2) or p0 in LSeg (p2,p3) or p0 in LSeg (p3,p1) ) ) by XBOOLE_0:def 3; :: thesis: verum
end;
thus ( p in Triangle (p1,p2,p3) implies ( tricord1 (p1,p2,p3,p) >= 0 & tricord2 (p1,p2,p3,p) >= 0 & tricord3 (p1,p2,p3,p) >= 0 & ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) ) ) :: thesis: ( tricord1 (p1,p2,p3,p) >= 0 & tricord2 (p1,p2,p3,p) >= 0 & tricord3 (p1,p2,p3,p) >= 0 & ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) implies p in Triangle (p1,p2,p3) )
proof
set x = p;
assume A3: p in Triangle (p1,p2,p3) ; :: thesis: ( tricord1 (p1,p2,p3,p) >= 0 & tricord2 (p1,p2,p3,p) >= 0 & tricord3 (p1,p2,p3,p) >= 0 & ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) )
A4: now :: thesis: ( ( p in LSeg (p1,p2) & ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) or ( p in LSeg (p2,p3) & ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) or ( p in LSeg (p3,p1) & ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) )
per cases ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) by A2, A3;
case p in LSeg (p1,p2) ; :: thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then consider lambda being Real such that
A5: p = ((1 - lambda) * p1) + (lambda * p2) and
A6: 0 <= lambda and
A7: lambda <= 1 ;
A8: p = (((1 - lambda) * p1) + (lambda * p2)) + (0. (TOP-REAL 2)) by A5, RLVECT_1:4
.= (((1 - lambda) * p1) + (lambda * p2)) + (0 * p3) by RLVECT_1:10 ;
A9: ((1 - lambda) + lambda) + 0 = 1 ;
1 - lambda >= 0 by A7, XREAL_1:48;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A6, A9, A8; :: thesis: verum
end;
case p in LSeg (p2,p3) ; :: thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then consider lambda being Real such that
A10: p = ((1 - lambda) * p2) + (lambda * p3) and
A11: 0 <= lambda and
A12: lambda <= 1 ;
A13: p = ((0. (TOP-REAL 2)) + ((1 - lambda) * p2)) + (lambda * p3) by A10, RLVECT_1:4
.= ((0 * p1) + ((1 - lambda) * p2)) + (lambda * p3) by RLVECT_1:10 ;
A14: (0 + (1 - lambda)) + lambda = 1 ;
1 - lambda >= 0 by A12, XREAL_1:48;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A11, A14, A13; :: thesis: verum
end;
case p in LSeg (p3,p1) ; :: thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then consider lambda being Real such that
A15: p = ((1 - lambda) * p3) + (lambda * p1) and
A16: 0 <= lambda and
A17: lambda <= 1 ;
A18: p = ((lambda * p1) + (0. (TOP-REAL 2))) + ((1 - lambda) * p3) by A15, RLVECT_1:4
.= ((lambda * p1) + (0 * p2)) + ((1 - lambda) * p3) by RLVECT_1:10 ;
A19: (lambda + 0) + (1 - lambda) = 1 ;
1 - lambda >= 0 by A17, XREAL_1:48;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A16, A19, A18; :: thesis: verum
end;
end;
end;
p in the carrier of (TOP-REAL 2) ;
then p in REAL 2 by EUCLID:22;
then p in plane (p1,p2,p3) by A1, Th54;
hence ( tricord1 (p1,p2,p3,p) >= 0 & tricord2 (p1,p2,p3,p) >= 0 & tricord3 (p1,p2,p3,p) >= 0 & ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) ) by A1, A4, Def11, Def12, Def13; :: thesis: verum
end;
thus ( tricord1 (p1,p2,p3,p) >= 0 & tricord2 (p1,p2,p3,p) >= 0 & tricord3 (p1,p2,p3,p) >= 0 & ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) implies p in Triangle (p1,p2,p3) ) :: thesis: verum
proof
set p0 = p;
assume that
A20: tricord1 (p1,p2,p3,p) >= 0 and
A21: tricord2 (p1,p2,p3,p) >= 0 and
A22: tricord3 (p1,p2,p3,p) >= 0 and
A23: ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) ; :: thesis: p in Triangle (p1,p2,p3)
set i01 = tricord1 (p1,p2,p3,p);
set i02 = tricord2 (p1,p2,p3,p);
set i03 = tricord3 (p1,p2,p3,p);
p in the carrier of (TOP-REAL 2) ;
then p in REAL 2 by EUCLID:22;
then A24: p in plane (p1,p2,p3) by A1, Th54;
now :: thesis: ( ( tricord1 (p1,p2,p3,p) = 0 & ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) ) or ( tricord2 (p1,p2,p3,p) = 0 & ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) ) or ( tricord3 (p1,p2,p3,p) = 0 & ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) ) )
per cases ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) by A23;
case tricord1 (p1,p2,p3,p) = 0 ; :: thesis: ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) )
then consider a2, a3 being Real such that
A25: (0 + a2) + a3 = 1 and
A26: p = ((0 * p1) + (a2 * p2)) + (a3 * p3) by A1, A24, Def11;
a2 = tricord2 (p1,p2,p3,p) by A1, A24, A25, A26, Def12;
then A27: (1 - a3) + a3 >= 0 + a3 by A21, A25, XREAL_1:7;
A28: p = ((0. (TOP-REAL 2)) + (a2 * p2)) + (a3 * p3) by A26, RLVECT_1:10
.= (a2 * p2) + (a3 * p3) by RLVECT_1:4 ;
a3 = tricord3 (p1,p2,p3,p) by A1, A24, A25, A26, Def13;
hence ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) by A22, A25, A28, A27; :: thesis: verum
end;
case tricord2 (p1,p2,p3,p) = 0 ; :: thesis: ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) )
then consider a1, a3 being Real such that
A29: (a1 + 0) + a3 = 1 and
A30: p = ((a1 * p1) + (0 * p2)) + (a3 * p3) by A1, A24, Def12;
a1 = tricord1 (p1,p2,p3,p) by A1, A24, A29, A30, Def11;
then A31: (1 - a3) + a3 >= 0 + a3 by A20, A29, XREAL_1:7;
A32: p = ((a1 * p1) + (0. (TOP-REAL 2))) + (a3 * p3) by A30, RLVECT_1:10
.= (a1 * p1) + (a3 * p3) by RLVECT_1:4 ;
a3 = tricord3 (p1,p2,p3,p) by A1, A24, A29, A30, Def13;
then p in { (((1 - lambda) * p1) + (lambda * p3)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A22, A29, A32, A31;
hence ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) by RLTOPSP1:def 2; :: thesis: verum
end;
case tricord3 (p1,p2,p3,p) = 0 ; :: thesis: ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) )
then consider a1, a2 being Real such that
A33: (a1 + a2) + 0 = 1 and
A34: p = ((a1 * p1) + (a2 * p2)) + (0 * p3) by A1, A24, Def13;
a1 = tricord1 (p1,p2,p3,p) by A1, A24, A33, A34, Def11;
then A35: (1 - a2) + a2 >= 0 + a2 by A20, A33, XREAL_1:7;
A36: p = ((a1 * p1) + (a2 * p2)) + (0. (TOP-REAL 2)) by A34, RLVECT_1:10
.= (a1 * p1) + (a2 * p2) by RLVECT_1:4 ;
a2 = tricord2 (p1,p2,p3,p) by A1, A24, A33, A34, Def12;
hence ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) by A21, A33, A36, A35; :: thesis: verum
end;
end;
end;
hence p in Triangle (p1,p2,p3) by A2; :: thesis: verum
end;