let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies ( p in inside_of_triangle p1,p2,p3 iff ( tricord1 p1,p2,p3,p > 0 & tricord2 p1,p2,p3,p > 0 & tricord3 p1,p2,p3,p > 0 ) ) )
assume A1:
p2 - p1,p3 - p1 are_lindependent2
; :: thesis: ( p in inside_of_triangle p1,p2,p3 iff ( tricord1 p1,p2,p3,p > 0 & tricord2 p1,p2,p3,p > 0 & tricord3 p1,p2,p3,p > 0 ) )
A2:
inside_of_triangle p1,p2,p3 = { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
proof
thus
inside_of_triangle p1,
p2,
p3 c= { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
:: according to XBOOLE_0:def 10 :: thesis: { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } c= inside_of_triangle p1,p2,p3proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in inside_of_triangle p1,p2,p3 or x in { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } )
assume
x in inside_of_triangle p1,
p2,
p3
;
:: thesis: x in { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
then A3:
(
x in closed_inside_of_triangle p1,
p2,
p3 & not
x in Triangle p1,
p2,
p3 )
by XBOOLE_0:def 5;
then consider p0 being
Point of
(TOP-REAL 2) such that A4:
(
p0 = x & ex
a1,
a2,
a3 being
Real st
(
0 <= a1 &
0 <= a2 &
0 <= a3 &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) )
;
consider a1,
a2,
a3 being
Real such that A5:
(
0 <= a1 &
0 <= a2 &
0 <= a3 &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
by A4;
set i01 =
tricord1 p1,
p2,
p3,
p0;
set i02 =
tricord2 p1,
p2,
p3,
p0;
set i03 =
tricord3 p1,
p2,
p3,
p0;
p0 in the
carrier of
(TOP-REAL 2)
;
then
p0 in REAL 2
by EUCLID:25;
then A6:
p0 in plane p1,
p2,
p3
by A1, Th63;
then A7:
a1 = tricord1 p1,
p2,
p3,
p0
by A1, A5, Def11;
A8:
a2 = tricord2 p1,
p2,
p3,
p0
by A1, A5, A6, Def12;
A9:
a3 = tricord3 p1,
p2,
p3,
p0
by A1, A5, A6, Def13;
then
(
tricord1 p1,
p2,
p3,
p0 <> 0 &
tricord2 p1,
p2,
p3,
p0 <> 0 &
tricord3 p1,
p2,
p3,
p0 <> 0 )
by A1, A3, A4, A5, A7, A8, Th65;
hence
x in { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
by A4, A5, A7, A8, A9;
:: thesis: verum
end;
thus
{ p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } c= inside_of_triangle p1,
p2,
p3
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } or x in inside_of_triangle p1,p2,p3 )
assume
x in { p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }
;
:: thesis: x in inside_of_triangle p1,p2,p3
then consider p0 being
Point of
(TOP-REAL 2) such that A10:
(
x = p0 & ex
a1,
a2,
a3 being
Real st
(
0 < a1 &
0 < a2 &
0 < a3 &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) )
;
consider a01,
a02,
a03 being
Real such that A11:
(
0 < a01 &
0 < a02 &
0 < a03 &
(a01 + a02) + a03 = 1 &
p0 = ((a01 * p1) + (a02 * p2)) + (a03 * p3) )
by A10;
set i01 =
tricord1 p1,
p2,
p3,
p0;
set i02 =
tricord2 p1,
p2,
p3,
p0;
set i03 =
tricord3 p1,
p2,
p3,
p0;
p0 in the
carrier of
(TOP-REAL 2)
;
then
p0 in REAL 2
by EUCLID:25;
then A12:
p0 in plane p1,
p2,
p3
by A1, Th63;
then A13:
a01 = tricord1 p1,
p2,
p3,
p0
by A1, A11, Def11;
A14:
a02 = tricord2 p1,
p2,
p3,
p0
by A1, A11, A12, Def12;
a03 = tricord3 p1,
p2,
p3,
p0
by A1, A11, A12, Def13;
then
(
x in closed_inside_of_triangle p1,
p2,
p3 & not
x in Triangle p1,
p2,
p3 )
by A1, A10, A11, A13, A14, Th65;
hence
x in inside_of_triangle p1,
p2,
p3
by XBOOLE_0:def 5;
:: thesis: verum
end;
end;
thus
( p in inside_of_triangle p1,p2,p3 implies ( tricord1 p1,p2,p3,p > 0 & tricord2 p1,p2,p3,p > 0 & 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 implies p in inside_of_triangle p1,p2,p3 )proof
assume
p in inside_of_triangle p1,
p2,
p3
;
:: thesis: ( tricord1 p1,p2,p3,p > 0 & tricord2 p1,p2,p3,p > 0 & tricord3 p1,p2,p3,p > 0 )
then A15:
(
p in closed_inside_of_triangle p1,
p2,
p3 & not
p in Triangle p1,
p2,
p3 )
by XBOOLE_0:def 5;
then consider p0 being
Point of
(TOP-REAL 2) such that A16:
(
p0 = p & ex
a1,
a2,
a3 being
Real st
(
0 <= a1 &
0 <= a2 &
0 <= a3 &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) )
;
A17:
( not
tricord1 p1,
p2,
p3,
p0 >= 0 or not
tricord2 p1,
p2,
p3,
p0 >= 0 or not
tricord3 p1,
p2,
p3,
p0 >= 0 or ( not
tricord1 p1,
p2,
p3,
p0 = 0 & not
tricord2 p1,
p2,
p3,
p0 = 0 & not
tricord3 p1,
p2,
p3,
p0 = 0 ) )
by A1, A15, A16, Th65;
p in the
carrier of
(TOP-REAL 2)
;
then
p in REAL 2
by EUCLID:25;
then
p in plane p1,
p2,
p3
by A1, Th63;
hence
(
tricord1 p1,
p2,
p3,
p > 0 &
tricord2 p1,
p2,
p3,
p > 0 &
tricord3 p1,
p2,
p3,
p > 0 )
by A1, A16, A17, 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 implies p in inside_of_triangle p1,p2,p3 )
:: thesis: verumproof
assume A18:
(
tricord1 p1,
p2,
p3,
p > 0 &
tricord2 p1,
p2,
p3,
p > 0 &
tricord3 p1,
p2,
p3,
p > 0 )
;
:: thesis: p in inside_of_triangle p1,p2,p3
p in the
carrier of
(TOP-REAL 2)
;
then
p in REAL 2
by EUCLID:25;
then A19:
p in plane p1,
p2,
p3
by A1, Th63;
set i1 =
tricord1 p1,
p2,
p3,
p;
set i2 =
tricord2 p1,
p2,
p3,
p;
set i3 =
tricord3 p1,
p2,
p3,
p;
consider a2,
a3 being
Real such that A20:
(
((tricord1 p1,p2,p3,p) + a2) + a3 = 1 &
p = (((tricord1 p1,p2,p3,p) * p1) + (a2 * p2)) + (a3 * p3) )
by A1, A19, Def11;
A21:
a2 = tricord2 p1,
p2,
p3,
p
by A1, A19, A20, Def12;
a3 = tricord3 p1,
p2,
p3,
p
by A1, A19, A20, Def13;
hence
p in inside_of_triangle p1,
p2,
p3
by A2, A18, A20, A21;
:: thesis: verum
end;