let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 holds
P = plane (x1,x2,x3)
let x1, x2, x3 be Element of REAL n; :: thesis: for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 holds
P = plane (x1,x2,x3)
let P be Element of plane_of_REAL n; :: thesis: ( x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 implies P = plane (x1,x2,x3) )
assume that
A1: x1 in P and
A2: x2 in P and
A3: x3 in P and
A4: x2 - x1,x3 - x1 are_lindependent2 ; :: thesis: P = plane (x1,x2,x3)
P in plane_of_REAL n ;
then ex P9 being Subset of (REAL n) st
( P = P9 & ex y1, y2, y3 being Element of REAL n st P9 = plane (y1,y2,y3) ) ;
then consider y1, y2, y3 being Element of REAL n such that
A5: P = plane (y1,y2,y3) ;
ex x9 being Element of REAL n st
( x2 = x9 & ex a19, a29, a39 being Real st
( (a19 + a29) + a39 = 1 & x9 = ((a19 * y1) + (a29 * y2)) + (a39 * y3) ) ) by A2, A5;
then consider a21, a22, a23 being Real such that
A6: ( (a21 + a22) + a23 = 1 & x2 = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ) ;
ex x9 being Element of REAL n st
( x1 = x9 & ex a19, a29, a39 being Real st
( (a19 + a29) + a39 = 1 & x9 = ((a19 * y1) + (a29 * y2)) + (a39 * y3) ) ) by A1, A5;
then consider a11, a12, a13 being Real such that
A7: ( (a11 + a12) + a13 = 1 & x1 = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ) ;
ex x9 being Element of REAL n st
( x3 = x9 & ex a19, a29, a39 being Real st
( (a19 + a29) + a39 = 1 & x9 = ((a19 * y1) + (a29 * y2)) + (a39 * y3) ) ) by A3, A5;
then consider a31, a32, a33 being Real such that
A8: ( (a31 + a32) + a33 = 1 & x3 = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ) ;
x3 = (y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1)) by A8, Th27;
then A9: x3 - x1 = ((y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1))) + (- ((y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1)))) by A7, Th27
.= ((y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1))) + (((- y1) + (- (a12 * (y2 - y1)))) + (- (a13 * (y3 - y1)))) by Th8
.= ((y1 + (- y1)) + ((a32 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a33 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th17
.= ((0* n) + ((a32 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a33 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th2
.= ((0* n) + ((a32 - a12) * (y2 - y1))) + ((a33 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th11
.= ((0* n) + ((a32 - a12) * (y2 - y1))) + ((a33 - a13) * (y3 - y1)) by Th11
.= ((a32 - a12) * (y2 - y1)) + ((a33 - a13) * (y3 - y1)) by EUCLID_4:1 ;
A10: x1 = (y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1)) by A7, Th27;
then x2 - x1 = ((y1 + (a22 * (y2 - y1))) + (a23 * (y3 - y1))) + (- ((y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1)))) by A6, Th27
.= ((y1 + (a22 * (y2 - y1))) + (a23 * (y3 - y1))) + (((- y1) + (- (a12 * (y2 - y1)))) + (- (a13 * (y3 - y1)))) by Th8
.= ((y1 + (- y1)) + ((a22 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a23 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th17
.= ((0* n) + ((a22 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a23 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th2
.= ((0* n) + ((a22 - a12) * (y2 - y1))) + ((a23 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th11
.= ((0* n) + ((a22 - a12) * (y2 - y1))) + ((a23 - a13) * (y3 - y1)) by Th11
.= ((a22 - a12) * (y2 - y1)) + ((a23 - a13) * (y3 - y1)) by EUCLID_4:1 ;
then consider c1, c2, d1, d2 being Real such that
A11: ( y2 - y1 = (c1 * (x2 - x1)) + (c2 * (x3 - x1)) & y3 - y1 = (d1 * (x2 - x1)) + (d2 * (x3 - x1)) ) by A4, A9, Th36;
A12: x1 = y1 + ((a12 * (y2 - y1)) + (a13 * (y3 - y1))) by A10, RVSUM_1:15;
now :: thesis: for y being object st y in P holds
y in plane (x1,x2,x3)
let y be object ; :: thesis: ( y in P implies y in plane (x1,x2,x3) )
assume y in P ; :: thesis: y in plane (x1,x2,x3)
then ex x9 being Element of REAL n st
( y = x9 & ex a19, a29, a39 being Real st
( (a19 + a29) + a39 = 1 & x9 = ((a19 * y1) + (a29 * y2)) + (a39 * y3) ) ) by A5;
then consider b1, b2, b3 being Real such that
A13: ( (b1 + b2) + b3 = 1 & y = ((b1 * y1) + (b2 * y2)) + (b3 * y3) ) ;
y = (y1 + (b2 * (y2 - y1))) + (b3 * (y3 - y1)) by A13, Th27
.= ((x1 - ((a12 * (y2 - y1)) + (a13 * (y3 - y1)))) + (b2 * (y2 - y1))) + (b3 * (y3 - y1)) by A12, Th6
.= (((x1 - (a12 * (y2 - y1))) - (a13 * (y3 - y1))) + (b2 * (y2 - y1))) + (b3 * (y3 - y1)) by RVSUM_1:39
.= (((x1 + (- (a12 * (y2 - y1)))) + (b2 * (y2 - y1))) + (- (a13 * (y3 - y1)))) + (b3 * (y3 - y1)) by RVSUM_1:15
.= ((x1 + ((- (a12 * (y2 - y1))) + (b2 * (y2 - y1)))) + (- (a13 * (y3 - y1)))) + (b3 * (y3 - y1)) by RVSUM_1:15
.= (x1 + ((- (a12 * (y2 - y1))) + (b2 * (y2 - y1)))) + ((- (a13 * (y3 - y1))) + (b3 * (y3 - y1))) by RVSUM_1:15
.= (x1 + ((b2 - a12) * (y2 - y1))) + ((- (a13 * (y3 - y1))) + (b3 * (y3 - y1))) by Th11
.= (x1 + ((b2 - a12) * (y2 - y1))) + ((b3 - a13) * (y3 - y1)) by Th11
.= (x1 + (((b2 - a12) * (c1 * (x2 - x1))) + ((b2 - a12) * (c2 * (x3 - x1))))) + ((b3 - a13) * ((d1 * (x2 - x1)) + (d2 * (x3 - x1)))) by A11, EUCLID_4:6
.= (x1 + (((b2 - a12) * (c1 * (x2 - x1))) + ((b2 - a12) * (c2 * (x3 - x1))))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:6
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + ((b2 - a12) * (c2 * (x3 - x1))))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:4
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:4
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + ((((b3 - a13) * d1) * (x2 - x1)) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:4
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + ((((b3 - a13) * d1) * (x2 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by EUCLID_4:4
.= ((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + ((((b3 - a13) * d1) * (x2 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by RVSUM_1:15
.= (((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d1) * (x2 - x1))) + (((b3 - a13) * d2) * (x3 - x1)) by RVSUM_1:15
.= (((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b3 - a13) * d1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d2) * (x3 - x1)) by RVSUM_1:15
.= ((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b3 - a13) * d1) * (x2 - x1)))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d2) * (x3 - x1)) by RVSUM_1:15
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b3 - a13) * d1) * (x2 - x1)))) + ((((b2 - a12) * c2) * (x3 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by RVSUM_1:15
.= (x1 + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * (x2 - x1))) + ((((b2 - a12) * c2) * (x3 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by EUCLID_4:7
.= (x1 + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * (x2 - x1))) + ((((b2 - a12) * c2) + ((b3 - a13) * d2)) * (x3 - x1)) by EUCLID_4:7 ;
then ex a being Real st
( y = ((a * x1) + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * x2)) + ((((b2 - a12) * c2) + ((b3 - a13) * d2)) * x3) & (a + (((b2 - a12) * c1) + ((b3 - a13) * d1))) + (((b2 - a12) * c2) + ((b3 - a13) * d2)) = 1 ) by Th28;
hence y in plane (x1,x2,x3) ; :: thesis: verum
end;
then A14: P c= plane (x1,x2,x3) ;
plane (x1,x2,x3) c= P by A1, A2, A3, A5, Th83;
hence P = plane (x1,x2,x3) by A14, XBOOLE_0:def 10; :: thesis: verum