let p1, p2, p3, p be Point of (TOP-REAL 2); ( 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
; ( 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) 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) ) }
proof
let x be
object ;
TARSKI:def 3 ( 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 A3:
x in inside_of_triangle (
p1,
p2,
p3)
;
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 A4:
not
x in Triangle (
p1,
p2,
p3)
by XBOOLE_0:def 5;
x in closed_inside_of_triangle (
p1,
p2,
p3)
by A3, XBOOLE_0:def 5;
then consider p0 being
Point of
(TOP-REAL 2) such that A5:
p0 = x
and A6:
ex
a1,
a2,
a3 being
Real st
(
0 <= a1 &
0 <= a2 &
0 <= a3 &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
;
reconsider i01 =
tricord1 (
p1,
p2,
p3,
p0),
i02 =
tricord2 (
p1,
p2,
p3,
p0),
i03 =
tricord3 (
p1,
p2,
p3,
p0) as
Real ;
consider a1,
a2,
a3 being
Real such that A7:
0 <= a1
and A8:
0 <= a2
and A9:
0 <= a3
and A10:
(
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
by A6;
p0 in the
carrier of
(TOP-REAL 2)
;
then
p0 in REAL 2
by EUCLID:22;
then A11:
p0 in plane (
p1,
p2,
p3)
by A1, Th54;
then A12:
a1 = i01
by A1, A10, Def11;
A13:
a3 = i03
by A1, A10, A11, Def13;
then A14:
i02 <> 0
by A1, A4, A5, A7, A9, A12, Th56;
A15:
a2 = i02
by A1, A10, A11, Def12;
then A16:
i03 <> 0
by A1, A4, A5, A7, A8, A12, Th56;
i01 <> 0
by A1, A4, A5, A8, A9, A15, A13, Th56;
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 A5, A7, A8, A9, A10, A12, A15, A13, A14, A16;
verum
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 ) )
( 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
p in the
carrier of
(TOP-REAL 2)
;
then
p in REAL 2
by EUCLID:22;
then A17:
p in plane (
p1,
p2,
p3)
by A1, Th54;
assume A18:
p in inside_of_triangle (
p1,
p2,
p3)
;
( tricord1 (p1,p2,p3,p) > 0 & tricord2 (p1,p2,p3,p) > 0 & tricord3 (p1,p2,p3,p) > 0 )
then
p in closed_inside_of_triangle (
p1,
p2,
p3)
by XBOOLE_0:def 5;
then consider p0 being
Point of
(TOP-REAL 2) such that A19:
p0 = p
and A20:
ex
a1,
a2,
a3 being
Real st
(
0 <= a1 &
0 <= a2 &
0 <= a3 &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
;
not
p in Triangle (
p1,
p2,
p3)
by A18, XBOOLE_0:def 5;
then
( 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, A19, Th56;
hence
(
tricord1 (
p1,
p2,
p3,
p)
> 0 &
tricord2 (
p1,
p2,
p3,
p)
> 0 &
tricord3 (
p1,
p2,
p3,
p)
> 0 )
by A1, A19, A17, A20, Def11, Def12, Def13;
verum
end;
{ 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)
proof
let x be
object ;
TARSKI:def 3 ( 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) ) }
;
x in inside_of_triangle (p1,p2,p3)
then consider p0 being
Point of
(TOP-REAL 2) such that A21:
x = p0
and A22:
ex
a1,
a2,
a3 being
Real st
(
0 < a1 &
0 < a2 &
0 < a3 &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
;
A23:
x in closed_inside_of_triangle (
p1,
p2,
p3)
by A21, A22;
set i01 =
tricord1 (
p1,
p2,
p3,
p0);
set i02 =
tricord2 (
p1,
p2,
p3,
p0);
set i03 =
tricord3 (
p1,
p2,
p3,
p0);
consider a01,
a02,
a03 being
Real such that A24:
(
0 < a01 &
0 < a02 &
0 < a03 )
and A25:
(
(a01 + a02) + a03 = 1 &
p0 = ((a01 * p1) + (a02 * p2)) + (a03 * p3) )
by A22;
p0 in the
carrier of
(TOP-REAL 2)
;
then
p0 in REAL 2
by EUCLID:22;
then A26:
p0 in plane (
p1,
p2,
p3)
by A1, Th54;
then A27:
a03 = tricord3 (
p1,
p2,
p3,
p0)
by A1, A25, Def13;
(
a01 = tricord1 (
p1,
p2,
p3,
p0) &
a02 = tricord2 (
p1,
p2,
p3,
p0) )
by A1, A25, A26, Def11, Def12;
then
not
x in Triangle (
p1,
p2,
p3)
by A1, A21, A24, A27, Th56;
hence
x in inside_of_triangle (
p1,
p2,
p3)
by A23, XBOOLE_0:def 5;
verum
end;
then A28:
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) ) }
by A2;
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) )
verumproof
reconsider i1 =
tricord1 (
p1,
p2,
p3,
p),
i2 =
tricord2 (
p1,
p2,
p3,
p),
i3 =
tricord3 (
p1,
p2,
p3,
p) as
Real ;
assume A29:
(
tricord1 (
p1,
p2,
p3,
p)
> 0 &
tricord2 (
p1,
p2,
p3,
p)
> 0 &
tricord3 (
p1,
p2,
p3,
p)
> 0 )
;
p in inside_of_triangle (p1,p2,p3)
p in the
carrier of
(TOP-REAL 2)
;
then
p in REAL 2
by EUCLID:22;
then A30:
p in plane (
p1,
p2,
p3)
by A1, Th54;
then consider a2,
a3 being
Real such that A31:
(
(i1 + a2) + a3 = 1 &
p = ((i1 * p1) + (a2 * p2)) + (a3 * p3) )
by A1, Def11;
(
a2 = i2 &
a3 = i3 )
by A1, A30, A31, Def12, Def13;
hence
p in inside_of_triangle (
p1,
p2,
p3)
by A28, A29, A31;
verum
end;