let n be Element of NAT ; :: thesis: for p1, p2, p3, p0 being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p0 in plane (p1,p2,p3) holds
ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )
let p1, p2, p3, p0 be Point of (TOP-REAL n); :: thesis: ( p2 - p1,p3 - p1 are_lindependent2 & p0 in plane (p1,p2,p3) implies ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) ) )
assume that
A1: p2 - p1,p3 - p1 are_lindependent2 and
A2: p0 in plane (p1,p2,p3) ; :: thesis: ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )
set q2 = p2 - p1;
set q3 = p3 - p1;
consider a01, a02, a03 being Real such that
A3: (a01 + a02) + a03 = 1 and
A4: p0 = ((a01 * p1) + (a02 * p2)) + (a03 * p3) by A2, Th48;
for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a01 & b2 = a02 & b3 = a03 )
proof
A5: p0 + (- p1) = (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 + a02) + a03) * p1)) by A3, A4, RLVECT_1:def 8
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 + a02) * p1) + (a03 * p1))) by RLVECT_1:def 6
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 * p1) + (a02 * p1)) + (a03 * p1))) by RLVECT_1:def 6
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + ((- ((a01 * p1) + (a02 * p1))) - (a03 * p1)) by RLVECT_1:30
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (((- (a01 * p1)) - (a02 * p1)) - (a03 * p1)) by RLVECT_1:30
.= ((a01 * p1) + ((a02 * p2) + (a03 * p3))) + (((- (a01 * p1)) + (- (a02 * p1))) + (- (a03 * p1))) by RLVECT_1:def 3
.= ((a01 * p1) + ((a02 * p2) + (a03 * p3))) + ((- (a01 * p1)) + ((- (a02 * p1)) + (- (a03 * p1)))) by RLVECT_1:def 3
.= ((((a02 * p2) + (a03 * p3)) + (a01 * p1)) - (a01 * p1)) + ((- (a02 * p1)) + (- (a03 * p1))) by RLVECT_1:def 3
.= ((a02 * p2) + (a03 * p3)) + ((- (a02 * p1)) + (- (a03 * p1))) by RLVECT_4:1
.= (((a02 * p2) + (a03 * p3)) + (- (a02 * p1))) + (- (a03 * p1)) by RLVECT_1:def 3
.= (((a02 * p2) + (- (a02 * p1))) + (a03 * p3)) + (- (a03 * p1)) by RLVECT_1:def 3
.= (((a02 * p2) + (a02 * (- p1))) + (a03 * p3)) + (- (a03 * p1)) by RLVECT_1:25
.= ((a02 * (p2 + (- p1))) + (a03 * p3)) + (- (a03 * p1)) by RLVECT_1:def 5
.= (a02 * (p2 + (- p1))) + ((a03 * p3) + (- (a03 * p1))) by RLVECT_1:def 3
.= (a02 * (p2 + (- p1))) + ((a03 * p3) + (a03 * (- p1))) by RLVECT_1:25
.= (a02 * (p2 - p1)) + (a03 * (p3 - p1)) by RLVECT_1:def 5 ;
let b1, b2, b3 be Real; :: thesis: ( p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 implies ( b1 = a01 & b2 = a02 & b3 = a03 ) )
assume that
A6: p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) and
A7: (b1 + b2) + b3 = 1 ; :: thesis: ( b1 = a01 & b2 = a02 & b3 = a03 )
p0 + (- p1) = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 + b2) + b3) * p1)) by A6, A7, RLVECT_1:def 8
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 + b2) * p1) + (b3 * p1))) by RLVECT_1:def 6
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 * p1) + (b2 * p1)) + (b3 * p1))) by RLVECT_1:def 6
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + ((- ((b1 * p1) + (b2 * p1))) - (b3 * p1)) by RLVECT_1:30
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (((- (b1 * p1)) - (b2 * p1)) - (b3 * p1)) by RLVECT_1:30
.= ((b1 * p1) + ((b2 * p2) + (b3 * p3))) + (((- (b1 * p1)) + (- (b2 * p1))) + (- (b3 * p1))) by RLVECT_1:def 3
.= ((b1 * p1) + ((b2 * p2) + (b3 * p3))) + ((- (b1 * p1)) + ((- (b2 * p1)) + (- (b3 * p1)))) by RLVECT_1:def 3
.= ((((b2 * p2) + (b3 * p3)) + (b1 * p1)) - (b1 * p1)) + ((- (b2 * p1)) + (- (b3 * p1))) by RLVECT_1:def 3
.= ((b2 * p2) + (b3 * p3)) + ((- (b2 * p1)) + (- (b3 * p1))) by RLVECT_4:1
.= (((b2 * p2) + (b3 * p3)) + (- (b2 * p1))) + (- (b3 * p1)) by RLVECT_1:def 3
.= (((b2 * p2) + (- (b2 * p1))) + (b3 * p3)) + (- (b3 * p1)) by RLVECT_1:def 3
.= (((b2 * p2) + (b2 * (- p1))) + (b3 * p3)) + (- (b3 * p1)) by RLVECT_1:25
.= ((b2 * (p2 + (- p1))) + (b3 * p3)) + (- (b3 * p1)) by RLVECT_1:def 5
.= (b2 * (p2 + (- p1))) + ((b3 * p3) + (- (b3 * p1))) by RLVECT_1:def 3
.= (b2 * (p2 + (- p1))) + ((b3 * p3) + (b3 * (- p1))) by RLVECT_1:25
.= (b2 * (p2 - p1)) + (b3 * (p3 - p1)) by RLVECT_1:def 5 ;
then ((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + (- ((a02 * (p2 - p1)) + (a03 * (p3 - p1)))) = 0. (TOP-REAL n) by A5, RLVECT_1:5;
then ((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + ((- (a02 * (p2 - p1))) - (a03 * (p3 - p1))) = 0. (TOP-REAL n) by RLVECT_1:30;
then (((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + (- (a02 * (p2 - p1)))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by RLVECT_1:def 3;
then (((b2 * (p2 - p1)) + (- (a02 * (p2 - p1)))) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by RLVECT_1:def 3;
then (((b2 * (p2 - p1)) + ((- a02) * (p2 - p1))) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by RLVECT_1:79;
then (((b2 + (- a02)) * (p2 - p1)) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by RLVECT_1:def 6;
then ((b2 + (- a02)) * (p2 - p1)) + ((b3 * (p3 - p1)) + (- (a03 * (p3 - p1)))) = 0. (TOP-REAL n) by RLVECT_1:def 3;
then ((b2 + (- a02)) * (p2 - p1)) + ((b3 * (p3 - p1)) + ((- a03) * (p3 - p1))) = 0. (TOP-REAL n) by RLVECT_1:79;
then ((b2 + (- a02)) * (p2 - p1)) + ((b3 + (- a03)) * (p3 - p1)) = 0. (TOP-REAL n) by RLVECT_1:def 6;
then ( (b2 - a02) + a02 = 0 + a02 & b3 + (- a03) = 0 ) by A1;
hence ( b1 = a01 & b2 = a02 & b3 = a03 ) by A3, A7; :: thesis: verum
end;
hence ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) ) by A3, A4; :: thesis: verum