:: EUCLIDLP semantic presentation begin theorem Th1: :: EUCLIDLP:1 for s, t, u being Real for n being Element of NAT for x being Element of REAL n holds ( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x ) proof let s, t, u be Real; ::_thesis: for n being Element of NAT for x being Element of REAL n holds ( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x ) let n be Element of NAT ; ::_thesis: for x being Element of REAL n holds ( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x ) let x be Element of REAL n; ::_thesis: ( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x ) thus (s / t) * (u * x) = ((s / t) * u) * x by EUCLID_4:4 .= ((s * u) / t) * x by XCMPLX_1:74 ; ::_thesis: (1 / t) * (u * x) = (u / t) * x thus (1 / t) * (u * x) = ((1 / t) * u) * x by EUCLID_4:4 .= (u / t) * x by XCMPLX_1:99 ; ::_thesis: verum end; theorem Th2: :: EUCLIDLP:2 for n being Element of NAT for x being Element of REAL n holds ( x - x = 0* n & x + (- x) = 0* n ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n holds ( x - x = 0* n & x + (- x) = 0* n ) let x be Element of REAL n; ::_thesis: ( x - x = 0* n & x + (- x) = 0* n ) thus x - x = 0* n by RVSUM_1:37; ::_thesis: x + (- x) = 0* n hence x + (- x) = 0* n ; ::_thesis: verum end; theorem Th3: :: EUCLIDLP:3 for a being Real for n being Element of NAT for x being Element of REAL n holds ( - (a * x) = (- a) * x & - (a * x) = a * (- x) ) proof let a be Real; ::_thesis: for n being Element of NAT for x being Element of REAL n holds ( - (a * x) = (- a) * x & - (a * x) = a * (- x) ) let n be Element of NAT ; ::_thesis: for x being Element of REAL n holds ( - (a * x) = (- a) * x & - (a * x) = a * (- x) ) let x be Element of REAL n; ::_thesis: ( - (a * x) = (- a) * x & - (a * x) = a * (- x) ) thus - (a * x) = ((- 1) * a) * x by EUCLID_4:4 .= (- a) * x ; ::_thesis: - (a * x) = a * (- x) hence - (a * x) = (a * (- 1)) * x .= a * (- x) by EUCLID_4:4 ; ::_thesis: verum end; theorem Th4: :: EUCLIDLP:4 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds x1 - (x2 - x3) = (x1 - x2) + x3 proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds x1 - (x2 - x3) = (x1 - x2) + x3 let x1, x2, x3 be Element of REAL n; ::_thesis: x1 - (x2 - x3) = (x1 - x2) + x3 thus x1 - (x2 - x3) = (x1 - x2) - (- x3) by RVSUM_1:39 .= (x1 - x2) + x3 ; ::_thesis: verum end; theorem Th5: :: EUCLIDLP:5 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds x1 + (x2 - x3) = (x1 + x2) - x3 proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds x1 + (x2 - x3) = (x1 + x2) - x3 let x1, x2, x3 be Element of REAL n; ::_thesis: x1 + (x2 - x3) = (x1 + x2) - x3 thus x1 + (x2 - x3) = (x1 + x2) + (- x3) by RVSUM_1:15 .= (x1 + x2) - x3 ; ::_thesis: verum end; theorem Th6: :: EUCLIDLP:6 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds ( x1 = x2 + x3 iff x2 = x1 - x3 ) proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds ( x1 = x2 + x3 iff x2 = x1 - x3 ) let x1, x2, x3 be Element of REAL n; ::_thesis: ( x1 = x2 + x3 iff x2 = x1 - x3 ) thus ( x1 = x2 + x3 implies x2 = x1 - x3 ) ::_thesis: ( x2 = x1 - x3 implies x1 = x2 + x3 ) proof assume x1 = x2 + x3 ; ::_thesis: x2 = x1 - x3 hence x1 - x3 = x2 + (x3 + (- x3)) by RVSUM_1:15 .= x2 + (0* n) by Th2 .= x2 by EUCLID_4:1 ; ::_thesis: verum end; now__::_thesis:_(_x2_=_x1_-_x3_implies_x2_+_x3_=_x1_) assume x2 = x1 - x3 ; ::_thesis: x2 + x3 = x1 hence x2 + x3 = x1 + ((- x3) + x3) by RVSUM_1:15 .= x1 + (0* n) by Th2 .= x1 by EUCLID_4:1 ; ::_thesis: verum end; hence ( x2 = x1 - x3 implies x1 = x2 + x3 ) ; ::_thesis: verum end; theorem Th7: :: EUCLIDLP:7 for n being Element of NAT for x, x1, x2, x3 being Element of REAL n holds ( x = (x1 + x2) + x3 iff x - x1 = x2 + x3 ) proof let n be Element of NAT ; ::_thesis: for x, x1, x2, x3 being Element of REAL n holds ( x = (x1 + x2) + x3 iff x - x1 = x2 + x3 ) let x, x1, x2, x3 be Element of REAL n; ::_thesis: ( x = (x1 + x2) + x3 iff x - x1 = x2 + x3 ) thus ( x = (x1 + x2) + x3 implies x - x1 = x2 + x3 ) ::_thesis: ( x - x1 = x2 + x3 implies x = (x1 + x2) + x3 ) proof assume x = (x1 + x2) + x3 ; ::_thesis: x - x1 = x2 + x3 then x = x1 + (x2 + x3) by RVSUM_1:15; hence x - x1 = x2 + x3 by Th6; ::_thesis: verum end; now__::_thesis:_(_x_-_x1_=_x2_+_x3_implies_x_=_(x1_+_x2)_+_x3_) assume x - x1 = x2 + x3 ; ::_thesis: x = (x1 + x2) + x3 hence x = x1 + (x2 + x3) by Th6 .= (x1 + x2) + x3 by RVSUM_1:15 ; ::_thesis: verum end; hence ( x - x1 = x2 + x3 implies x = (x1 + x2) + x3 ) ; ::_thesis: verum end; theorem Th8: :: EUCLIDLP:8 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3) proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3) let x1, x2, x3 be Element of REAL n; ::_thesis: - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3) thus - ((x1 + x2) + x3) = (0* n) - ((x1 + x2) + x3) by RVSUM_1:33 .= ((0* n) - (x1 + x2)) - x3 by RVSUM_1:39 .= (((0* n) - x1) - x2) - x3 by RVSUM_1:39 .= ((- x1) + (- x2)) + (- x3) by RVSUM_1:33 ; ::_thesis: verum end; Lm1: for n being Element of NAT for x1, x2 being Element of REAL n st x1 <> x2 holds |.(x1 - x2).| <> 0 proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1 <> x2 holds |.(x1 - x2).| <> 0 let x1, x2 be Element of REAL n; ::_thesis: ( x1 <> x2 implies |.(x1 - x2).| <> 0 ) now__::_thesis:_(_x1_<>_x2_implies_|.(x1_-_x2).|_<>_0_) assume that A1: x1 <> x2 and A2: not |.(x1 - x2).| <> 0 ; ::_thesis: contradiction |((x1 - x2),(x1 - x2))| = 0 by A2, EUCLID_4:16; then x1 - x2 = 0* n by EUCLID_4:17; then x1 = x2 + (0* n) by Th6 .= x2 by EUCLID_4:1 ; hence contradiction by A1; ::_thesis: verum end; hence ( x1 <> x2 implies |.(x1 - x2).| <> 0 ) ; ::_thesis: verum end; theorem Th9: :: EUCLIDLP:9 for n being Element of NAT for x1, x2 being Element of REAL n holds ( x1 = x2 iff x1 - x2 = 0* n ) proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n holds ( x1 = x2 iff x1 - x2 = 0* n ) let x1, x2 be Element of REAL n; ::_thesis: ( x1 = x2 iff x1 - x2 = 0* n ) thus ( x1 = x2 implies x1 - x2 = 0* n ) by Th2; ::_thesis: ( x1 - x2 = 0* n implies x1 = x2 ) assume x1 - x2 = 0* n ; ::_thesis: x1 = x2 hence x1 = x2 + (0* n) by Th6 .= x2 by EUCLID_4:1 ; ::_thesis: verum end; theorem Th10: :: EUCLIDLP:10 for t being Real for n being Element of NAT for x1, x0, x being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds t <> 0 proof let t be Real; ::_thesis: for n being Element of NAT for x1, x0, x being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds t <> 0 let n be Element of NAT ; ::_thesis: for x1, x0, x being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds t <> 0 let x1, x0, x be Element of REAL n; ::_thesis: ( x1 - x0 = t * x & x1 <> x0 implies t <> 0 ) assume that A1: x1 - x0 = t * x and A2: x1 <> x0 ; ::_thesis: t <> 0 assume not t <> 0 ; ::_thesis: contradiction then x1 - x0 = 0* n by A1, EUCLID_4:3; hence contradiction by A2, Th9; ::_thesis: verum end; theorem Th11: :: EUCLIDLP:11 for a, b being Real for n being Element of NAT for x being Element of REAL n holds ( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) ) proof let a, b be Real; ::_thesis: for n being Element of NAT for x being Element of REAL n holds ( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) ) let n be Element of NAT ; ::_thesis: for x being Element of REAL n holds ( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) ) let x be Element of REAL n; ::_thesis: ( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) ) thus A1: (a - b) * x = (a + (- b)) * x .= (a * x) + ((- b) * x) by EUCLID_4:7 ; ::_thesis: ( (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) ) hence (a - b) * x = (a * x) + (- (b * x)) by Th3; ::_thesis: (a - b) * x = (a * x) - (b * x) thus (a - b) * x = (a * x) - (b * x) by A1, Th3; ::_thesis: verum end; theorem Th12: :: EUCLIDLP:12 for a being Real for n being Element of NAT for x, y being Element of REAL n holds ( a * (x - y) = (a * x) + (- (a * y)) & a * (x - y) = (a * x) + ((- a) * y) & a * (x - y) = (a * x) - (a * y) ) proof let a be Real; ::_thesis: for n being Element of NAT for x, y being Element of REAL n holds ( a * (x - y) = (a * x) + (- (a * y)) & a * (x - y) = (a * x) + ((- a) * y) & a * (x - y) = (a * x) - (a * y) ) let n be Element of NAT ; ::_thesis: for x, y being Element of REAL n holds ( a * (x - y) = (a * x) + (- (a * y)) & a * (x - y) = (a * x) + ((- a) * y) & a * (x - y) = (a * x) - (a * y) ) let x, y be Element of REAL n; ::_thesis: ( a * (x - y) = (a * x) + (- (a * y)) & a * (x - y) = (a * x) + ((- a) * y) & a * (x - y) = (a * x) - (a * y) ) thus A1: a * (x - y) = (a * x) + (a * (- y)) by EUCLID_4:6 .= (a * x) + (- (a * y)) by Th3 ; ::_thesis: ( a * (x - y) = (a * x) + ((- a) * y) & a * (x - y) = (a * x) - (a * y) ) hence a * (x - y) = (a * x) + ((- a) * y) by Th3; ::_thesis: a * (x - y) = (a * x) - (a * y) thus a * (x - y) = (a * x) - (a * y) by A1; ::_thesis: verum end; theorem Th13: :: EUCLIDLP:13 for s, t, u being Real for n being Element of NAT for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x) proof let s, t, u be Real; ::_thesis: for n being Element of NAT for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x) let n be Element of NAT ; ::_thesis: for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x) let x be Element of REAL n; ::_thesis: ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x) thus ((s - t) - u) * x = ((s - t) * x) - (u * x) by Th11 .= ((s * x) - (t * x)) - (u * x) by Th11 ; ::_thesis: verum end; theorem Th14: :: EUCLIDLP:14 for a1, a2, a3 being Real for n being Element of NAT for x, x1, x2, x3 being Element of REAL n holds x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3)) proof let a1, a2, a3 be Real; ::_thesis: for n being Element of NAT for x, x1, x2, x3 being Element of REAL n holds x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3)) let n be Element of NAT ; ::_thesis: for x, x1, x2, x3 being Element of REAL n holds x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3)) let x, x1, x2, x3 be Element of REAL n; ::_thesis: x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3)) thus x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + (((- (a1 * x1)) + (- (a2 * x2))) + (- (a3 * x3))) by Th8 .= x + ((((- a1) * x1) + (- (a2 * x2))) + (- (a3 * x3))) by Th3 .= x + ((((- a1) * x1) + ((- a2) * x2)) + (- (a3 * x3))) by Th3 .= x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3)) by Th3 ; ::_thesis: verum end; theorem :: EUCLIDLP:15 for s, t, u being Real for n being Element of NAT for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y) proof let s, t, u be Real; ::_thesis: for n being Element of NAT for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y) let n be Element of NAT ; ::_thesis: for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y) let x, y be Element of REAL n; ::_thesis: x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y) thus x - (((s + t) + u) * y) = x - (((s + t) * y) + (u * y)) by EUCLID_4:7 .= x - (((s * y) + (t * y)) + (u * y)) by EUCLID_4:7 .= x + ((((- s) * y) + ((- t) * y)) + ((- u) * y)) by Th14 .= (x + (((- s) * y) + ((- t) * y))) + ((- u) * y) by RVSUM_1:15 .= ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y) by RVSUM_1:15 ; ::_thesis: verum end; theorem Th16: :: EUCLIDLP:16 for n being Element of NAT for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2) proof let n be Element of NAT ; ::_thesis: for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2) let x1, x2, y1, y2 be Element of REAL n; ::_thesis: (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2) thus (x1 + x2) + (y1 + y2) = ((x1 + x2) + y1) + y2 by RVSUM_1:15 .= ((x1 + y1) + x2) + y2 by RVSUM_1:15 .= (x1 + y1) + (x2 + y2) by RVSUM_1:15 ; ::_thesis: verum end; theorem Th17: :: EUCLIDLP:17 for n being Element of NAT for x1, x2, x3, y1, y2, y3 being Element of REAL n holds ((x1 + x2) + x3) + ((y1 + y2) + y3) = ((x1 + y1) + (x2 + y2)) + (x3 + y3) proof let n be Element of NAT ; ::_thesis: for x1, x2, x3, y1, y2, y3 being Element of REAL n holds ((x1 + x2) + x3) + ((y1 + y2) + y3) = ((x1 + y1) + (x2 + y2)) + (x3 + y3) let x1, x2, x3, y1, y2, y3 be Element of REAL n; ::_thesis: ((x1 + x2) + x3) + ((y1 + y2) + y3) = ((x1 + y1) + (x2 + y2)) + (x3 + y3) thus ((x1 + x2) + x3) + ((y1 + y2) + y3) = ((x1 + x2) + (y1 + y2)) + (x3 + y3) by Th16 .= ((x1 + y1) + (x2 + y2)) + (x3 + y3) by Th16 ; ::_thesis: verum end; theorem Th18: :: EUCLIDLP:18 for n being Element of NAT for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) - (y1 + y2) = (x1 - y1) + (x2 - y2) proof let n be Element of NAT ; ::_thesis: for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) - (y1 + y2) = (x1 - y1) + (x2 - y2) let x1, x2, y1, y2 be Element of REAL n; ::_thesis: (x1 + x2) - (y1 + y2) = (x1 - y1) + (x2 - y2) thus (x1 + x2) - (y1 + y2) = ((x1 + x2) - y1) - y2 by RVSUM_1:39 .= (x1 + x2) + ((- y1) + (- y2)) by RVSUM_1:15 .= (x1 - y1) + (x2 - y2) by Th16 ; ::_thesis: verum end; theorem :: EUCLIDLP:19 for n being Element of NAT for x1, x2, x3, y1, y2, y3 being Element of REAL n holds ((x1 + x2) + x3) - ((y1 + y2) + y3) = ((x1 - y1) + (x2 - y2)) + (x3 - y3) proof let n be Element of NAT ; ::_thesis: for x1, x2, x3, y1, y2, y3 being Element of REAL n holds ((x1 + x2) + x3) - ((y1 + y2) + y3) = ((x1 - y1) + (x2 - y2)) + (x3 - y3) let x1, x2, x3, y1, y2, y3 be Element of REAL n; ::_thesis: ((x1 + x2) + x3) - ((y1 + y2) + y3) = ((x1 - y1) + (x2 - y2)) + (x3 - y3) thus ((x1 + x2) + x3) - ((y1 + y2) + y3) = ((x1 + x2) - (y1 + y2)) + (x3 - y3) by Th18 .= ((x1 - y1) + (x2 - y2)) + (x3 - y3) by Th18 ; ::_thesis: verum end; theorem Th20: :: EUCLIDLP:20 for a being Real for n being Element of NAT for x1, x2, x3 being Element of REAL n holds a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3) proof let a be Real; ::_thesis: for n being Element of NAT for x1, x2, x3 being Element of REAL n holds a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3) let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3) let x1, x2, x3 be Element of REAL n; ::_thesis: a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3) thus a * ((x1 + x2) + x3) = (a * (x1 + x2)) + (a * x3) by EUCLID_4:6 .= ((a * x1) + (a * x2)) + (a * x3) by EUCLID_4:6 ; ::_thesis: verum end; theorem Th21: :: EUCLIDLP:21 for a, b1, b2 being Real for n being Element of NAT for x1, x2 being Element of REAL n holds a * ((b1 * x1) + (b2 * x2)) = ((a * b1) * x1) + ((a * b2) * x2) proof let a, b1, b2 be Real; ::_thesis: for n being Element of NAT for x1, x2 being Element of REAL n holds a * ((b1 * x1) + (b2 * x2)) = ((a * b1) * x1) + ((a * b2) * x2) let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n holds a * ((b1 * x1) + (b2 * x2)) = ((a * b1) * x1) + ((a * b2) * x2) let x1, x2 be Element of REAL n; ::_thesis: a * ((b1 * x1) + (b2 * x2)) = ((a * b1) * x1) + ((a * b2) * x2) thus a * ((b1 * x1) + (b2 * x2)) = (a * (b1 * x1)) + (a * (b2 * x2)) by EUCLID_4:6 .= ((a * b1) * x1) + (a * (b2 * x2)) by EUCLID_4:4 .= ((a * b1) * x1) + ((a * b2) * x2) by EUCLID_4:4 ; ::_thesis: verum end; theorem Th22: :: EUCLIDLP:22 for a, b1, b2, b3 being Real for n being Element of NAT for x1, x2, x3 being Element of REAL n holds a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3) proof let a, b1, b2, b3 be Real; ::_thesis: for n being Element of NAT for x1, x2, x3 being Element of REAL n holds a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3) let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3) let x1, x2, x3 be Element of REAL n; ::_thesis: a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3) thus a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = ((a * (b1 * x1)) + (a * (b2 * x2))) + (a * (b3 * x3)) by Th20 .= (((a * b1) * x1) + (a * (b2 * x2))) + (a * (b3 * x3)) by EUCLID_4:4 .= (((a * b1) * x1) + ((a * b2) * x2)) + (a * (b3 * x3)) by EUCLID_4:4 .= (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3) by EUCLID_4:4 ; ::_thesis: verum end; theorem Th23: :: EUCLIDLP:23 for a1, a2, b1, b2 being Real for n being Element of NAT for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2)) = ((a1 + b1) * x1) + ((a2 + b2) * x2) proof let a1, a2, b1, b2 be Real; ::_thesis: for n being Element of NAT for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2)) = ((a1 + b1) * x1) + ((a2 + b2) * x2) let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2)) = ((a1 + b1) * x1) + ((a2 + b2) * x2) let x1, x2 be Element of REAL n; ::_thesis: ((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2)) = ((a1 + b1) * x1) + ((a2 + b2) * x2) thus ((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2)) = ((a1 * x1) + (b1 * x1)) + ((a2 * x2) + (b2 * x2)) by Th16 .= ((a1 + b1) * x1) + ((a2 * x2) + (b2 * x2)) by EUCLID_4:7 .= ((a1 + b1) * x1) + ((a2 + b2) * x2) by EUCLID_4:7 ; ::_thesis: verum end; theorem Th24: :: EUCLIDLP:24 for a1, a2, a3, b1, b2, b3 being Real for n being Element of NAT for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3) proof let a1, a2, a3, b1, b2, b3 be Real; ::_thesis: for n being Element of NAT for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3) let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3) let x1, x2, x3 be Element of REAL n; ::_thesis: (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3) thus (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2))) + ((a3 * x3) + (b3 * x3)) by Th16 .= (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 * x3) + (b3 * x3)) by Th23 .= (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3) by EUCLID_4:7 ; ::_thesis: verum end; theorem Th25: :: EUCLIDLP:25 for a1, a2, b1, b2 being Real for n being Element of NAT for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2) proof let a1, a2, b1, b2 be Real; ::_thesis: for n being Element of NAT for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2) let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2) let x1, x2 be Element of REAL n; ::_thesis: ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2) thus ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 * x1) - (b1 * x1)) + ((a2 * x2) - (b2 * x2)) by Th18 .= ((a1 - b1) * x1) + ((a2 * x2) - (b2 * x2)) by Th11 .= ((a1 - b1) * x1) + ((a2 - b2) * x2) by Th11 ; ::_thesis: verum end; theorem Th26: :: EUCLIDLP:26 for a1, a2, a3, b1, b2, b3 being Real for n being Element of NAT for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3) proof let a1, a2, a3, b1, b2, b3 be Real; ::_thesis: for n being Element of NAT for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3) let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3) let x1, x2, x3 be Element of REAL n; ::_thesis: (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3) thus (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2))) + ((a3 * x3) - (b3 * x3)) by Th18 .= (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 * x3) - (b3 * x3)) by Th25 .= (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3) by Th11 ; ::_thesis: verum end; theorem Th27: :: EUCLIDLP:27 for a1, a2, a3 being Real for n being Element of NAT for x1, x2, x3 being Element of REAL n st (a1 + a2) + a3 = 1 holds ((a1 * x1) + (a2 * x2)) + (a3 * x3) = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) proof let a1, a2, a3 be Real; ::_thesis: for n being Element of NAT for x1, x2, x3 being Element of REAL n st (a1 + a2) + a3 = 1 holds ((a1 * x1) + (a2 * x2)) + (a3 * x3) = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n st (a1 + a2) + a3 = 1 holds ((a1 * x1) + (a2 * x2)) + (a3 * x3) = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) let x1, x2, x3 be Element of REAL n; ::_thesis: ( (a1 + a2) + a3 = 1 implies ((a1 * x1) + (a2 * x2)) + (a3 * x3) = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) ) assume (a1 + a2) + a3 = 1 ; ::_thesis: ((a1 * x1) + (a2 * x2)) + (a3 * x3) = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) then a1 = (1 - a2) - a3 ; hence ((a1 * x1) + (a2 * x2)) + (a3 * x3) = ((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by Th13 .= (((x1 + (- (a2 * x1))) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by EUCLID_4:3 .= (((x1 + (- (a2 * x1))) + (a2 * x2)) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15 .= ((x1 + ((a2 * x2) + (- (a2 * x1)))) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15 .= (x1 + ((a2 * x2) + (- (a2 * x1)))) + ((a3 * x3) + (- (a3 * x1))) by RVSUM_1:15 .= (x1 + (a2 * (x2 - x1))) + ((a3 * x3) + (- (a3 * x1))) by Th12 .= (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) by Th12 ; ::_thesis: verum end; theorem Th28: :: EUCLIDLP:28 for a2, a3 being Real for n being Element of NAT for x, x1, x2, x3 being Element of REAL n st x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) holds ex a1 being Real st ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) proof let a2, a3 be Real; ::_thesis: for n being Element of NAT for x, x1, x2, x3 being Element of REAL n st x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) holds ex a1 being Real st ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) let n be Element of NAT ; ::_thesis: for x, x1, x2, x3 being Element of REAL n st x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) holds ex a1 being Real st ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) let x, x1, x2, x3 be Element of REAL n; ::_thesis: ( x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) implies ex a1 being Real st ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) ) assume A1: x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) ; ::_thesis: ex a1 being Real st ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) reconsider a1 = (1 - a2) - a3 as Real ; take a1 ; ::_thesis: ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) ((a1 * x1) + (a2 * x2)) + (a3 * x3) = ((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by Th13 .= (((x1 + (- (a2 * x1))) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by EUCLID_4:3 .= (((x1 + (- (a2 * x1))) + (a2 * x2)) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15 .= ((x1 + ((a2 * x2) + (- (a2 * x1)))) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15 .= (x1 + ((a2 * x2) + (- (a2 * x1)))) + ((a3 * x3) + (- (a3 * x1))) by RVSUM_1:15 .= (x1 + (a2 * (x2 - x1))) + ((a3 * x3) + (- (a3 * x1))) by Th12 .= x by A1, Th12 ; hence ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) ; ::_thesis: verum end; theorem :: EUCLIDLP:29 for n being Element of NAT st n >= 1 holds 1* n <> 0* n proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies 1* n <> 0* n ) assume n >= 1 ; ::_thesis: 1* n <> 0* n then A1: 1 in Seg n by FINSEQ_1:1; assume A2: 1* n = 0* n ; ::_thesis: contradiction ( 1* n = n |-> 1 & (n |-> 0) . 1 = 0 ) by A1, FUNCOP_1:7; hence contradiction by A2, A1, FUNCOP_1:7; ::_thesis: verum end; theorem Th30: :: EUCLIDLP:30 for n being Element of NAT for A being Subset of (REAL n) for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds A = Line (x1,x2) proof let n be Element of NAT ; ::_thesis: for A being Subset of (REAL n) for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds A = Line (x1,x2) let A be Subset of (REAL n); ::_thesis: for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds A = Line (x1,x2) let x1, x2 be Element of REAL n; ::_thesis: ( A is being_line & x1 in A & x2 in A & x1 <> x2 implies A = Line (x1,x2) ) assume that A1: A is being_line and A2: ( x1 in A & x2 in A & x1 <> x2 ) ; ::_thesis: A = Line (x1,x2) ex y1, y2 being Element of REAL n st ( y1 <> y2 & A = Line (y1,y2) ) by A1, EUCLID_4:def_2; then ( Line (x1,x2) c= A & A c= Line (x1,x2) ) by A2, EUCLID_4:10, EUCLID_4:11; hence A = Line (x1,x2) by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th31: :: EUCLIDLP:31 for n being Element of NAT for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds ex a being Real st y2 - y1 = a * (x2 - x1) proof let n be Element of NAT ; ::_thesis: for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds ex a being Real st y2 - y1 = a * (x2 - x1) let y1, y2 be Element of REAL n; ::_thesis: for x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds ex a being Real st y2 - y1 = a * (x2 - x1) let x1, x2 be Element of REAL n; ::_thesis: ( y1 in Line (x1,x2) & y2 in Line (x1,x2) implies ex a being Real st y2 - y1 = a * (x2 - x1) ) assume y1 in Line (x1,x2) ; ::_thesis: ( not y2 in Line (x1,x2) or ex a being Real st y2 - y1 = a * (x2 - x1) ) then consider t being Real such that A1: y1 = ((1 - t) * x1) + (t * x2) ; assume y2 in Line (x1,x2) ; ::_thesis: ex a being Real st y2 - y1 = a * (x2 - x1) then consider s being Real such that A2: y2 = ((1 - s) * x1) + (s * x2) ; take s - t ; ::_thesis: y2 - y1 = (s - t) * (x2 - x1) y2 - y1 = ((((1 - s) * x1) + (s * x2)) - ((1 - t) * x1)) - (t * x2) by A1, A2, RVSUM_1:39 .= (((s * x2) + ((1 - s) * x1)) + (- (t * x2))) + (- ((1 - t) * x1)) by RVSUM_1:15 .= (((s * x2) + (- (t * x2))) + ((1 - s) * x1)) + (- ((1 - t) * x1)) by RVSUM_1:15 .= (((s - t) * x2) + ((1 - s) * x1)) + (- ((1 - t) * x1)) by Th11 .= ((s - t) * x2) + (((1 - s) * x1) + (- ((1 - t) * x1))) by RVSUM_1:15 .= ((s - t) * x2) + (((1 - s) - (1 - t)) * x1) by Th11 .= ((s - t) * x2) + ((- (s - t)) * x1) .= (s - t) * (x2 - x1) by Th12 ; hence y2 - y1 = (s - t) * (x2 - x1) ; ::_thesis: verum end; definition let n be Element of NAT ; let x1, x2 be Element of REAL n; predx1 // x2 means :Def1: :: EUCLIDLP:def 1 ( x1 <> 0* n & x2 <> 0* n & ex r being Real st x1 = r * x2 ); end; :: deftheorem Def1 defines // EUCLIDLP:def_1_:_ for n being Element of NAT for x1, x2 being Element of REAL n holds ( x1 // x2 iff ( x1 <> 0* n & x2 <> 0* n & ex r being Real st x1 = r * x2 ) ); theorem Th32: :: EUCLIDLP:32 for n being Element of NAT for x1, x2 being Element of REAL n st x1 // x2 holds ex a being Real st ( a <> 0 & x1 = a * x2 ) proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1 // x2 holds ex a being Real st ( a <> 0 & x1 = a * x2 ) let x1, x2 be Element of REAL n; ::_thesis: ( x1 // x2 implies ex a being Real st ( a <> 0 & x1 = a * x2 ) ) assume A1: x1 // x2 ; ::_thesis: ex a being Real st ( a <> 0 & x1 = a * x2 ) then consider a being Real such that A2: x1 = a * x2 by Def1; x1 <> 0* n by A1, Def1; then a <> 0 by A2, EUCLID_4:3; hence ex a being Real st ( a <> 0 & x1 = a * x2 ) by A2; ::_thesis: verum end; definition let n be Element of NAT ; let x1, x2 be Element of REAL n; :: original: // redefine predx1 // x2; symmetry for x1, x2 being Element of REAL n st (n,b1,b2) holds (n,b2,b1) proof let x1, x2 be Element of REAL n; ::_thesis: ( (n,x1,x2) implies (n,x2,x1) ) assume A1: x1 // x2 ; ::_thesis: (n,x2,x1) then A2: ( x1 <> 0* n & x2 <> 0* n ) by Def1; consider a being Real such that A3: a <> 0 and A4: x1 = a * x2 by A1, Th32; (1 / a) * x1 = (a / a) * x2 by A4, Th1 .= 1 * x2 by A3, XCMPLX_1:60 .= x2 by EUCLID_4:3 ; hence (n,x2,x1) by A2, Def1; ::_thesis: verum end; end; theorem Th33: :: EUCLIDLP:33 for n being Element of NAT for x1, x2, x3 being Element of REAL n st x1 // x2 & x2 // x3 holds x1 // x3 proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n st x1 // x2 & x2 // x3 holds x1 // x3 let x1, x2, x3 be Element of REAL n; ::_thesis: ( x1 // x2 & x2 // x3 implies x1 // x3 ) assume that A1: x1 // x2 and A2: x2 // x3 ; ::_thesis: x1 // x3 A3: ex t being Real st x1 = t * x3 proof consider b being Real such that A4: x2 = b * x3 by A2, Def1; consider a being Real such that A5: x1 = a * x2 by A1, Def1; x1 = (a * b) * x3 by A5, A4, EUCLID_4:4; hence ex t being Real st x1 = t * x3 ; ::_thesis: verum end; ( x1 <> 0* n & x3 <> 0* n ) by A1, A2, Def1; hence x1 // x3 by A3, Def1; ::_thesis: verum end; definition let n be Element of NAT ; let x1, x2 be Element of REAL n; predx1,x2 are_lindependent2 means :Def2: :: EUCLIDLP:def 2 for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds ( a1 = 0 & a2 = 0 ); symmetry for x1, x2 being Element of REAL n st ( for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds ( a1 = 0 & a2 = 0 ) ) holds for a1, a2 being Real st (a1 * x2) + (a2 * x1) = 0* n holds ( a1 = 0 & a2 = 0 ) ; end; :: deftheorem Def2 defines are_lindependent2 EUCLIDLP:def_2_:_ for n being Element of NAT for x1, x2 being Element of REAL n holds ( x1,x2 are_lindependent2 iff for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds ( a1 = 0 & a2 = 0 ) ); notation let n be Element of NAT ; let x1, x2 be Element of REAL n; antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2 ; end; Lm2: for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds x1 <> 0* n proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds x1 <> 0* n let x1, x2 be Element of REAL n; ::_thesis: ( x1,x2 are_lindependent2 implies x1 <> 0* n ) assume that A1: x1,x2 are_lindependent2 and A2: not x1 <> 0* n ; ::_thesis: contradiction 1 * x1 = 0* n by A2, EUCLID_4:2; then (1 * x1) + (0 * x2) = (0* n) + (0* n) by EUCLID_4:3 .= 0* n by EUCLID_4:1 ; hence contradiction by A1, Def2; ::_thesis: verum end; theorem :: EUCLIDLP:34 for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds ( x1 <> 0* n & x2 <> 0* n ) by Lm2; theorem Th35: :: EUCLIDLP:35 for a1, a2, b1, b2 being Real for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) holds ( a1 = b1 & a2 = b2 ) proof let a1, a2, b1, b2 be Real; ::_thesis: for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) holds ( a1 = b1 & a2 = b2 ) let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) holds ( a1 = b1 & a2 = b2 ) let x1, x2 be Element of REAL n; ::_thesis: ( x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) implies ( a1 = b1 & a2 = b2 ) ) assume A1: x1,x2 are_lindependent2 ; ::_thesis: ( not (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) or ( a1 = b1 & a2 = b2 ) ) assume A2: (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) ; ::_thesis: ( a1 = b1 & a2 = b2 ) 0* n = ((a1 * x1) + (a2 * x2)) - ((a1 * x1) + (a2 * x2)) by Th2 .= ((a1 - b1) * x1) + ((a2 - b2) * x2) by A2, Th25 ; then ( a1 - b1 = 0 & a2 - b2 = 0 ) by A1, Def2; hence ( a1 = b1 & a2 = b2 ) ; ::_thesis: verum end; theorem Th36: :: EUCLIDLP:36 for a1, a2, b1, b2 being Real for n being Element of NAT for y2, x1, x2, y1, y1 being Element of REAL n st y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) holds ex c1, c2, d1, d2 being Real st ( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) proof let a1, a2, b1, b2 be Real; ::_thesis: for n being Element of NAT for y2, x1, x2, y1, y1 being Element of REAL n st y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) holds ex c1, c2, d1, d2 being Real st ( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) let n be Element of NAT ; ::_thesis: for y2, x1, x2, y1, y1 being Element of REAL n st y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) holds ex c1, c2, d1, d2 being Real st ( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) let y2, x1, x2, y1, y1 be Element of REAL n; ::_thesis: ( y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) implies ex c1, c2, d1, d2 being Real st ( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) ) assume A1: y1,y2 are_lindependent2 ; ::_thesis: ( not y1 = (a1 * x1) + (a2 * x2) or not y2 = (b1 * x1) + (b2 * x2) or ex c1, c2, d1, d2 being Real st ( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) ) assume that A2: y1 = (a1 * x1) + (a2 * x2) and A3: y2 = (b1 * x1) + (b2 * x2) ; ::_thesis: ex c1, c2, d1, d2 being Real st ( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) A4: (- (b1 * y1)) + (a1 * y2) = ((- b1) * ((a1 * x1) + (a2 * x2))) + (a1 * ((b1 * x1) + (b2 * x2))) by A2, A3, Th3 .= ((((- b1) * a1) * x1) + (((- b1) * a2) * x2)) + (a1 * ((b1 * x1) + (b2 * x2))) by Th21 .= (((- (a1 * b1)) * x1) + ((- (a2 * b1)) * x2)) + (((a1 * b1) * x1) + ((a1 * b2) * x2)) by Th21 .= (((- (a1 * b1)) + (a1 * b1)) * x1) + (((- (a2 * b1)) + (a1 * b2)) * x2) by Th23 .= (0* n) + (((- (a2 * b1)) + (a1 * b2)) * x2) by EUCLID_4:3 .= ((a1 * b2) - (a2 * b1)) * x2 by EUCLID_4:1 ; A5: (b2 * y1) - (a2 * y2) = (((a1 * b2) * x1) + ((a2 * b2) * x2)) - (a2 * ((b1 * x1) + (b2 * x2))) by A2, A3, Th21 .= (((a1 * b2) * x1) + ((a2 * b2) * x2)) - (((a2 * b1) * x1) + ((a2 * b2) * x2)) by Th21 .= (((a1 * b2) - (a2 * b1)) * x1) + (((a2 * b2) - (a2 * b2)) * x2) by Th25 .= (((a1 * b2) - (a2 * b1)) * x1) + (0* n) by EUCLID_4:3 .= ((a1 * b2) - (a2 * b1)) * x1 by EUCLID_4:1 ; A6: (a1 * b2) - (a2 * b1) <> 0 proof assume not (a1 * b2) - (a2 * b1) <> 0 ; ::_thesis: contradiction then A7: (b2 * y1) + ((- a2) * y2) = 0 * x1 by A5, Th3 .= 0* n by EUCLID_4:3 ; then A8: y2 = (b1 * x1) + (0 * x2) by A1, A3, Def2 .= (b1 * x1) + (0* n) by EUCLID_4:3 .= b1 * x1 by EUCLID_4:1 ; A9: - a2 = 0 by A1, A7, Def2; then y1 = (a1 * x1) + (0* n) by A2, EUCLID_4:3 .= a1 * x1 by EUCLID_4:1 ; then (b1 * y1) + ((- a1) * y2) = ((a1 * b1) * x1) + ((- a1) * (b1 * x1)) by A8, EUCLID_4:4 .= ((a1 * b1) * x1) + (((- a1) * b1) * x1) by EUCLID_4:4 .= ((a1 * b1) + ((- a1) * b1)) * x1 by EUCLID_4:7 .= 0* n by EUCLID_4:3 ; then - a1 = 0 by A1, Def2; then y1 = (0* n) + (0 * x2) by A2, A9, EUCLID_4:3 .= (0* n) + (0* n) by EUCLID_4:3 .= 0* n by EUCLID_4:1 ; hence contradiction by A1, Lm2; ::_thesis: verum end; A10: x2 = 1 * x2 by EUCLID_4:3 .= ((1 / ((a1 * b2) - (a2 * b1))) * ((a1 * b2) - (a2 * b1))) * x2 by A6, XCMPLX_1:106 .= (1 / ((a1 * b2) - (a2 * b1))) * (((a1 * b2) - (a2 * b1)) * x2) by EUCLID_4:4 .= ((1 / ((a1 * b2) - (a2 * b1))) * (- (b1 * y1))) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2)) by A4, EUCLID_4:6 .= ((1 / ((a1 * b2) - (a2 * b1))) * ((- b1) * y1)) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2)) by Th3 .= (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2)) by Th1 .= (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((a1 / ((a1 * b2) - (a2 * b1))) * y2) by Th1 ; set d2 = a1 / ((a1 * b2) - (a2 * b1)); set d1 = (- b1) / ((a1 * b2) - (a2 * b1)); set c2 = (- a2) / ((a1 * b2) - (a2 * b1)); set c1 = b2 / ((a1 * b2) - (a2 * b1)); take b2 / ((a1 * b2) - (a2 * b1)) ; ::_thesis: ex c2, d1, d2 being Real st ( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) ) take (- a2) / ((a1 * b2) - (a2 * b1)) ; ::_thesis: ex d1, d2 being Real st ( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (d1 * y1) + (d2 * y2) ) take (- b1) / ((a1 * b2) - (a2 * b1)) ; ::_thesis: ex d2 being Real st ( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + (d2 * y2) ) take a1 / ((a1 * b2) - (a2 * b1)) ; ::_thesis: ( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((a1 / ((a1 * b2) - (a2 * b1))) * y2) ) x1 = 1 * x1 by EUCLID_4:3 .= ((1 / ((a1 * b2) - (a2 * b1))) * ((a1 * b2) - (a2 * b1))) * x1 by A6, XCMPLX_1:106 .= (1 / ((a1 * b2) - (a2 * b1))) * (((a1 * b2) - (a2 * b1)) * x1) by EUCLID_4:4 .= ((1 / ((a1 * b2) - (a2 * b1))) * (b2 * y1)) - ((1 / ((a1 * b2) - (a2 * b1))) * (a2 * y2)) by A5, Th12 .= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) - ((1 / ((a1 * b2) - (a2 * b1))) * (a2 * y2)) by Th1 .= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (- (((1 / ((a1 * b2) - (a2 * b1))) * a2) * y2)) by EUCLID_4:4 .= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + ((- ((1 / ((a1 * b2) - (a2 * b1))) * a2)) * y2) by Th3 .= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((1 / ((a1 * b2) - (a2 * b1))) * (- a2)) * y2) .= ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) by XCMPLX_1:99 ; hence ( x1 = ((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((- a2) / ((a1 * b2) - (a2 * b1))) * y2) & x2 = (((- b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((a1 / ((a1 * b2) - (a2 * b1))) * y2) ) by A10; ::_thesis: verum end; theorem Th37: :: EUCLIDLP:37 for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds x1 <> x2 proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds x1 <> x2 let x1, x2 be Element of REAL n; ::_thesis: ( x1,x2 are_lindependent2 implies x1 <> x2 ) assume A1: x1,x2 are_lindependent2 ; ::_thesis: x1 <> x2 assume A2: x1 = x2 ; ::_thesis: contradiction (1 * x1) + ((- 1) * x2) = 1 * (x1 - x2) by Th12 .= 1 * (0* n) by A2, Th2 .= 0* n by EUCLID_4:2 ; hence contradiction by A1, Def2; ::_thesis: verum end; theorem :: EUCLIDLP:38 for n being Element of NAT for x2, x1, x3 being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 holds x2 <> x3 by Th37; theorem :: EUCLIDLP:39 for t being Real for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds x1 + (t * x2),x2 are_lindependent2 proof let t be Real; ::_thesis: for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds x1 + (t * x2),x2 are_lindependent2 let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds x1 + (t * x2),x2 are_lindependent2 let x1, x2 be Element of REAL n; ::_thesis: ( x1,x2 are_lindependent2 implies x1 + (t * x2),x2 are_lindependent2 ) assume A1: x1,x2 are_lindependent2 ; ::_thesis: x1 + (t * x2),x2 are_lindependent2 for a, b being Real st (a * (x1 + (t * x2))) + (b * x2) = 0* n holds ( a = 0 & b = 0 ) proof let a, b be Real; ::_thesis: ( (a * (x1 + (t * x2))) + (b * x2) = 0* n implies ( a = 0 & b = 0 ) ) assume (a * (x1 + (t * x2))) + (b * x2) = 0* n ; ::_thesis: ( a = 0 & b = 0 ) then A2: 0* n = (a * ((1 * x1) + (t * x2))) + (b * x2) by EUCLID_4:3 .= (((a * 1) * x1) + ((a * t) * x2)) + (b * x2) by Th21 .= (a * x1) + (((a * t) * x2) + (b * x2)) by RVSUM_1:15 .= (a * x1) + (((a * t) + b) * x2) by EUCLID_4:7 ; then a = 0 by A1, Def2; hence ( a = 0 & b = 0 ) by A1, A2, Def2; ::_thesis: verum end; hence x1 + (t * x2),x2 are_lindependent2 by Def2; ::_thesis: verum end; theorem Th40: :: EUCLIDLP:40 for n being Element of NAT for x1, x0, x3, x2, y0, y1, y2, y3 being Element of REAL n st x1 - x0,x3 - x2 are_lindependent2 & y0 in Line (x0,x1) & y1 in Line (x0,x1) & y0 <> y1 & y2 in Line (x2,x3) & y3 in Line (x2,x3) & y2 <> y3 holds y1 - y0,y3 - y2 are_lindependent2 proof let n be Element of NAT ; ::_thesis: for x1, x0, x3, x2, y0, y1, y2, y3 being Element of REAL n st x1 - x0,x3 - x2 are_lindependent2 & y0 in Line (x0,x1) & y1 in Line (x0,x1) & y0 <> y1 & y2 in Line (x2,x3) & y3 in Line (x2,x3) & y2 <> y3 holds y1 - y0,y3 - y2 are_lindependent2 let x1, x0, x3, x2, y0, y1, y2, y3 be Element of REAL n; ::_thesis: ( x1 - x0,x3 - x2 are_lindependent2 & y0 in Line (x0,x1) & y1 in Line (x0,x1) & y0 <> y1 & y2 in Line (x2,x3) & y3 in Line (x2,x3) & y2 <> y3 implies y1 - y0,y3 - y2 are_lindependent2 ) assume that A1: x1 - x0,x3 - x2 are_lindependent2 and A2: ( y0 in Line (x0,x1) & y1 in Line (x0,x1) ) and A3: y0 <> y1 and A4: ( y2 in Line (x2,x3) & y3 in Line (x2,x3) ) and A5: y2 <> y3 ; ::_thesis: y1 - y0,y3 - y2 are_lindependent2 consider s being Real such that A6: y1 - y0 = s * (x1 - x0) by A2, Th31; consider t being Real such that A7: y3 - y2 = t * (x3 - x2) by A4, Th31; for a, b being Real st (a * (y1 - y0)) + (b * (y3 - y2)) = 0* n holds ( a = 0 & b = 0 ) proof let a, b be Real; ::_thesis: ( (a * (y1 - y0)) + (b * (y3 - y2)) = 0* n implies ( a = 0 & b = 0 ) ) assume (a * (y1 - y0)) + (b * (y3 - y2)) = 0* n ; ::_thesis: ( a = 0 & b = 0 ) then A8: 0* n = ((a * s) * (x1 - x0)) + (b * (t * (x3 - x2))) by A6, A7, EUCLID_4:4 .= ((a * s) * (x1 - x0)) + ((b * t) * (x3 - x2)) by EUCLID_4:4 ; then A9: a * s = 0 by A1, Def2; A10: b * t = 0 by A1, A8, Def2; A11: b = (b * t) / t by A5, A7, Th10, XCMPLX_1:89 .= 0 by A10 ; a = (a * s) / s by A3, A6, Th10, XCMPLX_1:89 .= 0 by A9 ; hence ( a = 0 & b = 0 ) by A11; ::_thesis: verum end; hence y1 - y0,y3 - y2 are_lindependent2 by Def2; ::_thesis: verum end; Lm3: for n being Element of NAT for x1, x2 being Element of REAL n st x1 // x2 holds x1,x2 are_ldependent2 proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1 // x2 holds x1,x2 are_ldependent2 let x1, x2 be Element of REAL n; ::_thesis: ( x1 // x2 implies x1,x2 are_ldependent2 ) assume x1 // x2 ; ::_thesis: x1,x2 are_ldependent2 then consider r being Real such that A1: x1 = r * x2 by Def1; assume A2: x1,x2 are_lindependent2 ; ::_thesis: contradiction 0* n = x1 - x1 by Th2 .= (1 * x1) + (- (r * x2)) by A1, EUCLID_4:3 .= (1 * x1) + ((- r) * x2) by Th3 ; hence contradiction by A2, Def2; ::_thesis: verum end; theorem :: EUCLIDLP:41 for n being Element of NAT for x1, x2 being Element of REAL n st x1 // x2 holds ( x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n ) by Def1, Lm3; Lm4: for n being Element of NAT for x1, x2 being Element of REAL n st x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n holds x1 // x2 proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n holds x1 // x2 let x1, x2 be Element of REAL n; ::_thesis: ( x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n implies x1 // x2 ) assume that A1: x1,x2 are_ldependent2 and A2: ( x1 <> 0* n & x2 <> 0* n ) ; ::_thesis: x1 // x2 consider a1, a2 being Real such that A3: (a1 * x1) + (a2 * x2) = 0* n and A4: ( a1 <> 0 or a2 <> 0 ) by A1, Def2; now__::_thesis:_(_(_a1_<>_0_&_ex_t_being_Element_of_REAL_st_x1_//_x2_)_or_(_a2_<>_0_&_ex_s_being_Element_of_REAL_st_x1_//_x2_)_) percases ( a1 <> 0 or a2 <> 0 ) by A4; caseA5: a1 <> 0 ; ::_thesis: ex t being Element of REAL st x1 // x2 set t = (- a2) / a1; take t = (- a2) / a1; ::_thesis: x1 // x2 A6: a1 * x1 = (0* n) - (a2 * x2) by A3, Th6 .= - (a2 * x2) by RVSUM_1:33 ; x1 = 1 * x1 by EUCLID_4:3 .= (a1 / a1) * x1 by A5, XCMPLX_1:60 .= (1 / a1) * (a1 * x1) by Th1 .= (1 / a1) * ((- a2) * x2) by A6, Th3 .= ((- a2) / a1) * x2 by Th1 ; hence x1 // x2 by A2, Def1; ::_thesis: verum end; caseA7: a2 <> 0 ; ::_thesis: ex s being Element of REAL st x1 // x2 set s = (- a1) / a2; take s = (- a1) / a2; ::_thesis: x1 // x2 A8: a2 * x2 = (0* n) - (a1 * x1) by A3, Th6 .= - (a1 * x1) by RVSUM_1:33 ; x2 = 1 * x2 by EUCLID_4:3 .= (a2 / a2) * x2 by A7, XCMPLX_1:60 .= (1 / a2) * (a2 * x2) by Th1 .= (1 / a2) * ((- a1) * x1) by A8, Th3 .= ((- a1) / a2) * x1 by Th1 ; hence x1 // x2 by A2, Def1; ::_thesis: verum end; end; end; hence x1 // x2 ; ::_thesis: verum end; theorem :: EUCLIDLP:42 for n being Element of NAT for x1, x2 being Element of REAL n holds ( not x1,x2 are_ldependent2 or x1 = 0* n or x2 = 0* n or x1 // x2 ) by Lm4; theorem Th43: :: EUCLIDLP:43 for n being Element of NAT for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) proof let n be Element of NAT ; ::_thesis: for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) let x1, x2, y1 be Element of REAL n; ::_thesis: ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) now__::_thesis:_(_(_x1_<>_x2_&_((1_-_(-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2))))_*_x1)_+_((-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2)))_*_x2)_in_Line_(x1,x2)_&_x1_-_x2,y1_-_(((1_-_(-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2))))_*_x1)_+_((-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2)))_*_x2))_are_orthogonal_)_or_(_x1_=_x2_&_(_for_mu_being_Real_ex_y2_being_Element_of_REAL_n_st_ (_y2_in_Line_(x1,x2)_&_x1_-_x2,y1_-_y2_are_orthogonal_)_)_)_) percases ( x1 <> x2 or x1 = x2 ) ; caseA1: x1 <> x2 ; ::_thesis: ( ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2) in Line (x1,x2) & x1 - x2,y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)) are_orthogonal ) set mu = - (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)); set y2 = ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2); |.(x1 - x2).| <> 0 by A1, Lm1; then A2: |.(x1 - x2).| ^2 <> 0 by SQUARE_1:12; |((x1 - x2),(y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2))))| = |((x1 - x2),((y1 - ((1 + (- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by RVSUM_1:39 .= |((x1 - x2),((y1 - ((1 * x1) + ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1))) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by EUCLID_4:7 .= |((x1 - x2),(((y1 - (1 * x1)) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by RVSUM_1:39 .= |((x1 - x2),(((y1 - x1) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by EUCLID_4:3 .= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2))))| by RVSUM_1:39 .= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + (- ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x2)))))| by Th3 .= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * (- x2)))))| by Th3 .= |((x1 - x2),((y1 - x1) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * (x1 - x2))))| by EUCLID_4:6 .= |((x1 - x2),(y1 - x1))| - |((x1 - x2),((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * (x1 - x2)))| by EUCLID_4:26 .= |((x1 - x2),(y1 - x1))| - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * |((x1 - x2),(x1 - x2))|) by EUCLID_4:21 .= |((x1 - x2),(y1 - x1))| + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * |((x1 - x2),(x1 - x2))|) .= |((x1 - x2),(y1 - x1))| + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * (|.(x1 - x2).| ^2)) by EUCLID_2:4 .= |((x1 - x2),(y1 - x1))| + (((- |((x1 - x2),(y1 - x1))|) / (|.(x1 - x2).| ^2)) * (|.(x1 - x2).| ^2)) by XCMPLX_1:187 .= |((x1 - x2),(y1 - x1))| + (- |((x1 - x2),(y1 - x1))|) by A2, XCMPLX_1:87 .= 0 ; hence ( ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2) in Line (x1,x2) & x1 - x2,y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)) are_orthogonal ) by RVSUM_1:def_17; ::_thesis: verum end; caseA3: x1 = x2 ; ::_thesis: for mu being Real ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) let mu be Real; ::_thesis: ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) set y2 = ((1 - mu) * x1) + (mu * x2); take y2 = ((1 - mu) * x1) + (mu * x2); ::_thesis: ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) x1 - x2 = 0* n by A3, Th2; then |((x1 - x2),(y1 - y2))| = 0 by EUCLID_4:18; hence ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) by RVSUM_1:def_17; ::_thesis: verum end; end; end; hence ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) ; ::_thesis: verum end; definition let n be Element of NAT ; let x1, x2 be Element of REAL n; predx1 _|_ x2 means :Def3: :: EUCLIDLP:def 3 ( x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal ); symmetry for x1, x2 being Element of REAL n st x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal holds ( x2 <> 0* n & x1 <> 0* n & x2,x1 are_orthogonal ) ; end; :: deftheorem Def3 defines _|_ EUCLIDLP:def_3_:_ for n being Element of NAT for x1, x2 being Element of REAL n holds ( x1 _|_ x2 iff ( x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal ) ); theorem Th44: :: EUCLIDLP:44 for n being Element of NAT for x, y0, y1 being Element of REAL n st x _|_ y0 & y0 // y1 holds x _|_ y1 proof let n be Element of NAT ; ::_thesis: for x, y0, y1 being Element of REAL n st x _|_ y0 & y0 // y1 holds x _|_ y1 let x, y0, y1 be Element of REAL n; ::_thesis: ( x _|_ y0 & y0 // y1 implies x _|_ y1 ) assume that A1: x _|_ y0 and A2: y0 // y1 ; ::_thesis: x _|_ y1 A3: x,y0 are_orthogonal by A1, Def3; consider r being Real such that A4: y1 = r * y0 by A2, Def1; |(x,y1)| = r * |(x,y0)| by A4, EUCLID_4:22 .= r * 0 by A3, RVSUM_1:def_17 .= 0 ; then A5: x,y1 are_orthogonal by RVSUM_1:def_17; ( x <> 0* n & y1 <> 0* n ) by A1, A2, Def1, Def3; hence x _|_ y1 by A5, Def3; ::_thesis: verum end; theorem Th45: :: EUCLIDLP:45 for n being Element of NAT for x, y being Element of REAL n st x _|_ y holds x,y are_lindependent2 proof let n be Element of NAT ; ::_thesis: for x, y being Element of REAL n st x _|_ y holds x,y are_lindependent2 let x, y be Element of REAL n; ::_thesis: ( x _|_ y implies x,y are_lindependent2 ) assume A1: x _|_ y ; ::_thesis: x,y are_lindependent2 then x,y are_orthogonal by Def3; then A2: |(x,y)| = 0 by RVSUM_1:def_17; x <> 0* n by A1, Def3; then |(x,x)| <> 0 by EUCLID_4:17; then A3: |(x,x)| > 0 by RVSUM_1:119; y <> 0* n by A1, Def3; then A4: |(y,y)| <> 0 by EUCLID_4:17; then A5: |(y,y)| > 0 by RVSUM_1:119; for a, b being Real st (a * x) + (b * y) = 0* n holds ( a = 0 & b = 0 ) proof let a, b be Real; ::_thesis: ( (a * x) + (b * y) = 0* n implies ( a = 0 & b = 0 ) ) assume (a * x) + (b * y) = 0* n ; ::_thesis: ( a = 0 & b = 0 ) then A6: 0 = |(((a * x) + (b * y)),((a * x) + (b * y)))| by EUCLID_4:17 .= (|((a * x),(a * x))| + (2 * |((a * x),(b * y))|)) + |((b * y),(b * y))| by EUCLID_4:32 .= ((a * |(x,(a * x))|) + (2 * |((a * x),(b * y))|)) + |((b * y),(b * y))| by EUCLID_4:21 .= ((a * |(x,(a * x))|) + (2 * (a * |(x,(b * y))|))) + |((b * y),(b * y))| by EUCLID_4:21 .= ((a * |(x,(a * x))|) + ((2 * a) * |(x,(b * y))|)) + (b * |(y,(b * y))|) by EUCLID_4:21 .= ((a * (a * |(x,x)|)) + ((2 * a) * |(x,(b * y))|)) + (b * |(y,(b * y))|) by EUCLID_4:22 .= (((a * a) * |(x,x)|) + ((2 * a) * (b * |(x,y)|))) + (b * |(y,(b * y))|) by EUCLID_4:22 .= (((a * a) * |(x,x)|) + (((2 * a) * b) * |(x,y)|)) + (b * (b * |(y,y)|)) by EUCLID_4:22 .= ((a * a) * |(x,x)|) + ((b * b) * |(y,y)|) by A2 ; A7: b * b >= 0 by XREAL_1:63; A8: a * a = 0 proof assume a * a <> 0 ; ::_thesis: contradiction then a * a > 0 by XREAL_1:63; then (a * a) * |(x,x)| > 0 by A3, XREAL_1:129; hence contradiction by A5, A6, A7; ::_thesis: verum end; then b * b = 0 by A4, A6, XCMPLX_1:6; hence ( a = 0 & b = 0 ) by A8, XCMPLX_1:6; ::_thesis: verum end; hence x,y are_lindependent2 by Def2; ::_thesis: verum end; theorem :: EUCLIDLP:46 for n being Element of NAT for x1, x2 being Element of REAL n st x1 // x2 holds not x1 _|_ x2 proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n st x1 // x2 holds not x1 _|_ x2 let x1, x2 be Element of REAL n; ::_thesis: ( x1 // x2 implies not x1 _|_ x2 ) assume A1: x1 // x2 ; ::_thesis: not x1 _|_ x2 then consider r being Real such that A2: x1 = r * x2 by Def1; x2 <> 0* n by A1, Def1; then A3: |(x2,x2)| <> 0 by EUCLID_4:17; x1 <> 0* n by A1, Def1; then A4: r <> 0 by A2, EUCLID_4:3; |(x1,x2)| = r * |(x2,x2)| by A2, EUCLID_4:21; then |(x1,x2)| <> 0 by A4, A3, XCMPLX_1:6; then not x1,x2 are_orthogonal by RVSUM_1:def_17; hence not x1 _|_ x2 by Def3; ::_thesis: verum end; definition let n be Element of NAT ; func line_of_REAL n -> Subset-Family of (REAL n) equals :: EUCLIDLP:def 4 { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ; correctness coherence { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } is Subset-Family of (REAL n); proof set A = { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ; { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } c= bool (REAL n) proof let L be set ; :: according to TARSKI:def_3 ::_thesis: ( not L in { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } or L in bool (REAL n) ) assume L in { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ; ::_thesis: L in bool (REAL n) then ex x1, x2 being Element of REAL n st L = Line (x1,x2) ; hence L in bool (REAL n) ; ::_thesis: verum end; hence { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } is Subset-Family of (REAL n) ; ::_thesis: verum end; end; :: deftheorem defines line_of_REAL EUCLIDLP:def_4_:_ for n being Element of NAT holds line_of_REAL n = { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ; registration let n be Element of NAT ; cluster line_of_REAL n -> non empty ; coherence not line_of_REAL n is empty proof reconsider L = Line ((0* n),(1* n)) as Subset of (REAL n) ; L in line_of_REAL n ; hence not line_of_REAL n is empty ; ::_thesis: verum end; end; theorem Th47: :: EUCLIDLP:47 for n being Element of NAT for x1, x2 being Element of REAL n holds Line (x1,x2) in line_of_REAL n ; theorem Th48: :: EUCLIDLP:48 for n being Element of NAT for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L holds Line (x1,x2) c= L proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L holds Line (x1,x2) c= L let x1, x2 be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L holds Line (x1,x2) c= L let L be Element of line_of_REAL n; ::_thesis: ( x1 in L & x2 in L implies Line (x1,x2) c= L ) L in line_of_REAL n ; then ex y1, y2 being Element of REAL n st L = Line (y1,y2) ; hence ( x1 in L & x2 in L implies Line (x1,x2) c= L ) by EUCLID_4:10; ::_thesis: verum end; theorem Th49: :: EUCLIDLP:49 for n being Element of NAT for L1, L2 being Element of line_of_REAL n holds ( L1 meets L2 iff ex x being Element of REAL n st ( x in L1 & x in L2 ) ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n holds ( L1 meets L2 iff ex x being Element of REAL n st ( x in L1 & x in L2 ) ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 meets L2 iff ex x being Element of REAL n st ( x in L1 & x in L2 ) ) thus ( L1 meets L2 implies ex x being Element of REAL n st ( x in L1 & x in L2 ) ) ::_thesis: ( ex x being Element of REAL n st ( x in L1 & x in L2 ) implies L1 meets L2 ) proof assume L1 meets L2 ; ::_thesis: ex x being Element of REAL n st ( x in L1 & x in L2 ) then consider x being set such that A1: x in L1 and A2: x in L2 by XBOOLE_0:3; reconsider x = x as Element of REAL n by A1; take x ; ::_thesis: ( x in L1 & x in L2 ) thus ( x in L1 & x in L2 ) by A1, A2; ::_thesis: verum end; thus ( ex x being Element of REAL n st ( x in L1 & x in L2 ) implies L1 meets L2 ) by XBOOLE_0:3; ::_thesis: verum end; theorem :: EUCLIDLP:50 for n being Element of NAT for x being Element of REAL n for L0, L1 being Element of line_of_REAL n st L0 misses L1 & x in L0 holds not x in L1 by Th49; theorem Th51: :: EUCLIDLP:51 for n being Element of NAT for L being Element of line_of_REAL n ex x1, x2 being Element of REAL n st L = Line (x1,x2) proof let n be Element of NAT ; ::_thesis: for L being Element of line_of_REAL n ex x1, x2 being Element of REAL n st L = Line (x1,x2) let L be Element of line_of_REAL n; ::_thesis: ex x1, x2 being Element of REAL n st L = Line (x1,x2) L in line_of_REAL n ; then consider x1, x2 being Element of REAL n such that A1: L = Line (x1,x2) ; take x1 ; ::_thesis: ex x2 being Element of REAL n st L = Line (x1,x2) take x2 ; ::_thesis: L = Line (x1,x2) thus L = Line (x1,x2) by A1; ::_thesis: verum end; theorem Th52: :: EUCLIDLP:52 for n being Element of NAT for L being Element of line_of_REAL n ex x being Element of REAL n st x in L proof let n be Element of NAT ; ::_thesis: for L being Element of line_of_REAL n ex x being Element of REAL n st x in L let L be Element of line_of_REAL n; ::_thesis: ex x being Element of REAL n st x in L consider x1, x2 being Element of REAL n such that A1: L = Line (x1,x2) by Th51; take x1 ; ::_thesis: x1 in L thus x1 in L by A1, EUCLID_4:9; ::_thesis: verum end; theorem Th53: :: EUCLIDLP:53 for n being Element of NAT for x0 being Element of REAL n for L being Element of line_of_REAL n st L is being_line holds ex x1 being Element of REAL n st ( x1 <> x0 & x1 in L ) proof let n be Element of NAT ; ::_thesis: for x0 being Element of REAL n for L being Element of line_of_REAL n st L is being_line holds ex x1 being Element of REAL n st ( x1 <> x0 & x1 in L ) let x0 be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st L is being_line holds ex x1 being Element of REAL n st ( x1 <> x0 & x1 in L ) let L be Element of line_of_REAL n; ::_thesis: ( L is being_line implies ex x1 being Element of REAL n st ( x1 <> x0 & x1 in L ) ) assume L is being_line ; ::_thesis: ex x1 being Element of REAL n st ( x1 <> x0 & x1 in L ) then consider y1, y2 being Element of REAL n such that A1: y1 in L and A2: ( y2 in L & y1 <> y2 ) by EUCLID_4:13; now__::_thesis:_(_(_y1_=_x0_&_ex_y2_being_Element_of_REAL_n_st_ (_y2_<>_x0_&_y2_in_L_)_)_or_(_y1_<>_x0_&_ex_y1_being_Element_of_REAL_n_st_ (_y1_<>_x0_&_y1_in_L_)_)_) percases ( y1 = x0 or y1 <> x0 ) ; caseA3: y1 = x0 ; ::_thesis: ex y2 being Element of REAL n st ( y2 <> x0 & y2 in L ) take y2 = y2; ::_thesis: ( y2 <> x0 & y2 in L ) thus ( y2 <> x0 & y2 in L ) by A2, A3; ::_thesis: verum end; caseA4: y1 <> x0 ; ::_thesis: ex y1 being Element of REAL n st ( y1 <> x0 & y1 in L ) take y1 = y1; ::_thesis: ( y1 <> x0 & y1 in L ) thus ( y1 <> x0 & y1 in L ) by A1, A4; ::_thesis: verum end; end; end; hence ex x1 being Element of REAL n st ( x1 <> x0 & x1 in L ) ; ::_thesis: verum end; theorem Th54: :: EUCLIDLP:54 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st not x in L & L is being_line holds ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) let L be Element of line_of_REAL n; ::_thesis: ( not x in L & L is being_line implies ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) ) assume that A1: not x in L and A2: L is being_line ; ::_thesis: ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) consider y0, y1 being Element of REAL n such that A3: y0 <> y1 and A4: L = Line (y0,y1) by A2, EUCLID_4:def_2; A5: y0 - y1 <> 0* n by A3, Th9; consider x1 being Element of REAL n such that A6: x1 in Line (y0,y1) and A7: y0 - y1,x - x1 are_orthogonal by Th43; x - x1 <> 0* n by A1, A4, A6, Th9; then A8: y0 - y1 _|_ x - x1 by A7, A5, Def3; take x1 ; ::_thesis: ex x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) consider x2 being Element of REAL n such that A9: x1 <> x2 and A10: x2 in L by A2, EUCLID_4:14; take x2 ; ::_thesis: ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) A11: x2 - x1 <> 0* n by A9, Th9; ex a being Real st x2 - x1 = a * (y0 - y1) by A4, A6, A10, Th31; then x2 - x1 // y0 - y1 by A5, A11, Def1; hence ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) by A2, A4, A6, A8, A9, A10, Th30, Th44; ::_thesis: verum end; theorem Th55: :: EUCLIDLP:55 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st not x in L & L is being_line holds ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) let L be Element of line_of_REAL n; ::_thesis: ( not x in L & L is being_line implies ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) ) assume ( not x in L & L is being_line ) ; ::_thesis: ex x1, x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) then consider x1, x2 being Element of REAL n such that A1: ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) by Th54; take x1 ; ::_thesis: ex x2 being Element of REAL n st ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) take x2 ; ::_thesis: ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) thus ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) by A1, Th45; ::_thesis: verum end; definition let n be Element of NAT ; let x be Element of REAL n; let L be Element of line_of_REAL n; func dist_v (x,L) -> Subset of REAL equals :: EUCLIDLP:def 5 { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ; correctness coherence { |.(x - x0).| where x0 is Element of REAL n : x0 in L } is Subset of REAL; proof set A = { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ; { |.(x - x0).| where x0 is Element of REAL n : x0 in L } c= REAL proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { |.(x - x0).| where x0 is Element of REAL n : x0 in L } or r in REAL ) assume r in { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ; ::_thesis: r in REAL then ex x0 being Element of REAL n st ( r = |.(x - x0).| & x0 in L ) ; hence r in REAL ; ::_thesis: verum end; hence { |.(x - x0).| where x0 is Element of REAL n : x0 in L } is Subset of REAL ; ::_thesis: verum end; end; :: deftheorem defines dist_v EUCLIDLP:def_5_:_ for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n holds dist_v (x,L) = { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ; definition let n be Element of NAT ; let x be Element of REAL n; let L be Element of line_of_REAL n; func dist (x,L) -> Real equals :: EUCLIDLP:def 6 lower_bound (dist_v (x,L)); correctness coherence lower_bound (dist_v (x,L)) is Real; ; end; :: deftheorem defines dist EUCLIDLP:def_6_:_ for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n holds dist (x,L) = lower_bound (dist_v (x,L)); theorem :: EUCLIDLP:56 for n being Element of NAT for x1, x2, x being Element of REAL n for L being Element of line_of_REAL n st L = Line (x1,x2) holds { |.(x - x0).| where x0 is Element of REAL n : x0 in Line (x1,x2) } = dist_v (x,L) ; theorem Th57: :: EUCLIDLP:57 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n ex x0 being Element of REAL n st ( x0 in L & |.(x - x0).| = dist (x,L) ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n ex x0 being Element of REAL n st ( x0 in L & |.(x - x0).| = dist (x,L) ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n ex x0 being Element of REAL n st ( x0 in L & |.(x - x0).| = dist (x,L) ) let L be Element of line_of_REAL n; ::_thesis: ex x0 being Element of REAL n st ( x0 in L & |.(x - x0).| = dist (x,L) ) consider x1, x2 being Element of REAL n such that A1: L = Line (x1,x2) by Th51; { |.(x - x9).| where x9 is Element of REAL n : x9 in Line (x1,x2) } = dist_v (x,L) by A1; then reconsider R = { |.(x - x9).| where x9 is Element of REAL n : x9 in Line (x1,x2) } as Subset of REAL ; consider x0 being Element of REAL n such that A2: ( x0 in Line (x1,x2) & |.(x - x0).| = lower_bound R ) and x1 - x2,x - x0 are_orthogonal by EUCLID_4:40; take x0 ; ::_thesis: ( x0 in L & |.(x - x0).| = dist (x,L) ) thus ( x0 in L & |.(x - x0).| = dist (x,L) ) by A1, A2; ::_thesis: verum end; theorem :: EUCLIDLP:58 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n holds dist (x,L) >= 0 proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n holds dist (x,L) >= 0 let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n holds dist (x,L) >= 0 let L be Element of line_of_REAL n; ::_thesis: dist (x,L) >= 0 ex x0 being Element of REAL n st ( x0 in L & |.(x - x0).| = dist (x,L) ) by Th57; hence dist (x,L) >= 0 ; ::_thesis: verum end; theorem :: EUCLIDLP:59 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n holds ( x in L iff dist (x,L) = 0 ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n holds ( x in L iff dist (x,L) = 0 ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n holds ( x in L iff dist (x,L) = 0 ) let L be Element of line_of_REAL n; ::_thesis: ( x in L iff dist (x,L) = 0 ) thus ( x in L implies dist (x,L) = 0 ) ::_thesis: ( dist (x,L) = 0 implies x in L ) proof A1: for r being real number st r in dist_v (x,L) holds 0 <= r proof let r be real number ; ::_thesis: ( r in dist_v (x,L) implies 0 <= r ) assume r in dist_v (x,L) ; ::_thesis: 0 <= r then ex x0 being Element of REAL n st ( r = |.(x - x0).| & x0 in L ) ; hence 0 <= r ; ::_thesis: verum end; A2: dist_v (x,L) is bounded_below proof take 0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of dist_v (x,L) let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in dist_v (x,L) or 0 <= r ) assume r in dist_v (x,L) ; ::_thesis: 0 <= r then ex x0 being Element of REAL n st ( r = |.(x - x0).| & x0 in L ) ; hence 0 <= r ; ::_thesis: verum end; assume A3: x in L ; ::_thesis: dist (x,L) = 0 |.(x - x).| = |.(0* n).| by Th9 .= sqrt |((0* n),(0* n))| by EUCLID_4:15 .= 0 by EUCLID_4:17, SQUARE_1:17 ; then A4: 0 in dist_v (x,L) by A3; then for s being real number st 0 < s holds ex r being real number st ( r in dist_v (x,L) & r < 0 + s ) ; hence dist (x,L) = 0 by A4, A1, A2, SEQ_4:def_2; ::_thesis: verum end; now__::_thesis:_(_dist_(x,L)_=_0_implies_x_in_L_) consider x0 being Element of REAL n such that A5: x0 in L and A6: |.(x - x0).| = dist (x,L) by Th57; assume dist (x,L) = 0 ; ::_thesis: x in L then |((x - x0),(x - x0))| = 0 by A6, EUCLID_4:16; then x - x0 = 0* n by EUCLID_4:17; hence x in L by A5, Th9; ::_thesis: verum end; hence ( dist (x,L) = 0 implies x in L ) ; ::_thesis: verum end; definition let n be Element of NAT ; let L1, L2 be Element of line_of_REAL n; predL1 // L2 means :Def7: :: EUCLIDLP:def 7 ex x1, x2, y1, y2 being Element of REAL n st ( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 // y2 - y1 ); symmetry for L1, L2 being Element of line_of_REAL n st ex x1, x2, y1, y2 being Element of REAL n st ( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 // y2 - y1 ) holds ex x1, x2, y1, y2 being Element of REAL n st ( L2 = Line (x1,x2) & L1 = Line (y1,y2) & x2 - x1 // y2 - y1 ) ; end; :: deftheorem Def7 defines // EUCLIDLP:def_7_:_ for n being Element of NAT for L1, L2 being Element of line_of_REAL n holds ( L1 // L2 iff ex x1, x2, y1, y2 being Element of REAL n st ( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 // y2 - y1 ) ); theorem :: EUCLIDLP:60 for n being Element of NAT for L0, L1, L2 being Element of line_of_REAL n st L0 // L1 & L1 // L2 holds L0 // L2 proof let n be Element of NAT ; ::_thesis: for L0, L1, L2 being Element of line_of_REAL n st L0 // L1 & L1 // L2 holds L0 // L2 let L0, L1, L2 be Element of line_of_REAL n; ::_thesis: ( L0 // L1 & L1 // L2 implies L0 // L2 ) assume that A1: L0 // L1 and A2: L1 // L2 ; ::_thesis: L0 // L2 consider x0, x1, x2, x3 being Element of REAL n such that A3: L0 = Line (x0,x1) and A4: L1 = Line (x2,x3) and A5: x1 - x0 // x3 - x2 by A1, Def7; A6: x3 - x2 <> 0* n by A5, Def1; consider y0, y1, y2, y3 being Element of REAL n such that A7: L1 = Line (y0,y1) and A8: L2 = Line (y2,y3) and A9: y1 - y0 // y3 - y2 by A2, Def7; A10: y1 - y0 <> 0* n by A9, Def1; ( x3 in Line (y1,y0) & x2 in Line (y1,y0) ) by A4, A7, EUCLID_4:9; then ex a being Real st x3 - x2 = a * (y1 - y0) by Th31; then x3 - x2 // y1 - y0 by A6, A10, Def1; then x1 - x0 // y1 - y0 by A5, Th33; then x1 - x0 // y3 - y2 by A9, Th33; hence L0 // L2 by A3, A8, Def7; ::_thesis: verum end; definition let n be Element of NAT ; let L1, L2 be Element of line_of_REAL n; predL1 _|_ L2 means :Def8: :: EUCLIDLP:def 8 ex x1, x2, y1, y2 being Element of REAL n st ( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ); symmetry for L1, L2 being Element of line_of_REAL n st ex x1, x2, y1, y2 being Element of REAL n st ( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ) holds ex x1, x2, y1, y2 being Element of REAL n st ( L2 = Line (x1,x2) & L1 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ) ; end; :: deftheorem Def8 defines _|_ EUCLIDLP:def_8_:_ for n being Element of NAT for L1, L2 being Element of line_of_REAL n holds ( L1 _|_ L2 iff ex x1, x2, y1, y2 being Element of REAL n st ( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ) ); theorem Th61: :: EUCLIDLP:61 for n being Element of NAT for L0, L1, L2 being Element of line_of_REAL n st L0 _|_ L1 & L1 // L2 holds L0 _|_ L2 proof let n be Element of NAT ; ::_thesis: for L0, L1, L2 being Element of line_of_REAL n st L0 _|_ L1 & L1 // L2 holds L0 _|_ L2 let L0, L1, L2 be Element of line_of_REAL n; ::_thesis: ( L0 _|_ L1 & L1 // L2 implies L0 _|_ L2 ) assume that A1: L0 _|_ L1 and A2: L1 // L2 ; ::_thesis: L0 _|_ L2 consider x0, x1, x2, x3 being Element of REAL n such that A3: L0 = Line (x0,x1) and A4: L1 = Line (x2,x3) and A5: x1 - x0 _|_ x3 - x2 by A1, Def8; A6: x3 - x2 <> 0* n by A5, Def3; consider y0, y1, y2, y3 being Element of REAL n such that A7: L1 = Line (y0,y1) and A8: L2 = Line (y2,y3) and A9: y1 - y0 // y3 - y2 by A2, Def7; A10: y1 - y0 <> 0* n by A9, Def1; ( x2 in Line (y0,y1) & x3 in Line (y0,y1) ) by A4, A7, EUCLID_4:9; then ex a being Real st x3 - x2 = a * (y1 - y0) by Th31; then x3 - x2 // y1 - y0 by A6, A10, Def1; then x1 - x0 _|_ y3 - y2 by A5, A9, Th33, Th44; hence L0 _|_ L2 by A3, A8, Def8; ::_thesis: verum end; theorem Th62: :: EUCLIDLP:62 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L & L0 meets L ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L & L0 meets L ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st not x in L & L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L & L0 meets L ) let L be Element of line_of_REAL n; ::_thesis: ( not x in L & L is being_line implies ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L & L0 meets L ) ) assume ( not x in L & L is being_line ) ; ::_thesis: ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L & L0 meets L ) then consider x1, x2 being Element of REAL n such that A1: L = Line (x1,x2) and A2: x - x1 _|_ x2 - x1 by Th54; reconsider L0 = Line (x1,x) as Subset of (REAL n) ; reconsider L0 = L0 as Element of line_of_REAL n by Th47; ( x1 in L0 & x1 in L ) by A1, EUCLID_4:9; then A3: ( x in L0 & L0 meets L ) by Th49, EUCLID_4:9; L0 _|_ L by A1, A2, Def8; hence ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L & L0 meets L ) by A3; ::_thesis: verum end; theorem Th63: :: EUCLIDLP:63 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 misses L2 holds ex x being Element of REAL n st ( x in L1 & not x in L2 ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 misses L2 holds ex x being Element of REAL n st ( x in L1 & not x in L2 ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 misses L2 implies ex x being Element of REAL n st ( x in L1 & not x in L2 ) ) assume A1: L1 misses L2 ; ::_thesis: ex x being Element of REAL n st ( x in L1 & not x in L2 ) consider x being Element of REAL n such that A2: x in L1 by Th52; take x ; ::_thesis: ( x in L1 & not x in L2 ) thus ( x in L1 & not x in L2 ) by A1, A2, Th49; ::_thesis: verum end; theorem Th64: :: EUCLIDLP:64 for n being Element of NAT for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L & x1 <> x2 holds ( Line (x1,x2) = L & L is being_line ) proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L & x1 <> x2 holds ( Line (x1,x2) = L & L is being_line ) let x1, x2 be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L & x1 <> x2 holds ( Line (x1,x2) = L & L is being_line ) let L be Element of line_of_REAL n; ::_thesis: ( x1 in L & x2 in L & x1 <> x2 implies ( Line (x1,x2) = L & L is being_line ) ) assume that A1: ( x1 in L & x2 in L ) and A2: x1 <> x2 ; ::_thesis: ( Line (x1,x2) = L & L is being_line ) A3: Line (x1,x2) c= L by A1, Th48; L in line_of_REAL n ; then ex y1, y2 being Element of REAL n st L = Line (y1,y2) ; then L c= Line (x1,x2) by A1, A2, EUCLID_4:11; then Line (x1,x2) = L by A3, XBOOLE_0:def_10; hence ( Line (x1,x2) = L & L is being_line ) by A2, EUCLID_4:def_2; ::_thesis: verum end; theorem Th65: :: EUCLIDLP:65 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 is being_line & L1 = L2 holds L1 // L2 proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 is being_line & L1 = L2 holds L1 // L2 let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 is being_line & L1 = L2 implies L1 // L2 ) assume L1 is being_line ; ::_thesis: ( not L1 = L2 or L1 // L2 ) then consider x0, x1 being Element of REAL n such that A1: x0 <> x1 and A2: L1 = Line (x0,x1) by EUCLID_4:def_2; assume A3: L1 = L2 ; ::_thesis: L1 // L2 A4: x1 - x0 = 1 * (x1 - x0) by EUCLID_4:3; x1 - x0 <> 0* n by A1, Th9; then x1 - x0 // x1 - x0 by A4, Def1; hence L1 // L2 by A3, A2, Def7; ::_thesis: verum end; theorem Th66: :: EUCLIDLP:66 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 // L2 holds ( L1 is being_line & L2 is being_line ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 // L2 holds ( L1 is being_line & L2 is being_line ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 // L2 implies ( L1 is being_line & L2 is being_line ) ) assume L1 // L2 ; ::_thesis: ( L1 is being_line & L2 is being_line ) then consider x1, x2, y1, y2 being Element of REAL n such that A1: ( L1 = Line (x1,x2) & L2 = Line (y1,y2) ) and A2: x2 - x1 // y2 - y1 by Def7; y2 - y1 <> 0* n by A2, Def1; then A3: y2 <> y1 by Th9; x2 - x1 <> 0* n by A2, Def1; then x2 <> x1 by Th9; hence ( L1 is being_line & L2 is being_line ) by A1, A3, EUCLID_4:def_2; ::_thesis: verum end; theorem Th67: :: EUCLIDLP:67 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds ( L1 is being_line & L2 is being_line ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds ( L1 is being_line & L2 is being_line ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 _|_ L2 implies ( L1 is being_line & L2 is being_line ) ) assume L1 _|_ L2 ; ::_thesis: ( L1 is being_line & L2 is being_line ) then consider x1, x2, y1, y2 being Element of REAL n such that A1: ( L1 = Line (x1,x2) & L2 = Line (y1,y2) ) and A2: x2 - x1 _|_ y2 - y1 by Def8; y2 - y1 <> 0* n by A2, Def3; then A3: y2 <> y1 by Th9; x2 - x1 <> 0* n by A2, Def3; then x2 <> x1 by Th9; hence ( L1 is being_line & L2 is being_line ) by A1, A3, EUCLID_4:def_2; ::_thesis: verum end; theorem :: EUCLIDLP:68 for a being Real for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds 0* n in L proof let a be Real; ::_thesis: for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds 0* n in L let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds 0* n in L let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds 0* n in L let L be Element of line_of_REAL n; ::_thesis: ( x in L & a <> 1 & a * x in L implies 0* n in L ) assume that A1: x in L and A2: a <> 1 and A3: a * x in L ; ::_thesis: 0* n in L A4: 1 - a <> 0 by A2; A5: (1 - (1 / (1 - a))) + ((1 / (1 - a)) * a) = (1 - (1 / (1 - a))) + (a / (1 - a)) by XCMPLX_1:99 .= 1 + ((- (1 / (1 - a))) + (a / (1 - a))) .= 1 + (((- 1) / (1 - a)) + (a / (1 - a))) by XCMPLX_1:187 .= 1 + (((- 1) + a) / (1 - a)) by XCMPLX_1:62 .= 1 + ((- ((- a) + 1)) / (1 - a)) .= 1 + (- ((1 - a) / (1 - a))) by XCMPLX_1:187 .= 1 - ((1 - a) / (1 - a)) .= 1 - 1 by A4, XCMPLX_1:60 .= 0 ; 0* n = 0 * x by EUCLID_4:3 .= ((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x) by A5, EUCLID_4:7 .= ((1 - (1 / (1 - a))) * x) + ((1 / (1 - a)) * (a * x)) by EUCLID_4:4 ; then A6: 0* n in Line (x,(a * x)) ; Line (x,(a * x)) c= L by A1, A3, Th48; hence 0* n in L by A6; ::_thesis: verum end; theorem :: EUCLIDLP:69 for a being Real for n being Element of NAT for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L holds ex x3 being Element of REAL n st ( x3 in L & x3 - x1 = a * (x2 - x1) ) proof let a be Real; ::_thesis: for n being Element of NAT for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L holds ex x3 being Element of REAL n st ( x3 in L & x3 - x1 = a * (x2 - x1) ) let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L holds ex x3 being Element of REAL n st ( x3 in L & x3 - x1 = a * (x2 - x1) ) let x1, x2 be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L holds ex x3 being Element of REAL n st ( x3 in L & x3 - x1 = a * (x2 - x1) ) let L be Element of line_of_REAL n; ::_thesis: ( x1 in L & x2 in L implies ex x3 being Element of REAL n st ( x3 in L & x3 - x1 = a * (x2 - x1) ) ) set x3 = ((1 - a) * x1) + (a * x2); assume ( x1 in L & x2 in L ) ; ::_thesis: ex x3 being Element of REAL n st ( x3 in L & x3 - x1 = a * (x2 - x1) ) then A1: Line (x1,x2) c= L by Th48; ((1 - a) * x1) + (a * x2) = ((1 * x1) + (- (a * x1))) + (a * x2) by Th11 .= (x1 + (- (a * x1))) + (a * x2) by EUCLID_4:3 .= x1 + ((a * x2) + (- (a * x1))) by RVSUM_1:15 .= x1 + (a * (x2 - x1)) by Th12 ; then ( ((1 - a) * x1) + (a * x2) in Line (x1,x2) & (((1 - a) * x1) + (a * x2)) - x1 = a * (x2 - x1) ) by Th6; hence ex x3 being Element of REAL n st ( x3 in L & x3 - x1 = a * (x2 - x1) ) by A1; ::_thesis: verum end; theorem Th70: :: EUCLIDLP:70 for n being Element of NAT for x1, x2, x3 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L & x3 in L & x1 <> x2 holds ex a being Real st x3 - x1 = a * (x2 - x1) proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n for L being Element of line_of_REAL n st x1 in L & x2 in L & x3 in L & x1 <> x2 holds ex a being Real st x3 - x1 = a * (x2 - x1) let x1, x2, x3 be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L & x3 in L & x1 <> x2 holds ex a being Real st x3 - x1 = a * (x2 - x1) let L be Element of line_of_REAL n; ::_thesis: ( x1 in L & x2 in L & x3 in L & x1 <> x2 implies ex a being Real st x3 - x1 = a * (x2 - x1) ) assume ( x1 in L & x2 in L & x3 in L & x1 <> x2 ) ; ::_thesis: ex a being Real st x3 - x1 = a * (x2 - x1) then ( x1 in Line (x1,x2) & x3 in Line (x1,x2) ) by Th64; then consider a being Real such that A1: x3 - x1 = a * (x2 - x1) by Th31; take a ; ::_thesis: x3 - x1 = a * (x2 - x1) thus x3 - x1 = a * (x2 - x1) by A1; ::_thesis: verum end; theorem Th71: :: EUCLIDLP:71 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds L1 misses L2 proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds L1 misses L2 let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 // L2 & L1 <> L2 implies L1 misses L2 ) assume that A1: L1 // L2 and A2: L1 <> L2 ; ::_thesis: L1 misses L2 assume not L1 misses L2 ; ::_thesis: contradiction then consider x being set such that A3: x in L1 and A4: x in L2 by XBOOLE_0:3; reconsider x = x as Element of REAL n by A3; consider x1, x2, y1, y2 being Element of REAL n such that A5: L1 = Line (x1,x2) and A6: L2 = Line (y1,y2) and A7: x2 - x1 // y2 - y1 by A1, Def7; A8: x2 - x1 <> 0* n by A7, Def1; then x1 <> x2 by Th9; then A9: L1 is being_line by A5, EUCLID_4:def_2; then consider x0 being Element of REAL n such that A10: x <> x0 and A11: x0 in L1 by EUCLID_4:14; A12: x0 - x <> 0* n by A10, Th9; ex a being Real st x0 - x = a * (x2 - x1) by A5, A3, A11, Th31; then x0 - x // x2 - x1 by A8, A12, Def1; then A13: x0 - x // y2 - y1 by A7, Th33; A14: y2 - y1 <> 0* n by A7, Def1; then y1 <> y2 by Th9; then A15: L2 is being_line by A6, EUCLID_4:def_2; then consider y0 being Element of REAL n such that A16: x <> y0 and A17: y0 in L2 by EUCLID_4:14; A18: y0 - x <> 0* n by A16, Th9; ex b being Real st y0 - x = b * (y2 - y1) by A6, A4, A17, Th31; then y0 - x // y2 - y1 by A14, A18, Def1; then A19: x0 - x // y0 - x by A13, Th33; A20: Line (x,x0) c= Line (x,y0) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Line (x,x0) or y in Line (x,y0) ) assume y in Line (x,x0) ; ::_thesis: y in Line (x,y0) then consider t being Real such that A21: y = ((1 - t) * x) + (t * x0) ; consider a being Real such that A22: x0 - x = a * (y0 - x) by A19, Def1; y = ((1 * x) + (- (t * x))) + (t * x0) by A21, Th11 .= (x + (- (t * x))) + (t * x0) by EUCLID_4:3 .= x + ((t * x0) + (- (t * x))) by RVSUM_1:15 .= x + (t * (x0 - x)) by Th12 ; then y = x + ((t * a) * (y0 - x)) by A22, EUCLID_4:4 .= x + (((t * a) * y0) + (- ((t * a) * x))) by Th12 .= (x + (- ((t * a) * x))) + ((t * a) * y0) by RVSUM_1:15 .= ((1 * x) + (- ((t * a) * x))) + ((t * a) * y0) by EUCLID_4:3 .= ((1 - (t * a)) * x) + ((t * a) * y0) by Th11 ; hence y in Line (x,y0) ; ::_thesis: verum end; A23: Line (x,y0) c= Line (x,x0) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Line (x,y0) or y in Line (x,x0) ) assume y in Line (x,y0) ; ::_thesis: y in Line (x,x0) then consider t being Real such that A24: y = ((1 - t) * x) + (t * y0) ; consider a being Real such that A25: y0 - x = a * (x0 - x) by A19, Def1; y = ((1 * x) + (- (t * x))) + (t * y0) by A24, Th11 .= (x + (- (t * x))) + (t * y0) by EUCLID_4:3 .= x + ((t * y0) + (- (t * x))) by RVSUM_1:15 .= x + (t * (y0 - x)) by Th12 ; then y = x + ((t * a) * (x0 - x)) by A25, EUCLID_4:4 .= x + (((t * a) * x0) + (- ((t * a) * x))) by Th12 .= (x + (- ((t * a) * x))) + ((t * a) * x0) by RVSUM_1:15 .= ((1 * x) + (- ((t * a) * x))) + ((t * a) * x0) by EUCLID_4:3 .= ((1 - (t * a)) * x) + ((t * a) * x0) by Th11 ; hence y in Line (x,x0) ; ::_thesis: verum end; A26: L2 = Line (x,y0) by A4, A15, A16, A17, Th30; L1 = Line (x,x0) by A3, A9, A10, A11, Th30; hence contradiction by A2, A26, A20, A23, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th72: :: EUCLIDLP:72 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n st L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L ) let L be Element of line_of_REAL n; ::_thesis: ( L is being_line implies ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L ) ) assume L is being_line ; ::_thesis: ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L ) then consider y0, y1 being Element of REAL n such that A1: y0 <> y1 and A2: L = Line (y0,y1) by EUCLID_4:def_2; set x9 = x + (y1 - y0); reconsider L0 = Line (x,(x + (y1 - y0))) as Element of line_of_REAL n by Th47; take L0 ; ::_thesis: ( x in L0 & L0 // L ) A3: y1 - y0 <> 0* n by A1, Th9; A4: (x + (y1 - y0)) - x = y1 - y0 by Th6; then (x + (y1 - y0)) - x = 1 * (y1 - y0) by EUCLID_4:3; then (x + (y1 - y0)) - x // y1 - y0 by A4, A3, Def1; hence ( x in L0 & L0 // L ) by A2, Def7, EUCLID_4:9; ::_thesis: verum end; theorem :: EUCLIDLP:73 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L & L0 <> L ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L & L0 <> L ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st not x in L & L is being_line holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L & L0 <> L ) let L be Element of line_of_REAL n; ::_thesis: ( not x in L & L is being_line implies ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L & L0 <> L ) ) assume that A1: not x in L and A2: L is being_line ; ::_thesis: ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L & L0 <> L ) ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L ) by A2, Th72; hence ex L0 being Element of line_of_REAL n st ( x in L0 & L0 // L & L0 <> L ) by A1; ::_thesis: verum end; theorem Th74: :: EUCLIDLP:74 for n being Element of NAT for x0, x1, y0, y1 being Element of REAL n for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds x1 - x0 _|_ y1 - y0 proof let n be Element of NAT ; ::_thesis: for x0, x1, y0, y1 being Element of REAL n for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds x1 - x0 _|_ y1 - y0 let x0, x1, y0, y1 be Element of REAL n; ::_thesis: for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds x1 - x0 _|_ y1 - y0 let L1, L2 be Element of line_of_REAL n; ::_thesis: ( x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 implies x1 - x0 _|_ y1 - y0 ) assume that A1: ( x0 in L1 & x1 in L1 ) and A2: x0 <> x1 and A3: ( y0 in L2 & y1 in L2 ) and A4: y0 <> y1 and A5: L1 _|_ L2 ; ::_thesis: x1 - x0 _|_ y1 - y0 consider x2, x3, y2, y3 being Element of REAL n such that A6: L1 = Line (x2,x3) and A7: L2 = Line (y2,y3) and A8: x3 - x2 _|_ y3 - y2 by A5, Def8; consider s being Real such that A9: x1 - x0 = s * (x3 - x2) by A1, A6, Th31; x3 - x2,y3 - y2 are_orthogonal by A8, Def3; then A10: |((x3 - x2),(y3 - y2))| = 0 by RVSUM_1:def_17; consider t being Real such that A11: y1 - y0 = t * (y3 - y2) by A3, A7, Th31; |((x1 - x0),(y1 - y0))| = s * |((x3 - x2),(y1 - y0))| by A9, EUCLID_4:21 .= s * (t * |((x3 - x2),(y3 - y2))|) by A11, EUCLID_4:22 .= 0 by A10 ; then A12: x1 - x0,y1 - y0 are_orthogonal by RVSUM_1:def_17; ( x1 - x0 <> 0* n & y1 - y0 <> 0* n ) by A2, A4, Th9; hence x1 - x0 _|_ y1 - y0 by A12, Def3; ::_thesis: verum end; theorem Th75: :: EUCLIDLP:75 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds L1 <> L2 proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds L1 <> L2 let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 _|_ L2 implies L1 <> L2 ) assume A1: L1 _|_ L2 ; ::_thesis: L1 <> L2 now__::_thesis:_(_(_L1_misses_L2_&_L1_<>_L2_)_or_(_L1_meets_L2_&_L1_<>_L2_)_) percases ( L1 misses L2 or L1 meets L2 ) ; caseA2: L1 misses L2 ; ::_thesis: L1 <> L2 ex x being Element of REAL n st x in L1 by Th52; hence L1 <> L2 by A2, Th49; ::_thesis: verum end; case L1 meets L2 ; ::_thesis: L1 <> L2 then consider x0 being Element of REAL n such that A3: x0 in L1 and A4: x0 in L2 by Th49; L1 is being_line by A1, Th67; then consider x1 being Element of REAL n such that A5: x1 <> x0 and A6: x1 in L1 by Th53; A7: x1 - x0 <> 0* n by A5, Th9; L2 is being_line by A1, Th67; then consider x2 being Element of REAL n such that A8: x2 <> x0 and A9: x2 in L2 by Th53; A10: x2 - x0 <> 0* n by A8, Th9; A11: x1 - x0 _|_ x2 - x0 by A1, A3, A4, A5, A6, A8, A9, Th74; not x1 in L2 proof assume x1 in L2 ; ::_thesis: contradiction then ex a being Real st x1 - x0 = a * (x2 - x0) by A4, A8, A9, Th70; then x1 - x0 // x2 - x0 by A7, A10, Def1; hence contradiction by A11, Lm3, Th45; ::_thesis: verum end; hence L1 <> L2 by A6; ::_thesis: verum end; end; end; hence L1 <> L2 ; ::_thesis: verum end; theorem Th76: :: EUCLIDLP:76 for n being Element of NAT for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st L is being_line & L = Line (x1,x2) holds x1 <> x2 proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n for L being Element of line_of_REAL n st L is being_line & L = Line (x1,x2) holds x1 <> x2 let x1, x2 be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st L is being_line & L = Line (x1,x2) holds x1 <> x2 let L be Element of line_of_REAL n; ::_thesis: ( L is being_line & L = Line (x1,x2) implies x1 <> x2 ) assume that A1: L is being_line and A2: L = Line (x1,x2) ; ::_thesis: x1 <> x2 consider y1, y2 being Element of REAL n such that A3: y1 <> y2 and A4: L = Line (y1,y2) by A1, EUCLID_4:def_2; ( y1 in L & y2 in L ) by A4, EUCLID_4:9; then consider a being Real such that A5: y2 - y1 = a * (x2 - x1) by A2, Th31; thus x1 <> x2 ::_thesis: verum proof assume x1 = x2 ; ::_thesis: contradiction then y2 - y1 = a * (0* n) by A5, Th2 .= 0* n by EUCLID_4:2 ; hence contradiction by A3, Th9; ::_thesis: verum end; end; theorem Th77: :: EUCLIDLP:77 for n being Element of NAT for x0, x1, y0, y1 being Element of REAL n for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 holds x1 - x0 // y1 - y0 proof let n be Element of NAT ; ::_thesis: for x0, x1, y0, y1 being Element of REAL n for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 holds x1 - x0 // y1 - y0 let x0, x1, y0, y1 be Element of REAL n; ::_thesis: for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 holds x1 - x0 // y1 - y0 let L1, L2 be Element of line_of_REAL n; ::_thesis: ( x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 implies x1 - x0 // y1 - y0 ) assume that A1: ( x0 in L1 & x1 in L1 ) and A2: x0 <> x1 and A3: ( y0 in L2 & y1 in L2 ) and A4: y0 <> y1 and A5: L1 // L2 ; ::_thesis: x1 - x0 // y1 - y0 consider x2, x3, y2, y3 being Element of REAL n such that A6: L1 = Line (x2,x3) and A7: L2 = Line (y2,y3) and A8: x3 - x2 // y3 - y2 by A5, Def7; consider t being Real such that A9: y1 - y0 = t * (y3 - y2) by A3, A7, Th31; A10: x1 - x0 <> 0* n by A2, Th9; A11: y1 - y0 <> 0* n by A4, Th9; then A12: t <> 0 by A9, EUCLID_4:3; consider s being Real such that A13: x1 - x0 = s * (x3 - x2) by A1, A6, Th31; consider a being Real such that A14: x3 - x2 = a * (y3 - y2) by A8, Def1; x1 - x0 = (s * a) * (y3 - y2) by A13, A14, EUCLID_4:4 .= (s * a) * (1 * (y3 - y2)) by EUCLID_4:3 .= (s * a) * (((1 / t) * t) * (y3 - y2)) by A12, XCMPLX_1:106 .= (s * a) * ((1 / t) * (t * (y3 - y2))) by EUCLID_4:4 .= ((s * a) * (1 / t)) * (t * (y3 - y2)) by EUCLID_4:4 .= ((s * a) / t) * (y1 - y0) by A9, XCMPLX_1:99 ; hence x1 - x0 // y1 - y0 by A10, A11, Def1; ::_thesis: verum end; theorem :: EUCLIDLP:78 for n being Element of NAT for x2, x1, x3, y2, y3 being Element of REAL n for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) holds ( L1 // L2 iff ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) proof let n be Element of NAT ; ::_thesis: for x2, x1, x3, y2, y3 being Element of REAL n for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) holds ( L1 // L2 iff ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) let x2, x1, x3, y2, y3 be Element of REAL n; ::_thesis: for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) holds ( L1 // L2 iff ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) implies ( L1 // L2 iff ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) ) assume that A1: x2 - x1,x3 - x1 are_lindependent2 and A2: y2 in Line (x1,x2) and A3: y3 in Line (x1,x3) and A4: L1 = Line (x2,x3) and A5: L2 = Line (y2,y3) ; ::_thesis: ( L1 // L2 iff ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) thus ( L1 // L2 implies ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) ::_thesis: ( ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 ) proof assume A6: L1 // L2 ; ::_thesis: ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) then L1 is being_line by Th66; then A7: x2 <> x3 by A4, Th76; L2 is being_line by A6, Th66; then A8: y2 <> y3 by A5, Th76; A9: ( y2 in L2 & y3 in L2 ) by A5, EUCLID_4:9; consider t being Real such that A10: y3 = ((1 - t) * x1) + (t * x3) by A3; ( x2 in L1 & x3 in L1 ) by A4, EUCLID_4:9; then A11: y3 - y2 // x3 - x2 by A6, A7, A8, A9, Th77; then consider a being Real such that A12: y3 - y2 = a * (x3 - x2) by Def1; take a ; ::_thesis: ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) consider s being Real such that A13: y2 = ((1 - s) * x1) + (s * x2) by A2; A14: 0* n = (y3 - y2) - (a * (x3 - x2)) by A12, Th9 .= (((((1 - t) * x1) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2)) by A13, A10, RVSUM_1:39 .= (((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2)) by Th11 .= (((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 * x1) + (- (s * x1)))) - (s * x2)) - (a * (x3 - x2)) by Th11 .= ((((((1 * x1) + (- (t * x1))) + (t * x3)) - (1 * x1)) - (- (s * x1))) - (s * x2)) - (a * (x3 - x2)) by RVSUM_1:39 .= ((((((1 * x1) + (- (t * x1))) + (- (1 * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by RVSUM_1:15 .= ((((((1 * x1) + (- (1 * x1))) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by RVSUM_1:15 .= (((((0* n) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by Th2 .= ((((- (t * x1)) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2)) by EUCLID_4:1 .= (((t * (x3 - x1)) + (s * x1)) + (- (s * x2))) - (a * (x3 - x2)) by Th12 .= (((t * (x3 - x1)) - (s * x2)) + (s * x1)) - (a * (x3 - x2)) by RVSUM_1:15 .= ((t * (x3 - x1)) - ((s * x2) - (s * x1))) - (a * (x3 - x2)) by Th4 .= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x2)) by Th12 .= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (0* n)) - x2)) by RVSUM_1:32 .= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (x1 - x1)) - x2)) by Th2 .= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (((x3 - x1) + x1) + (- x2))) by Th4 .= ((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - x1) + ((- x2) + x1))) by RVSUM_1:15 .= ((t * (x3 - x1)) - (s * (x2 - x1))) - ((a * (x3 - x1)) + (a * ((- x2) + x1))) by EUCLID_4:6 .= (((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x1))) - (a * ((- x2) + x1)) by RVSUM_1:39 .= ((t * (x3 - x1)) - ((a * (x3 - x1)) + (s * (x2 - x1)))) - (a * ((- x2) + x1)) by RVSUM_1:39 .= (((t * (x3 - x1)) - (a * (x3 - x1))) - (s * (x2 - x1))) - (a * ((- x2) + x1)) by RVSUM_1:39 .= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (a * ((- x2) + x1)) by Th11 .= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ((a * (- x2)) + (a * x1)) by EUCLID_4:6 .= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ((- (a * x2)) + (a * x1)) by Th3 .= ((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (- (a * x2))) - (a * x1) by RVSUM_1:39 .= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) + ((a * x2) + (- (a * x1))) by RVSUM_1:15 .= (((t - a) * (x3 - x1)) - (s * (x2 - x1))) + (a * (x2 - x1)) by Th12 .= ((t - a) * (x3 - x1)) - ((s * (x2 - x1)) - (a * (x2 - x1))) by Th4 .= ((t - a) * (x3 - x1)) + (- ((s - a) * (x2 - x1))) by Th11 .= ((t - a) * (x3 - x1)) + ((- (s - a)) * (x2 - x1)) by Th3 .= ((t - a) * (x3 - x1)) + ((a - s) * (x2 - x1)) ; then t - a = 0 by A1, Def2; then A15: y3 - x1 = (((1 * x1) + (- (a * x1))) + (a * x3)) - x1 by A10, Th11 .= ((x1 + (- (a * x1))) + (a * x3)) - x1 by EUCLID_4:3 .= (((- (a * x1)) + (a * x3)) + x1) - x1 by RVSUM_1:15 .= ((- (a * x1)) + (a * x3)) + (x1 - x1) by Th5 .= ((- (a * x1)) + (a * x3)) + (0* n) by Th2 .= (- (a * x1)) + (a * x3) by EUCLID_4:1 .= a * (x3 - x1) by Th12 ; a - s = 0 by A1, A14, Def2; then A16: y2 - x1 = (((1 * x1) + (- (a * x1))) + (a * x2)) - x1 by A13, Th11 .= ((x1 + (- (a * x1))) + (a * x2)) - x1 by EUCLID_4:3 .= (((- (a * x1)) + (a * x2)) + x1) - x1 by RVSUM_1:15 .= ((- (a * x1)) + (a * x2)) + (x1 - x1) by Th5 .= ((- (a * x1)) + (a * x2)) + (0* n) by Th2 .= (- (a * x1)) + (a * x2) by EUCLID_4:1 .= a * (x2 - x1) by Th12 ; y3 - y2 <> 0* n by A11, Def1; hence ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) by A12, A16, A15, EUCLID_4:3; ::_thesis: verum end; now__::_thesis:_(_ex_a_being_Real_st_ (_a_<>_0_&_y2_-_x1_=_a_*_(x2_-_x1)_&_y3_-_x1_=_a_*_(x3_-_x1)_)_implies_ex_a_being_Real_ex_x2,_x3,_y2,_y3_being_Element_of_REAL_n_st_L1_//_L2_) assume ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ; ::_thesis: ex a being Real ex x2, x3, y2, y3 being Element of REAL n st L1 // L2 then consider a being Real such that A17: a <> 0 and A18: y2 - x1 = a * (x2 - x1) and A19: y3 - x1 = a * (x3 - x1) ; take a = a; ::_thesis: ex x2, x3, y2, y3 being Element of REAL n st L1 // L2 take x2 = x2; ::_thesis: ex x3, y2, y3 being Element of REAL n st L1 // L2 take x3 = x3; ::_thesis: ex y2, y3 being Element of REAL n st L1 // L2 take y2 = y2; ::_thesis: ex y3 being Element of REAL n st L1 // L2 take y3 = y3; ::_thesis: L1 // L2 x2 <> x3 by A1, Th37; then A20: x3 - x2 <> 0* n by Th9; A21: y3 - y2 = (x1 + (a * (x3 - x1))) - y2 by A19, Th6 .= ((a * (x3 - x1)) + x1) - (x1 + (a * (x2 - x1))) by A18, Th6 .= (((a * (x3 - x1)) + x1) - x1) - (a * (x2 - x1)) by RVSUM_1:39 .= ((a * (x3 - x1)) + (x1 - x1)) - (a * (x2 - x1)) by Th5 .= ((a * (x3 - x1)) + (0* n)) - (a * (x2 - x1)) by Th2 .= (a * (x3 - x1)) - (a * (x2 - x1)) by EUCLID_4:1 .= ((a * x3) + (- (a * x1))) - (a * (x2 - x1)) by Th12 .= ((a * x3) + (- (a * x1))) - ((- (a * x1)) + (a * x2)) by Th12 .= (((a * x3) + (- (a * x1))) - (- (a * x1))) - (a * x2) by RVSUM_1:39 .= ((a * x3) + ((- (a * x1)) - (- (a * x1)))) - (a * x2) by Th5 .= ((a * x3) + (0* n)) - (a * x2) by Th2 .= (a * x3) - (a * x2) by EUCLID_4:1 .= a * (x3 - x2) by Th12 ; then y3 - y2 <> 0* n by A17, A20, EUCLID_4:5; then y3 - y2 // x3 - x2 by A21, A20, Def1; hence L1 // L2 by A4, A5, Def7; ::_thesis: verum end; hence ( ex a being Real st ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 ) ; ::_thesis: verum end; theorem Th79: :: EUCLIDLP:79 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 holds ex x being Element of REAL n st ( x in L1 & not x in L2 ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 holds ex x being Element of REAL n st ( x in L1 & not x in L2 ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 is being_line & L2 is being_line & L1 <> L2 implies ex x being Element of REAL n st ( x in L1 & not x in L2 ) ) assume that A1: L1 is being_line and A2: L2 is being_line ; ::_thesis: ( not L1 <> L2 or ex x being Element of REAL n st ( x in L1 & not x in L2 ) ) consider x1, x2 being Element of REAL n such that A3: x1 <> x2 and A4: L1 = Line (x1,x2) by A1, EUCLID_4:def_2; assume A5: L1 <> L2 ; ::_thesis: ex x being Element of REAL n st ( x in L1 & not x in L2 ) now__::_thesis:_(_(_not_x1_in_L2_&_x1_in_L1_&_not_x1_in_L2_)_or_(_not_x2_in_L2_&_x2_in_L1_&_not_x2_in_L2_)_) percases ( not x1 in L2 or not x2 in L2 ) by A2, A3, A4, A5, Th30; caseA6: not x1 in L2 ; ::_thesis: ( x1 in L1 & not x1 in L2 ) set x = x1; thus ( x1 in L1 & not x1 in L2 ) by A4, A6, EUCLID_4:9; ::_thesis: verum end; caseA7: not x2 in L2 ; ::_thesis: ( x2 in L1 & not x2 in L2 ) set x = x2; thus ( x2 in L1 & not x2 in L2 ) by A4, A7, EUCLID_4:9; ::_thesis: verum end; end; end; hence ex x being Element of REAL n st ( x in L1 & not x in L2 ) ; ::_thesis: verum end; theorem Th80: :: EUCLIDLP:80 for n being Element of NAT for x being Element of REAL n for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L2 & L0 // L1 ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L2 & L0 // L1 ) let x be Element of REAL n; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L2 & L0 // L1 ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 _|_ L2 implies ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L2 & L0 // L1 ) ) assume A1: L1 _|_ L2 ; ::_thesis: ex L0 being Element of line_of_REAL n st ( x in L0 & L0 _|_ L2 & L0 // L1 ) then L1 is being_line by Th67; then consider L0 being Element of line_of_REAL n such that A2: ( x in L0 & L0 // L1 ) by Th72; take L0 ; ::_thesis: ( x in L0 & L0 _|_ L2 & L0 // L1 ) thus ( x in L0 & L0 _|_ L2 & L0 // L1 ) by A1, A2, Th61; ::_thesis: verum end; theorem Th81: :: EUCLIDLP:81 for n being Element of NAT for x being Element of REAL n for L1, L2 being Element of line_of_REAL n st x in L2 & L1 _|_ L2 holds ex x0 being Element of REAL n st ( x <> x0 & x0 in L1 & not x0 in L2 ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L1, L2 being Element of line_of_REAL n st x in L2 & L1 _|_ L2 holds ex x0 being Element of REAL n st ( x <> x0 & x0 in L1 & not x0 in L2 ) let x be Element of REAL n; ::_thesis: for L1, L2 being Element of line_of_REAL n st x in L2 & L1 _|_ L2 holds ex x0 being Element of REAL n st ( x <> x0 & x0 in L1 & not x0 in L2 ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( x in L2 & L1 _|_ L2 implies ex x0 being Element of REAL n st ( x <> x0 & x0 in L1 & not x0 in L2 ) ) assume that A1: x in L2 and A2: L1 _|_ L2 ; ::_thesis: ex x0 being Element of REAL n st ( x <> x0 & x0 in L1 & not x0 in L2 ) ( L1 is being_line & L2 is being_line ) by A2, Th67; then ex x0 being Element of REAL n st ( x0 in L1 & not x0 in L2 ) by A2, Th75, Th79; hence ex x0 being Element of REAL n st ( x <> x0 & x0 in L1 & not x0 in L2 ) by A1; ::_thesis: verum end; definition let n be Element of NAT ; let x1, x2, x3 be Element of REAL n; func plane (x1,x2,x3) -> Subset of (REAL n) equals :: EUCLIDLP:def 9 { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ; correctness coherence { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } is Subset of (REAL n); proof set A = { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ; { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } c= REAL n proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } or x in REAL n ) assume x in { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ; ::_thesis: x in REAL n then ex x9 being Element of REAL n st ( x = x9 & ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x9 = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) ; hence x in REAL n ; ::_thesis: verum end; hence { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } is Subset of (REAL n) ; ::_thesis: verum end; end; :: deftheorem defines plane EUCLIDLP:def_9_:_ for n being Element of NAT for x1, x2, x3 being Element of REAL n holds plane (x1,x2,x3) = { x where x is Element of REAL n : ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ; registration let n be Element of NAT ; let x1, x2, x3 be Element of REAL n; cluster plane (x1,x2,x3) -> non empty ; coherence not plane (x1,x2,x3) is empty proof A1: 0 * x3 = 0* n by EUCLID_4:3; A2: (1 + 0) + 0 = 1 ; ( 1 * x1 = x1 & 0 * x2 = 0* n ) by EUCLID_4:3; then ((1 * x1) + (0 * x2)) + (0 * x3) = x1 + (0* n) by A1, EUCLID_4:1 .= x1 by EUCLID_4:1 ; then x1 in plane (x1,x2,x3) by A2; hence not plane (x1,x2,x3) is empty ; ::_thesis: verum end; end; definition let n be Element of NAT ; let A be Subset of (REAL n); attrA is being_plane means :Def10: :: EUCLIDLP:def 10 ex x1, x2, x3 being Element of REAL n st ( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) ); end; :: deftheorem Def10 defines being_plane EUCLIDLP:def_10_:_ for n being Element of NAT for A being Subset of (REAL n) holds ( A is being_plane iff ex x1, x2, x3 being Element of REAL n st ( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) ) ); theorem Th82: :: EUCLIDLP:82 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) ) proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) ) let x1, x2, x3 be Element of REAL n; ::_thesis: ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) ) A1: 0 * x3 = 0* n by EUCLID_4:3; ( 1 * x1 = x1 & 0 * x2 = 0* n ) by EUCLID_4:3; then A2: ((1 * x1) + (0 * x2)) + (0 * x3) = x1 + (0* n) by A1, EUCLID_4:1 .= x1 by EUCLID_4:1 ; A3: 0 * x3 = 0* n by EUCLID_4:3; A4: 1 * x3 = x3 by EUCLID_4:3; ( 0 * x1 = 0* n & 0 * x2 = 0* n ) by EUCLID_4:3; then A5: ((0 * x1) + (0 * x2)) + (1 * x3) = (0* n) + x3 by A4, EUCLID_4:1 .= x3 by EUCLID_4:1 ; ( 0 * x1 = 0* n & 1 * x2 = x2 ) by EUCLID_4:3; then A6: ((0 * x1) + (1 * x2)) + (0 * x3) = x2 + (0* n) by A3, EUCLID_4:1 .= x2 by EUCLID_4:1 ; (0 + 0) + 1 = 1 ; hence ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) ) by A2, A6, A5; ::_thesis: verum end; theorem Th83: :: EUCLIDLP:83 for n being Element of NAT for x1, y1, y2, y3, x2, x3 being Element of REAL n st x1 in plane (y1,y2,y3) & x2 in plane (y1,y2,y3) & x3 in plane (y1,y2,y3) holds plane (x1,x2,x3) c= plane (y1,y2,y3) proof let n be Element of NAT ; ::_thesis: for x1, y1, y2, y3, x2, x3 being Element of REAL n st x1 in plane (y1,y2,y3) & x2 in plane (y1,y2,y3) & x3 in plane (y1,y2,y3) holds plane (x1,x2,x3) c= plane (y1,y2,y3) let x1, y1, y2, y3, x2, x3 be Element of REAL n; ::_thesis: ( x1 in plane (y1,y2,y3) & x2 in plane (y1,y2,y3) & x3 in plane (y1,y2,y3) implies plane (x1,x2,x3) c= plane (y1,y2,y3) ) assume that A1: x1 in plane (y1,y2,y3) and A2: x2 in plane (y1,y2,y3) and A3: x3 in plane (y1,y2,y3) ; ::_thesis: plane (x1,x2,x3) c= plane (y1,y2,y3) ex x29 being Element of REAL n st ( x2 = x29 & ex a21, a22, a23 being Real st ( (a21 + a22) + a23 = 1 & x29 = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ) ) by A2; then consider a21, a22, a23 being Real such that A4: (a21 + a22) + a23 = 1 and A5: x2 = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ; ex x19 being Element of REAL n st ( x1 = x19 & ex a11, a12, a13 being Real st ( (a11 + a12) + a13 = 1 & x19 = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ) ) by A1; then consider a11, a12, a13 being Real such that A6: (a11 + a12) + a13 = 1 and A7: x1 = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in plane (x1,x2,x3) or x in plane (y1,y2,y3) ) assume x in plane (x1,x2,x3) ; ::_thesis: x in plane (y1,y2,y3) then ex x9 being Element of REAL n st ( x = x9 & ex b1, b2, b3 being Real st ( (b1 + b2) + b3 = 1 & x9 = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ) ) ; then consider b1, b2, b3 being Real such that A8: (b1 + b2) + b3 = 1 and A9: x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ; ex x39 being Element of REAL n st ( x3 = x39 & ex a31, a32, a33 being Real st ( (a31 + a32) + a33 = 1 & x39 = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ) ) by A3; then consider a31, a32, a33 being Real such that A10: (a31 + a32) + a33 = 1 and A11: x3 = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ; A12: ((((b1 * a11) + (b2 * a21)) + (b3 * a31)) + (((b1 * a12) + (b2 * a22)) + (b3 * a32))) + (((b1 * a13) + (b2 * a23)) + (b3 * a33)) = ((b1 * ((a11 + a12) + a13)) + (b2 * ((a21 + a22) + a23))) + (b3 * ((a31 + a32) + a33)) .= 1 by A6, A4, A10, A8 ; x = (((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + (b2 * (((a21 * y1) + (a22 * y2)) + (a23 * y3)))) + (b3 * (((a31 * y1) + (a32 * y2)) + (a33 * y3))) by A7, A5, A11, A9, Th22 .= (((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + ((((b2 * a21) * y1) + ((b2 * a22) * y2)) + ((b2 * a23) * y3))) + (b3 * (((a31 * y1) + (a32 * y2)) + (a33 * y3))) by Th22 .= (((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + ((((b2 * a21) * y1) + ((b2 * a22) * y2)) + ((b2 * a23) * y3))) + ((((b3 * a31) * y1) + ((b3 * a32) * y2)) + ((b3 * a33) * y3)) by Th22 .= (((((b1 * a11) + (b2 * a21)) * y1) + (((b1 * a12) + (b2 * a22)) * y2)) + (((b1 * a13) + (b2 * a23)) * y3)) + ((((b3 * a31) * y1) + ((b3 * a32) * y2)) + ((b3 * a33) * y3)) by Th24 .= (((((b1 * a11) + (b2 * a21)) + (b3 * a31)) * y1) + ((((b1 * a12) + (b2 * a22)) + (b3 * a32)) * y2)) + ((((b1 * a13) + (b2 * a23)) + (b3 * a33)) * y3) by Th24 ; hence x in plane (y1,y2,y3) by A12; ::_thesis: verum end; theorem :: EUCLIDLP:84 for n being Element of NAT for A being Subset of (REAL n) for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st ( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) holds 0* n in plane (x1,x2,x3) proof let n be Element of NAT ; ::_thesis: for A being Subset of (REAL n) for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st ( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) holds 0* n in plane (x1,x2,x3) let A be Subset of (REAL n); ::_thesis: for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st ( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) holds 0* n in plane (x1,x2,x3) let x, x1, x2, x3 be Element of REAL n; ::_thesis: ( x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st ( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) implies 0* n in plane (x1,x2,x3) ) assume that A1: x in plane (x1,x2,x3) and A2: ex c1, c2, c3 being Real st ( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) ; ::_thesis: 0* n in plane (x1,x2,x3) consider c1, c2, c3 being Real such that A3: (c1 + c2) + c3 = 0 and A4: x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) by A2; ex x9 being Element of REAL n st ( x = x9 & ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x9 = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) by A1; then consider a1, a2, a3 being Real such that A5: (a1 + a2) + a3 = 1 and A6: x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ; A7: ((a1 + (- c1)) + (a2 + (- c2))) + (a3 + (- c3)) = 1 by A5, A3; 0* n = x - x by Th2 .= (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + ((((- c1) * x1) + ((- c2) * x2)) + ((- c3) * x3)) by A6, A4, Th14 .= (((a1 + (- c1)) * x1) + ((a2 + (- c2)) * x2)) + ((a3 + (- c3)) * x3) by Th24 ; hence 0* n in plane (x1,x2,x3) by A7; ::_thesis: verum end; theorem Th85: :: EUCLIDLP:85 for n being Element of NAT for y1, x1, x2, x3, y2 being Element of REAL n st y1 in plane (x1,x2,x3) & y2 in plane (x1,x2,x3) holds Line (y1,y2) c= plane (x1,x2,x3) proof let n be Element of NAT ; ::_thesis: for y1, x1, x2, x3, y2 being Element of REAL n st y1 in plane (x1,x2,x3) & y2 in plane (x1,x2,x3) holds Line (y1,y2) c= plane (x1,x2,x3) let y1, x1, x2, x3, y2 be Element of REAL n; ::_thesis: ( y1 in plane (x1,x2,x3) & y2 in plane (x1,x2,x3) implies Line (y1,y2) c= plane (x1,x2,x3) ) assume that A1: y1 in plane (x1,x2,x3) and A2: y2 in plane (x1,x2,x3) ; ::_thesis: Line (y1,y2) c= plane (x1,x2,x3) consider y29 being Element of REAL n such that A3: y2 = y29 and A4: ex a21, a22, a23 being Real st ( (a21 + a22) + a23 = 1 & y29 = ((a21 * x1) + (a22 * x2)) + (a23 * x3) ) by A2; consider y19 being Element of REAL n such that A5: y1 = y19 and A6: ex a11, a12, a13 being Real st ( (a11 + a12) + a13 = 1 & y19 = ((a11 * x1) + (a12 * x2)) + (a13 * x3) ) by A1; Line (y1,y2) c= plane (x1,x2,x3) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Line (y1,y2) or x in plane (x1,x2,x3) ) assume x in Line (y1,y2) ; ::_thesis: x in plane (x1,x2,x3) then consider t being Real such that A7: x = ((1 - t) * y1) + (t * y2) ; consider a21, a22, a23 being Real such that A8: (a21 + a22) + a23 = 1 and A9: y29 = ((a21 * x1) + (a22 * x2)) + (a23 * x3) by A4; consider a11, a12, a13 being Real such that A10: (a11 + a12) + a13 = 1 and A11: y19 = ((a11 * x1) + (a12 * x2)) + (a13 * x3) by A6; A12: ((((1 - t) * a11) + (t * a21)) + (((1 - t) * a12) + (t * a22))) + (((1 - t) * a13) + (t * a23)) = ((1 - t) * ((a11 + a12) + a13)) + (t * ((a21 + a22) + a23)) .= (1 - t) + t by A10, A8 .= 1 ; x = (((((1 - t) * a11) * x1) + (((1 - t) * a12) * x2)) + (((1 - t) * a13) * x3)) + (t * (((a21 * x1) + (a22 * x2)) + (a23 * x3))) by A5, A3, A7, A11, A9, Th22 .= (((((1 - t) * a11) * x1) + (((1 - t) * a12) * x2)) + (((1 - t) * a13) * x3)) + ((((t * a21) * x1) + ((t * a22) * x2)) + ((t * a23) * x3)) by Th22 .= (((((1 - t) * a11) + (t * a21)) * x1) + ((((1 - t) * a12) + (t * a22)) * x2)) + ((((1 - t) * a13) + (t * a23)) * x3) by Th24 ; hence x in plane (x1,x2,x3) by A12; ::_thesis: verum end; hence Line (y1,y2) c= plane (x1,x2,x3) ; ::_thesis: verum end; theorem :: EUCLIDLP:86 for n being Element of NAT for A being Subset of (REAL n) for x being Element of REAL n st A is being_plane & x in A & ex a being Real st ( a <> 1 & a * x in A ) holds 0* n in A proof let n be Element of NAT ; ::_thesis: for A being Subset of (REAL n) for x being Element of REAL n st A is being_plane & x in A & ex a being Real st ( a <> 1 & a * x in A ) holds 0* n in A let A be Subset of (REAL n); ::_thesis: for x being Element of REAL n st A is being_plane & x in A & ex a being Real st ( a <> 1 & a * x in A ) holds 0* n in A let x be Element of REAL n; ::_thesis: ( A is being_plane & x in A & ex a being Real st ( a <> 1 & a * x in A ) implies 0* n in A ) assume that A1: A is being_plane and A2: x in A and A3: ex a being Real st ( a <> 1 & a * x in A ) ; ::_thesis: 0* n in A consider a being Real such that A4: a <> 1 and A5: a * x in A by A3; A6: 1 - a <> 0 by A4; A7: (1 - (1 / (1 - a))) + ((1 / (1 - a)) * a) = (1 - (1 / (1 - a))) + (a / (1 - a)) by XCMPLX_1:99 .= 1 + ((- (1 / (1 - a))) + (a / (1 - a))) .= 1 + (((- 1) / (1 - a)) + (a / (1 - a))) by XCMPLX_1:187 .= 1 + (((- 1) + a) / (1 - a)) by XCMPLX_1:62 .= 1 + ((- ((- a) - (- 1))) / (1 - a)) .= 1 + (- ((1 - a) / (1 - a))) by XCMPLX_1:187 .= 1 - ((1 - a) / (1 - a)) .= 1 - 1 by A6, XCMPLX_1:60 .= 0 ; 0* n = 0 * x by EUCLID_4:3 .= ((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x) by A7, EUCLID_4:7 .= ((1 - (1 / (1 - a))) * x) + ((1 / (1 - a)) * (a * x)) by EUCLID_4:4 ; then A8: 0* n in Line (x,(a * x)) ; ex x1, x2, x3 being Element of REAL n st ( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) ) by A1, Def10; then Line (x,(a * x)) c= A by A2, A5, Th85; hence 0* n in A by A8; ::_thesis: verum end; theorem :: EUCLIDLP:87 for a1, a2, a3 being Real for n being Element of NAT for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds 0* n in plane (x1,x2,x3) proof let a1, a2, a3 be Real; ::_thesis: for n being Element of NAT for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds 0* n in plane (x1,x2,x3) let n be Element of NAT ; ::_thesis: for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds 0* n in plane (x1,x2,x3) let x, x1, x2, x3 be Element of REAL n; ::_thesis: ( x in plane (x1,x2,x3) & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 implies 0* n in plane (x1,x2,x3) ) assume that A1: x in plane (x1,x2,x3) and A2: x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) and A3: not (a1 + a2) + a3 = 1 ; ::_thesis: 0* n in plane (x1,x2,x3) ex x9 being Element of REAL n st ( x = x9 & ex a19, a29, a39 being Real st ( (a19 + a29) + a39 = 1 & x9 = ((a19 * x1) + (a29 * x2)) + (a39 * x3) ) ) by A1; then consider a19, a29, a39 being Real such that A4: (a19 + a29) + a39 = 1 and A5: x = ((a19 * x1) + (a29 * x2)) + (a39 * x3) ; A6: ((a1 - a19) + (a2 - a29)) + (a3 - a39) <> 0 by A3, A4; set t = ((a1 - a19) + (a2 - a29)) + (a3 - a39); A7: (((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) + ((a2 - a29) / (((a1 - a19) + (a2 - a29)) + (a3 - a39)))) + ((a3 - a39) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) = (((a1 - a19) + (a2 - a29)) + (a3 - a39)) / (((a1 - a19) + (a2 - a29)) + (a3 - a39)) by XCMPLX_1:63 .= 1 by A6, XCMPLX_1:60 ; A8: 0* n = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((a19 * x1) + (a29 * x2)) + (a39 * x3)) by A2, A5, Th2 .= (((a1 - a19) * x1) + ((a2 - a29) * x2)) + ((a3 - a39) * x3) by Th26 ; 0* n = (1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (0* n) by EUCLID_4:2 .= ((((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a1 - a19)) * x1) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a2 - a29)) * x2)) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a3 - a39)) * x3) by A8, Th22 .= ((((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x1) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a2 - a29)) * x2)) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a3 - a39)) * x3) by XCMPLX_1:99 .= ((((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x1) + (((a2 - a29) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x2)) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a3 - a39)) * x3) by XCMPLX_1:99 .= ((((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x1) + (((a2 - a29) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x2)) + (((a3 - a39) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x3) by XCMPLX_1:99 ; hence 0* n in plane (x1,x2,x3) by A7; ::_thesis: verum end; theorem Th88: :: EUCLIDLP:88 for n being Element of NAT for x, x1, x2, x3 being Element of REAL n holds ( x in plane (x1,x2,x3) iff ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) proof let n be Element of NAT ; ::_thesis: for x, x1, x2, x3 being Element of REAL n holds ( x in plane (x1,x2,x3) iff ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) let x, x1, x2, x3 be Element of REAL n; ::_thesis: ( x in plane (x1,x2,x3) iff ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) thus ( x in plane (x1,x2,x3) implies ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) ::_thesis: ( ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) implies x in plane (x1,x2,x3) ) proof assume x in plane (x1,x2,x3) ; ::_thesis: ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) then ex x9 being Element of REAL n st ( x = x9 & ex a19, a29, a39 being Real st ( (a19 + a29) + a39 = 1 & x9 = ((a19 * x1) + (a29 * x2)) + (a39 * x3) ) ) ; hence ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ; ::_thesis: verum end; thus ( ex a1, a2, a3 being Real st ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) implies x in plane (x1,x2,x3) ) ; ::_thesis: verum end; theorem :: EUCLIDLP:89 for a1, a2, a3, b1, b2, b3 being Real for n being Element of NAT for x2, x1, x3, x being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds ( a1 = b1 & a2 = b2 & a3 = b3 ) proof let a1, a2, a3, b1, b2, b3 be Real; ::_thesis: for n being Element of NAT for x2, x1, x3, x being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds ( a1 = b1 & a2 = b2 & a3 = b3 ) let n be Element of NAT ; ::_thesis: for x2, x1, x3, x being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds ( a1 = b1 & a2 = b2 & a3 = b3 ) let x2, x1, x3, x be Element of REAL n; ::_thesis: ( x2 - x1,x3 - x1 are_lindependent2 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) implies ( a1 = b1 & a2 = b2 & a3 = b3 ) ) assume A1: x2 - x1,x3 - x1 are_lindependent2 ; ::_thesis: ( not (a1 + a2) + a3 = 1 or not x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) or not (b1 + b2) + b3 = 1 or not x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) or ( a1 = b1 & a2 = b2 & a3 = b3 ) ) assume that A2: (a1 + a2) + a3 = 1 and A3: x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) and A4: (b1 + b2) + b3 = 1 and A5: x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ; ::_thesis: ( a1 = b1 & a2 = b2 & a3 = b3 ) a1 = (1 - a2) - a3 by A2; then x = ((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by A3, Th13 .= (((x1 + (- (a2 * x1))) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by EUCLID_4:3 .= (((x1 + (- (a2 * x1))) + (a2 * x2)) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15 .= ((x1 + ((a2 * x2) + (- (a2 * x1)))) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15 .= (x1 + ((a2 * x2) + (- (a2 * x1)))) + ((a3 * x3) + (- (a3 * x1))) by RVSUM_1:15 .= (x1 + ((a2 * x2) + (a2 * (- x1)))) + ((a3 * x3) + (- (a3 * x1))) by Th3 .= (x1 + ((a2 * x2) + (a2 * (- x1)))) + ((a3 * x3) + (a3 * (- x1))) by Th3 .= (x1 + (a2 * (x2 + (- x1)))) + ((a3 * x3) + (a3 * (- x1))) by EUCLID_4:6 .= (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) by EUCLID_4:6 ; then A6: x - x1 = (a2 * (x2 - x1)) + (a3 * (x3 - x1)) by Th7; x = ((((1 - b2) - b3) * x1) + (b2 * x2)) + (b3 * x3) by A4, A5 .= ((((1 * x1) - (b2 * x1)) - (b3 * x1)) + (b2 * x2)) + (b3 * x3) by Th13 .= (((x1 + (- (b2 * x1))) - (b3 * x1)) + (b2 * x2)) + (b3 * x3) by EUCLID_4:3 .= (((x1 + (- (b2 * x1))) + (b2 * x2)) + (- (b3 * x1))) + (b3 * x3) by RVSUM_1:15 .= ((x1 + ((b2 * x2) + (- (b2 * x1)))) + (- (b3 * x1))) + (b3 * x3) by RVSUM_1:15 .= (x1 + ((b2 * x2) + (- (b2 * x1)))) + ((b3 * x3) + (- (b3 * x1))) by RVSUM_1:15 .= (x1 + ((b2 * x2) + (b2 * (- x1)))) + ((b3 * x3) + (- (b3 * x1))) by Th3 .= (x1 + ((b2 * x2) + (b2 * (- x1)))) + ((b3 * x3) + (b3 * (- x1))) by Th3 .= (x1 + (b2 * (x2 + (- x1)))) + ((b3 * x3) + (b3 * (- x1))) by EUCLID_4:6 .= (x1 + (b2 * (x2 - x1))) + (b3 * (x3 - x1)) by EUCLID_4:6 ; then (a2 * (x2 - x1)) + (a3 * (x3 - x1)) = (b2 * (x2 - x1)) + (b3 * (x3 - x1)) by A6, Th7; then ( a2 = b2 & a3 = b3 ) by A1, Th35; hence ( a1 = b1 & a2 = b2 & a3 = b3 ) by A2, A4; ::_thesis: verum end; definition let n be Element of NAT ; func plane_of_REAL n -> Subset-Family of (REAL n) equals :: EUCLIDLP:def 11 { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ; correctness coherence { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } is Subset-Family of (REAL n); proof set A = { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ; { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } c= bool (REAL n) proof let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } or P in bool (REAL n) ) assume P in { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ; ::_thesis: P in bool (REAL n) then ex P9 being Subset of (REAL n) st ( P = P9 & ex x1, x2, x3 being Element of REAL n st P9 = plane (x1,x2,x3) ) ; hence P in bool (REAL n) ; ::_thesis: verum end; hence { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } is Subset-Family of (REAL n) ; ::_thesis: verum end; end; :: deftheorem defines plane_of_REAL EUCLIDLP:def_11_:_ for n being Element of NAT holds plane_of_REAL n = { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ; registration let n be Element of NAT ; cluster plane_of_REAL n -> non empty ; coherence not plane_of_REAL n is empty proof reconsider P = plane ((0* n),(1* n),(1* n)) as Subset of (REAL n) ; P in plane_of_REAL n ; hence not plane_of_REAL n is empty ; ::_thesis: verum end; end; theorem Th90: :: EUCLIDLP:90 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds plane (x1,x2,x3) in plane_of_REAL n ; theorem Th91: :: EUCLIDLP:91 for n being Element of NAT 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 holds plane (x1,x2,x3) c= P proof let n be Element of 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 holds plane (x1,x2,x3) c= P 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 holds plane (x1,x2,x3) c= P let P be Element of plane_of_REAL n; ::_thesis: ( x1 in P & x2 in P & x3 in P implies plane (x1,x2,x3) c= P ) P in plane_of_REAL n ; then A1: 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) ) ; assume ( x1 in P & x2 in P & x3 in P ) ; ::_thesis: plane (x1,x2,x3) c= P hence plane (x1,x2,x3) c= P by A1, Th83; ::_thesis: verum end; theorem Th92: :: EUCLIDLP:92 for n being Element of NAT 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) proof let n be Element of 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_set_st_y_in_P_holds_ y_in_plane_(x1,x2,x3) let y be set ; ::_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) by TARSKI:def_3; 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 end; theorem :: EUCLIDLP:93 for n being Element of NAT for P1, P2 being Element of plane_of_REAL n st P1 is being_plane & P1 c= P2 holds P1 = P2 proof let n be Element of NAT ; ::_thesis: for P1, P2 being Element of plane_of_REAL n st P1 is being_plane & P1 c= P2 holds P1 = P2 let P1, P2 be Element of plane_of_REAL n; ::_thesis: ( P1 is being_plane & P1 c= P2 implies P1 = P2 ) assume that A1: P1 is being_plane and A2: P1 c= P2 ; ::_thesis: P1 = P2 consider x1, x2, x3 being Element of REAL n such that A3: ( x2 - x1,x3 - x1 are_lindependent2 & P1 = plane (x1,x2,x3) ) by A1, Def10; A4: x3 in plane (x1,x2,x3) by Th82; ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) ) by Th82; hence P1 = P2 by A2, A3, A4, Th92; ::_thesis: verum end; theorem :: EUCLIDLP:94 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds ( Line (x1,x2) c= plane (x1,x2,x3) & Line (x2,x3) c= plane (x1,x2,x3) & Line (x3,x1) c= plane (x1,x2,x3) ) proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds ( Line (x1,x2) c= plane (x1,x2,x3) & Line (x2,x3) c= plane (x1,x2,x3) & Line (x3,x1) c= plane (x1,x2,x3) ) let x1, x2, x3 be Element of REAL n; ::_thesis: ( Line (x1,x2) c= plane (x1,x2,x3) & Line (x2,x3) c= plane (x1,x2,x3) & Line (x3,x1) c= plane (x1,x2,x3) ) A1: x3 in plane (x1,x2,x3) by Th82; ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) ) by Th82; hence ( Line (x1,x2) c= plane (x1,x2,x3) & Line (x2,x3) c= plane (x1,x2,x3) & Line (x3,x1) c= plane (x1,x2,x3) ) by A1, Th85; ::_thesis: verum end; theorem Th95: :: EUCLIDLP:95 for n being Element of NAT for x1, x2 being Element of REAL n for P being Element of plane_of_REAL n st x1 in P & x2 in P holds Line (x1,x2) c= P proof let n be Element of NAT ; ::_thesis: for x1, x2 being Element of REAL n for P being Element of plane_of_REAL n st x1 in P & x2 in P holds Line (x1,x2) c= P let x1, x2 be Element of REAL n; ::_thesis: for P being Element of plane_of_REAL n st x1 in P & x2 in P holds Line (x1,x2) c= P let P be Element of plane_of_REAL n; ::_thesis: ( x1 in P & x2 in P implies Line (x1,x2) c= P ) P in plane_of_REAL n ; then A1: 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) ) ; assume ( x1 in P & x2 in P ) ; ::_thesis: Line (x1,x2) c= P hence Line (x1,x2) c= P by A1, Th85; ::_thesis: verum end; definition let n be Element of NAT ; let L1, L2 be Element of line_of_REAL n; predL1,L2 are_coplane means :Def12: :: EUCLIDLP:def 12 ex x1, x2, x3 being Element of REAL n st ( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ); end; :: deftheorem Def12 defines are_coplane EUCLIDLP:def_12_:_ for n being Element of NAT for L1, L2 being Element of line_of_REAL n holds ( L1,L2 are_coplane iff ex x1, x2, x3 being Element of REAL n st ( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) ); theorem Th96: :: EUCLIDLP:96 for n being Element of NAT for L1, L2 being Element of line_of_REAL n holds ( L1,L2 are_coplane iff ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n holds ( L1,L2 are_coplane iff ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1,L2 are_coplane iff ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) ) thus ( L1,L2 are_coplane implies ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) ) ::_thesis: ( ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) implies L1,L2 are_coplane ) proof assume L1,L2 are_coplane ; ::_thesis: ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) then consider x1, x2, x3 being Element of REAL n such that A1: ( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) by Def12; set P = plane (x1,x2,x3); take plane (x1,x2,x3) ; ::_thesis: ( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) thus ( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) by A1, Th90; ::_thesis: verum end; now__::_thesis:_(_ex_P_being_Element_of_plane_of_REAL_n_st_ (_L1_c=_P_&_L2_c=_P_)_implies_L1,L2_are_coplane_) assume ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) ; ::_thesis: L1,L2 are_coplane then consider P being Element of plane_of_REAL n such that A2: ( L1 c= P & L2 c= P ) ; P in plane_of_REAL n ; then ex P9 being Subset of (REAL n) st ( P = P9 & ex x1, x2, x3 being Element of REAL n st P9 = plane (x1,x2,x3) ) ; hence L1,L2 are_coplane by A2, Def12; ::_thesis: verum end; hence ( ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) implies L1,L2 are_coplane ) ; ::_thesis: verum end; theorem Th97: :: EUCLIDLP:97 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 // L2 holds L1,L2 are_coplane proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 // L2 holds L1,L2 are_coplane let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 // L2 implies L1,L2 are_coplane ) assume L1 // L2 ; ::_thesis: L1,L2 are_coplane then consider x1, x2, y1, y2 being Element of REAL n such that A1: L1 = Line (x1,x2) and A2: L2 = Line (y1,y2) and A3: x2 - x1 // y2 - y1 by Def7; consider a being Real such that a <> 0 and A4: x2 - x1 = a * (y2 - y1) by A3, Th32; A5: (1 + (- a)) + a = 1 ; ( y1 in plane (x1,y1,y2) & y2 in plane (x1,y1,y2) ) by Th82; then A6: L2 c= plane (x1,y1,y2) by A2, Th85; x2 = x1 + (a * (y2 - y1)) by A4, Th6 .= (1 * x1) + (a * (y2 - y1)) by EUCLID_4:3 .= (1 * x1) + ((a * y2) + ((- a) * y1)) by Th12 .= ((1 * x1) + ((- a) * y1)) + (a * y2) by RVSUM_1:15 ; then A7: x2 in plane (x1,y1,y2) by A5; x1 in plane (x1,y1,y2) by Th82; then L1 c= plane (x1,y1,y2) by A1, A7, Th85; hence L1,L2 are_coplane by A6, Def12; ::_thesis: verum end; theorem Th98: :: EUCLIDLP:98 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 misses L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 misses L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 misses L2 implies ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) ) assume that A1: L1 is being_line and A2: L2 is being_line and A3: L1,L2 are_coplane ; ::_thesis: ( not L1 misses L2 or ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) ) consider x1, x2, x3 being Element of REAL n such that A4: ( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) by A3, Def12; consider y2, y3 being Element of REAL n such that y2 <> y3 and A5: L2 = Line (y2,y3) by A2, EUCLID_4:def_2; consider y0, y1 being Element of REAL n such that A6: y0 <> y1 and A7: L1 = Line (y0,y1) by A1, EUCLID_4:def_2; A8: y0 - y1 <> 0* n by A6, Th9; set P = plane (x1,x2,x3); A9: y2 in L2 by A5, EUCLID_4:9; consider y being Element of REAL n such that A10: y in Line (y0,y1) and A11: y0 - y1,y2 - y are_orthogonal by Th43; assume L1 misses L2 ; ::_thesis: ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) then A12: y <> y2 by A7, A9, A10, XBOOLE_0:3; then y2 - y <> 0* n by Th9; then A13: y0 - y1 _|_ y2 - y by A11, A8, Def3; consider y9 being Element of REAL n such that A14: y <> y9 and A15: y9 in L1 by A1, EUCLID_4:14; take plane (x1,x2,x3) ; ::_thesis: ( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) & plane (x1,x2,x3) is being_plane ) ( y in Line (y,y2) & y2 in Line (y,y2) ) by EUCLID_4:9; then A16: ( plane (x1,x2,x3) in plane_of_REAL n & y9 - y,y2 - y are_lindependent2 ) by A7, A10, A12, A13, A14, A15, Th40, Th45; then plane (x1,x2,x3) = plane (y,y9,y2) by A4, A7, A9, A10, A15, Th92; hence ( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) & plane (x1,x2,x3) is being_plane ) by A4, A16, Def10; ::_thesis: verum end; theorem Th99: :: EUCLIDLP:99 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n ex P being Element of plane_of_REAL n st ( x in P & L c= P ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n ex P being Element of plane_of_REAL n st ( x in P & L c= P ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n ex P being Element of plane_of_REAL n st ( x in P & L c= P ) let L be Element of line_of_REAL n; ::_thesis: ex P being Element of plane_of_REAL n st ( x in P & L c= P ) L in line_of_REAL n ; then consider x1, x2 being Element of REAL n such that A1: L = Line (x1,x2) ; take P = plane (x,x1,x2); ::_thesis: ( P is Element of plane_of_REAL n & x in P & L c= P ) ( x1 in P & x2 in P ) by Th82; hence ( P is Element of plane_of_REAL n & x in P & L c= P ) by A1, Th82, Th85, Th90; ::_thesis: verum end; theorem Th100: :: EUCLIDLP:100 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex P being Element of plane_of_REAL n st ( x in P & L c= P & P is being_plane ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n st not x in L & L is being_line holds ex P being Element of plane_of_REAL n st ( x in P & L c= P & P is being_plane ) let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n st not x in L & L is being_line holds ex P being Element of plane_of_REAL n st ( x in P & L c= P & P is being_plane ) let L be Element of line_of_REAL n; ::_thesis: ( not x in L & L is being_line implies ex P being Element of plane_of_REAL n st ( x in P & L c= P & P is being_plane ) ) consider P being Element of plane_of_REAL n such that A1: ( x in P & L c= P ) by Th99; assume ( not x in L & L is being_line ) ; ::_thesis: ex P being Element of plane_of_REAL n st ( x in P & L c= P & P is being_plane ) then consider x1, x2 being Element of REAL n such that A2: L = Line (x1,x2) and A3: x - x1,x2 - x1 are_lindependent2 by Th55; take P ; ::_thesis: ( x in P & L c= P & P is being_plane ) ( x1 in L & x2 in L ) by A2, EUCLID_4:9; then P = plane (x1,x,x2) by A1, A3, Th92; hence ( x in P & L c= P & P is being_plane ) by A1, A3, Def10; ::_thesis: verum end; theorem Th101: :: EUCLIDLP:101 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n for P being Element of plane_of_REAL n st x in P & L c= P & not x in L & L is being_line holds P is being_plane proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n for P being Element of plane_of_REAL n st x in P & L c= P & not x in L & L is being_line holds P is being_plane let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n for P being Element of plane_of_REAL n st x in P & L c= P & not x in L & L is being_line holds P is being_plane let L be Element of line_of_REAL n; ::_thesis: for P being Element of plane_of_REAL n st x in P & L c= P & not x in L & L is being_line holds P is being_plane let P be Element of plane_of_REAL n; ::_thesis: ( x in P & L c= P & not x in L & L is being_line implies P is being_plane ) assume A1: ( x in P & L c= P ) ; ::_thesis: ( x in L or not L is being_line or P is being_plane ) assume ( not x in L & L is being_line ) ; ::_thesis: P is being_plane then consider x1, x2 being Element of REAL n such that A2: L = Line (x1,x2) and A3: x - x1,x2 - x1 are_lindependent2 by Th55; ( x1 in L & x2 in L ) by A2, EUCLID_4:9; then P = plane (x1,x,x2) by A1, A3, Th92; hence P is being_plane by A3, Def10; ::_thesis: verum end; theorem Th102: :: EUCLIDLP:102 for n being Element of NAT for x being Element of REAL n for L being Element of line_of_REAL n for P0, P1 being Element of plane_of_REAL n st not x in L & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 holds P0 = P1 proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L being Element of line_of_REAL n for P0, P1 being Element of plane_of_REAL n st not x in L & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 holds P0 = P1 let x be Element of REAL n; ::_thesis: for L being Element of line_of_REAL n for P0, P1 being Element of plane_of_REAL n st not x in L & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 holds P0 = P1 let L be Element of line_of_REAL n; ::_thesis: for P0, P1 being Element of plane_of_REAL n st not x in L & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 holds P0 = P1 let P0, P1 be Element of plane_of_REAL n; ::_thesis: ( not x in L & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 implies P0 = P1 ) assume that A1: ( not x in L & L is being_line ) and A2: ( x in P0 & L c= P0 ) and A3: ( x in P1 & L c= P1 ) ; ::_thesis: P0 = P1 consider x1, x2 being Element of REAL n such that A4: L = Line (x1,x2) and A5: x - x1,x2 - x1 are_lindependent2 by A1, Th55; A6: ( x1 in L & x2 in L ) by A4, EUCLID_4:9; then P0 = plane (x1,x,x2) by A2, A5, Th92; hence P0 = P1 by A3, A5, A6, Th92; ::_thesis: verum end; theorem :: EUCLIDLP:103 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 <> L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 <> L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 <> L2 implies ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) ) assume that A1: L1 is being_line and A2: ( L2 is being_line & L1,L2 are_coplane & L1 <> L2 ) ; ::_thesis: ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) ( ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P ) & ex x being Element of REAL n st ( x in L2 & not x in L1 ) ) by A1, A2, Th79, Th96; hence ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) by A1, Th101; ::_thesis: verum end; theorem :: EUCLIDLP:104 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 implies ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) ) assume that A1: L1 is being_line and A2: L2 is being_line and A3: L1 <> L2 and A4: L1 meets L2 ; ::_thesis: ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) consider x being Element of REAL n such that A5: x in L1 and A6: not x in L2 by A1, A2, A3, Th79; A7: ex P being Element of plane_of_REAL n st ( x in P & L2 c= P & P is being_plane ) by A2, A6, Th100; consider y being Element of REAL n such that A8: y in L1 and A9: y in L2 by A4, Th49; L1 = Line (x,y) by A1, A5, A6, A8, A9, Th30; hence ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) by A7, A9, Th95; ::_thesis: verum end; theorem :: EUCLIDLP:105 for n being Element of NAT for L1, L2 being Element of line_of_REAL n for P1, P2 being Element of plane_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds P1 = P2 proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n for P1, P2 being Element of plane_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds P1 = P2 let L1, L2 be Element of line_of_REAL n; ::_thesis: for P1, P2 being Element of plane_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds P1 = P2 let P1, P2 be Element of plane_of_REAL n; ::_thesis: ( L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 implies P1 = P2 ) assume that A1: L1 is being_line and A2: L2 is being_line and A3: L1 <> L2 and A4: ( L1 c= P1 & L2 c= P1 ) and A5: ( L1 c= P2 & L2 c= P2 ) ; ::_thesis: P1 = P2 consider x being Element of REAL n such that A6: x in L1 and A7: not x in L2 by A1, A2, A3, Th79; consider x1, x2 being Element of REAL n such that A8: L2 = Line (x1,x2) and A9: x - x1,x2 - x1 are_lindependent2 by A2, A7, Th55; A10: ( x1 in L2 & x2 in L2 ) by A8, EUCLID_4:9; then P2 = plane (x1,x,x2) by A5, A6, A9, Th92; hence P1 = P2 by A4, A6, A9, A10, Th92; ::_thesis: verum end; theorem Th106: :: EUCLIDLP:106 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 // L2 & L1 <> L2 implies ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) ) assume that A1: L1 // L2 and A2: L1 <> L2 ; ::_thesis: ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) A3: L2 is being_line by A1, Th66; ( L1,L2 are_coplane & L1 is being_line ) by A1, Th66, Th97; hence ex P being Element of plane_of_REAL n st ( L1 c= P & L2 c= P & P is being_plane ) by A1, A2, A3, Th71, Th98; ::_thesis: verum end; theorem Th107: :: EUCLIDLP:107 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & L1 meets L2 holds ex P being Element of plane_of_REAL n st ( P is being_plane & L1 c= P & L2 c= P ) proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & L1 meets L2 holds ex P being Element of plane_of_REAL n st ( P is being_plane & L1 c= P & L2 c= P ) let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1 _|_ L2 & L1 meets L2 implies ex P being Element of plane_of_REAL n st ( P is being_plane & L1 c= P & L2 c= P ) ) assume that A1: L1 _|_ L2 and A2: L1 meets L2 ; ::_thesis: ex P being Element of plane_of_REAL n st ( P is being_plane & L1 c= P & L2 c= P ) consider x1 being Element of REAL n such that A3: x1 in L1 and A4: x1 in L2 by A2, Th49; L1 is being_line by A1, Th67; then consider x2 being Element of REAL n such that A5: ( x2 <> x1 & x2 in L1 ) by Th53; A6: L1 = Line (x1,x2) by A3, A5, Th64; L2 is being_line by A1, Th67; then consider x3 being Element of REAL n such that A7: ( x3 <> x1 & x3 in L2 ) by Th53; reconsider P = plane (x1,x2,x3) as Subset of (REAL n) ; take P ; ::_thesis: ( P is Element of plane_of_REAL n & P is being_plane & L1 c= P & L2 c= P ) A8: ( x1 in P & x2 in P ) by Th82; A9: x3 in P by Th82; A10: L2 = Line (x1,x3) by A4, A7, Th64; x2 - x1,x3 - x1 are_lindependent2 by A1, A3, A4, A5, A7, Th45, Th74; hence ( P is Element of plane_of_REAL n & P is being_plane & L1 c= P & L2 c= P ) by A6, A10, A8, A9, Def10, Th85, Th90; ::_thesis: verum end; theorem Th108: :: EUCLIDLP:108 for n being Element of NAT for x being Element of REAL n for L0, L1, L2 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds L0 = L1 proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L0, L1, L2 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds L0 = L1 let x be Element of REAL n; ::_thesis: for L0, L1, L2 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds L0 = L1 let L0, L1, L2 be Element of line_of_REAL n; ::_thesis: for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds L0 = L1 let P be Element of plane_of_REAL n; ::_thesis: ( L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 implies L0 = L1 ) assume that A1: L0 c= P and A2: L1 c= P and A3: L2 c= P and A4: x in L0 and A5: x in L1 and A6: x in L2 ; ::_thesis: ( not L0 _|_ L2 or not L1 _|_ L2 or L0 = L1 ) A7: L1 meets L0 by A4, A5, Th49; assume that A8: L0 _|_ L2 and A9: L1 _|_ L2 ; ::_thesis: L0 = L1 consider x0 being Element of REAL n such that A10: x <> x0 and A11: x0 in L0 and not x0 in L2 by A6, A8, Th81; L1 is being_line by A9, Th67; then consider x1 being Element of REAL n such that A12: x1 <> x and A13: x1 in L1 by Th53; consider x2 being Element of REAL n such that A14: x <> x2 and A15: x2 in L2 and not x2 in L1 by A5, A9, Th81; A16: x0 - x _|_ x2 - x by A4, A6, A8, A10, A11, A14, A15, Th74; then P = plane (x,x0,x2) by A1, A3, A4, A11, A15, Th45, Th92; then consider a1, a2, a3 being Real such that A17: ( (a1 + a2) + a3 = 1 & x1 = ((a1 * x) + (a2 * x0)) + (a3 * x2) ) by A2, A13, Th88; x0 - x,x2 - x are_orthogonal by A16, Def3; then A18: |((x0 - x),(x2 - x))| = 0 by RVSUM_1:def_17; A19: x1 - x = (- x) + ((x + (a2 * (x0 - x))) + (a3 * (x2 - x))) by A17, Th27 .= (- x) + (x + ((a2 * (x0 - x)) + (a3 * (x2 - x)))) by RVSUM_1:15 .= ((- x) + x) + ((a2 * (x0 - x)) + (a3 * (x2 - x))) by RVSUM_1:15 .= (0* n) + ((a2 * (x0 - x)) + (a3 * (x2 - x))) by Th2 .= (a2 * (x0 - x)) + (a3 * (x2 - x)) by EUCLID_4:1 ; x2 - x <> 0* n by A14, Th9; then A20: |((x2 - x),(x2 - x))| <> 0 by EUCLID_4:17; x1 - x _|_ x2 - x by A5, A6, A9, A14, A15, A12, A13, Th74; then x1 - x,x2 - x are_orthogonal by Def3; then 0 = |(((a2 * (x0 - x)) + (a3 * (x2 - x))),(x2 - x))| by A19, RVSUM_1:def_17 .= |((a2 * (x0 - x)),(x2 - x))| + |((a3 * (x2 - x)),(x2 - x))| by EUCLID_4:20 .= (a2 * |((x0 - x),(x2 - x))|) + |((a3 * (x2 - x)),(x2 - x))| by EUCLID_4:21 .= a3 * |((x2 - x),(x2 - x))| by A18, EUCLID_4:21 ; then A21: x1 - x = (a2 * (x0 - x)) + (0 * (x2 - x)) by A19, A20, XCMPLX_1:6 .= (a2 * (x0 - x)) + (0* n) by EUCLID_4:3 .= a2 * (x0 - x) by EUCLID_4:1 ; A22: x0 - x <> 0* n by A10, Th9; x1 - x <> 0* n by A12, Th9; then A23: x1 - x // x0 - x by A21, A22, Def1; A24: L1 = Line (x,x1) by A5, A12, A13, Th64; L0 = Line (x,x0) by A4, A10, A11, Th64; then L1 // L0 by A24, A23, Def7; hence L0 = L1 by A7, Th71; ::_thesis: verum end; theorem Th109: :: EUCLIDLP:109 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 _|_ L2 holds L1 meets L2 proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 _|_ L2 holds L1 meets L2 let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1,L2 are_coplane & L1 _|_ L2 implies L1 meets L2 ) assume A1: L1,L2 are_coplane ; ::_thesis: ( not L1 _|_ L2 or L1 meets L2 ) assume A2: L1 _|_ L2 ; ::_thesis: L1 meets L2 then A3: L2 is being_line by Th67; L1 is being_line by A2, Th67; then consider x0 being Element of REAL n such that A4: x0 in L1 and A5: not x0 in L2 by A2, A3, Th75, Th79; consider L being Element of line_of_REAL n such that A6: x0 in L and A7: L _|_ L2 and A8: L meets L2 by A3, A5, Th62; consider x being Element of REAL n such that A9: x in L and A10: x in L2 by A8, Th49; x in L1 proof A11: L1 meets L by A4, A6, Th49; consider P being Element of plane_of_REAL n such that P is being_plane and A12: ( L c= P & L2 c= P ) by A7, A8, Th107; consider P0 being Element of plane_of_REAL n such that A13: ( L1 c= P0 & L2 c= P0 ) by A1, Th96; A14: P = P0 by A3, A4, A5, A6, A13, A12, Th102; consider L0 being Element of line_of_REAL n such that A15: x in L0 and A16: L0 _|_ L2 and A17: L0 // L1 by A2, Th80; assume A18: not x in L1 ; ::_thesis: contradiction then consider P1 being Element of plane_of_REAL n such that A19: L0 c= P1 and A20: L1 c= P1 and P1 is being_plane by A15, A17, Th106; L1 is being_line by A17, Th66; then P = P1 by A10, A18, A13, A14, A15, A19, A20, Th102; then L = L0 by A7, A9, A10, A12, A15, A16, A19, Th108; hence contradiction by A18, A15, A17, A11, Th71; ::_thesis: verum end; hence L1 meets L2 by A10, Th49; ::_thesis: verum end; theorem Th110: :: EUCLIDLP:110 for n being Element of NAT for x being Element of REAL n for L1, L2, L0 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds ( L0 c= P & L0 _|_ L1 ) proof let n be Element of NAT ; ::_thesis: for x being Element of REAL n for L1, L2, L0 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds ( L0 c= P & L0 _|_ L1 ) let x be Element of REAL n; ::_thesis: for L1, L2, L0 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds ( L0 c= P & L0 _|_ L1 ) let L1, L2, L0 be Element of line_of_REAL n; ::_thesis: for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds ( L0 c= P & L0 _|_ L1 ) let P be Element of plane_of_REAL n; ::_thesis: ( L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 implies ( L0 c= P & L0 _|_ L1 ) ) assume that A1: ( L1 c= P & L2 c= P ) and A2: L1 _|_ L2 and A3: x in P ; ::_thesis: ( not L0 // L2 or not x in L0 or ( L0 c= P & L0 _|_ L1 ) ) L1,L2 are_coplane by A1, Th96; then L1 meets L2 by A2, Th109; then consider x0 being Element of REAL n such that A4: x0 in L1 and A5: x0 in L2 by Th49; L2 is being_line by A2, Th67; then consider x1 being Element of REAL n such that A6: x1 <> x0 and A7: x1 in L2 by Th53; A8: plane (x,x1,x0) c= P by A1, A3, A4, A7, Th91; assume that A9: L0 // L2 and A10: x in L0 ; ::_thesis: ( L0 c= P & L0 _|_ L1 ) L0 is being_line by A9, Th66; then consider x2 being Element of REAL n such that A11: ( x2 <> x & x2 in L0 ) by Th53; consider a being Real such that a <> 0 and A12: x2 - x = a * (x1 - x0) by A9, A10, A5, A6, A7, A11, Th32, Th77; A13: (1 + a) + (- a) = 1 ; x2 = x + (a * (x1 - x0)) by A12, Th6 .= (1 * x) + (a * (x1 - x0)) by EUCLID_4:3 .= (1 * x) + ((a * x1) + ((- a) * x0)) by Th12 .= ((1 * x) + (a * x1)) + ((- a) * x0) by RVSUM_1:15 ; then A14: x2 in plane (x,x1,x0) by A13; L0 = Line (x2,x) by A10, A11, Th64; hence ( L0 c= P & L0 _|_ L1 ) by A2, A3, A9, A14, A8, Th61, Th95; ::_thesis: verum end; theorem Th111: :: EUCLIDLP:111 for n being Element of NAT for L, L1, L2 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds L1 // L2 proof let n be Element of NAT ; ::_thesis: for L, L1, L2 being Element of line_of_REAL n for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds L1 // L2 let L, L1, L2 be Element of line_of_REAL n; ::_thesis: for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds L1 // L2 let P be Element of plane_of_REAL n; ::_thesis: ( L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 implies L1 // L2 ) assume that A1: L c= P and A2: L1 c= P and A3: L2 c= P ; ::_thesis: ( not L _|_ L1 or not L _|_ L2 or L1 // L2 ) assume that A4: L _|_ L1 and A5: L _|_ L2 ; ::_thesis: L1 // L2 L,L2 are_coplane by A1, A3, Th96; then L meets L2 by A5, Th109; then consider x2 being Element of REAL n such that A6: x2 in L and A7: x2 in L2 by Th49; A8: L1 is being_line by A4, Th67; L,L1 are_coplane by A1, A2, Th96; then L meets L1 by A4, Th109; then consider x1 being Element of REAL n such that A9: x1 in L and A10: x1 in L1 by Th49; A11: L2 is being_line by A5, Th67; now__::_thesis:_(_(_x1_=_x2_&_L1_//_L2_)_or_(_x1_<>_x2_&_L1_//_L2_)_) percases ( x1 = x2 or x1 <> x2 ) ; case x1 = x2 ; ::_thesis: L1 // L2 hence L1 // L2 by A1, A2, A3, A4, A5, A9, A10, A7, A8, Th65, Th108; ::_thesis: verum end; caseA12: x1 <> x2 ; ::_thesis: L1 // L2 then x1 - x2 <> 0* n by Th9; then A13: |((x1 - x2),(x1 - x2))| <> 0 by EUCLID_4:17; consider x being Element of REAL n such that A14: x <> x2 and A15: x in L2 by A11, Th53; A16: L2 = Line (x2,x) by A7, A14, A15, Th64; consider x0 being Element of REAL n such that A17: x0 <> x1 and A18: x0 in L1 by A8, Th53; A19: L1 = Line (x0,x1) by A10, A17, A18, Th64; A20: x0 - x1 _|_ x2 - x1 by A4, A9, A10, A6, A12, A17, A18, Th74; then x0 - x1,x2 - x1 are_orthogonal by Def3; then A21: |((x0 - x1),(x2 - x1))| = 0 by RVSUM_1:def_17; P = plane (x1,x0,x2) by A1, A2, A9, A6, A18, A20, Th45, Th92; then consider a1, a3, a2 being Real such that A22: (a1 + a3) + a2 = 1 and A23: x = ((a1 * x1) + (a3 * x0)) + (a2 * x2) by A3, A15, Th88; A24: (a2 + a1) + a3 = 1 by A22; A25: x - x2 = (- x2) + (((a2 * x2) + (a1 * x1)) + (a3 * x0)) by A23, RVSUM_1:15 .= (- x2) + ((x2 + (a1 * (x1 - x2))) + (a3 * (x0 - x2))) by A24, Th27 .= (- x2) + (x2 + ((a1 * (x1 - x2)) + (a3 * (x0 - x2)))) by RVSUM_1:15 .= ((- x2) + x2) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))) by RVSUM_1:15 .= (0* n) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))) by Th2 .= (a1 * (x1 - x2)) + (a3 * (x0 - x2)) by EUCLID_4:1 ; A26: |((x0 - x1),(x1 - x2))| = |((x0 - x1),(((- 1) * x2) + (- (- x1))))| .= |((x0 - x1),((- 1) * (x2 + (- x1))))| by EUCLID_4:6 .= (- 1) * |((x0 - x1),(x2 - x1))| by EUCLID_4:22 .= 0 by A21 ; A27: x0 - x2 = x0 - ((0* n) + x2) by EUCLID_4:1 .= x0 - ((x1 - x1) + x2) by Th2 .= (x0 - (x1 - x1)) - x2 by RVSUM_1:39 .= ((x0 - x1) + x1) - x2 by Th4 .= (x0 - x1) + (x1 - x2) by Th5 ; x - x2 _|_ x1 - x2 by A5, A9, A6, A7, A12, A14, A15, Th74; then x - x2,x1 - x2 are_orthogonal by Def3; then 0 = |(((a1 * (x1 - x2)) + (a3 * (x0 - x2))),(x1 - x2))| by A25, RVSUM_1:def_17 .= |((a1 * (x1 - x2)),(x1 - x2))| + |((a3 * (x0 - x2)),(x1 - x2))| by EUCLID_4:20 .= (a1 * |((x1 - x2),(x1 - x2))|) + |((a3 * (x0 - x2)),(x1 - x2))| by EUCLID_4:21 .= (a1 * |((x1 - x2),(x1 - x2))|) + (a3 * |((x0 - x2),(x1 - x2))|) by EUCLID_4:21 .= (a1 * |((x1 - x2),(x1 - x2))|) + (a3 * (|((x0 - x1),(x1 - x2))| + |((x1 - x2),(x1 - x2))|)) by A27, EUCLID_4:20 .= (a1 + a3) * |((x1 - x2),(x1 - x2))| by A26 ; then a1 + a3 = 0 by A13, XCMPLX_1:6; then a3 = - a1 ; then A28: x - x2 = a1 * ((x1 + (- x2)) - (x0 - x2)) by A25, Th12 .= a1 * ((x1 - x0) + ((- x2) - (- x2))) by Th18 .= a1 * ((x1 - x0) + (0* n)) by Th2 .= a1 * (x1 - x0) by EUCLID_4:1 ; A29: x1 - x0 <> 0* n by A17, Th9; x - x2 <> 0* n by A14, Th9; then x - x2 // x1 - x0 by A28, A29, Def1; hence L1 // L2 by A19, A16, Def7; ::_thesis: verum end; end; end; hence L1 // L2 ; ::_thesis: verum end; theorem Th112: :: EUCLIDLP:112 for n being Element of NAT for L0, L1, L2, L being Element of line_of_REAL n for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds L meets L2 proof let n be Element of NAT ; ::_thesis: for L0, L1, L2, L being Element of line_of_REAL n for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds L meets L2 let L0, L1, L2, L be Element of line_of_REAL n; ::_thesis: for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds L meets L2 let P be Element of plane_of_REAL n; ::_thesis: ( L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 implies L meets L2 ) assume that A1: ( L0 c= P & L1 c= P ) and A2: L2 c= P and A3: L0 // L1 and A4: L1 // L2 and A5: L0 <> L1 ; ::_thesis: ( not L meets L0 or not L meets L1 or L meets L2 ) A6: L1 is being_line by A3, Th66; assume that A7: L meets L0 and A8: L meets L1 ; ::_thesis: L meets L2 consider x0 being Element of REAL n such that A9: x0 in L and A10: x0 in L0 by A7, Th49; A11: L0 misses L1 by A3, A5, Th71; then not x0 in L1 by A10, Th49; then consider L9 being Element of line_of_REAL n such that A12: x0 in L9 and A13: L9 _|_ L1 and A14: L9 meets L1 by A6, Th62; consider y1 being Element of REAL n such that A15: y1 in L9 and A16: y1 in L1 by A14, Th49; A17: x0 <> y1 by A10, A11, A16, Th49; then A18: L9 = Line (x0,y1) by A12, A15, Th64; then L9 c= P by A1, A10, A16, Th95; then L9,L2 are_coplane by A2, Th96; then A19: L9 meets L2 by A4, A13, Th61, Th109; then consider y2 being Element of REAL n such that A20: y2 in L9 and A21: y2 in L2 by Th49; consider a being Real such that A22: y2 - x0 = a * (y1 - x0) by A12, A15, A17, A20, Th70; L2 is being_line by A4, Th66; then consider x2 being Element of REAL n such that A23: ( x2 <> y2 & x2 in L2 ) by Th53; consider x1 being Element of REAL n such that A24: x1 in L and A25: x1 in L1 by A8, Th49; x0 <> x1 by A10, A25, A11, Th49; then A26: L = Line (x0,x1) by A9, A24, Th64; A27: L2 = Line (y2,x2) by A21, A23, Th64; now__::_thesis:_(_(_x1_=_y1_&_L_meets_L2_)_or_(_x1_<>_y1_&_L_meets_L2_)_) percases ( x1 = y1 or x1 <> y1 ) ; case x1 = y1 ; ::_thesis: L meets L2 hence L meets L2 by A9, A24, A17, A18, A19, Th64; ::_thesis: verum end; caseA28: x1 <> y1 ; ::_thesis: L meets L2 set x = ((1 - a) * x0) + (a * x1); consider b being Real such that A29: b <> 0 and A30: x2 - y2 = b * (x1 - y1) by A4, A25, A16, A21, A23, A28, Th32, Th77; A31: x1 - y1 = 1 * (x1 - y1) by EUCLID_4:3 .= ((1 / b) * b) * (x1 - y1) by A29, XCMPLX_1:87 .= (1 / b) * (x2 - y2) by A30, EUCLID_4:4 ; ((1 - a) * x0) + (a * x1) = ((1 * x0) + (- (a * x0))) + (a * x1) by Th11 .= (x0 + (- (a * x0))) + (a * x1) by EUCLID_4:3 .= ((a * x1) + (- (a * x0))) + x0 by RVSUM_1:15 .= (a * (x1 - x0)) + x0 by Th12 .= (a * ((x1 + (0* n)) + (- x0))) + x0 by EUCLID_4:1 .= (a * ((x1 + ((- y1) + y1)) + (- x0))) + x0 by Th2 .= (a * (((x1 + (- y1)) + y1) + (- x0))) + x0 by RVSUM_1:15 .= (a * ((x1 - y1) + (y1 + (- x0)))) + x0 by RVSUM_1:15 .= ((a * ((1 / b) * (x2 - y2))) + (a * (y1 - x0))) + x0 by A31, EUCLID_4:6 .= (((a * (1 / b)) * (x2 - y2)) + (a * (y1 - x0))) + x0 by EUCLID_4:4 .= (((a / b) * (x2 - y2)) + (a * (y1 - x0))) + x0 by XCMPLX_1:99 .= ((a / b) * (x2 - y2)) + ((y2 + (- x0)) + x0) by A22, RVSUM_1:15 .= ((a / b) * (x2 - y2)) + (y2 + ((- x0) + x0)) by RVSUM_1:15 .= ((a / b) * (x2 - y2)) + (y2 + (0* n)) by Th2 .= ((a / b) * (x2 - y2)) + y2 by EUCLID_4:1 .= (((a / b) * x2) + (- ((a / b) * y2))) + y2 by Th12 .= (y2 + (- ((a / b) * y2))) + ((a / b) * x2) by RVSUM_1:15 .= ((1 * y2) + (- ((a / b) * y2))) + ((a / b) * x2) by EUCLID_4:3 .= ((1 - (a / b)) * y2) + ((a / b) * x2) by Th11 ; then A32: ((1 - a) * x0) + (a * x1) in L2 by A27; ((1 - a) * x0) + (a * x1) in L by A26; hence L meets L2 by A32, Th49; ::_thesis: verum end; end; end; hence L meets L2 ; ::_thesis: verum end; theorem Th113: :: EUCLIDLP:113 for n being Element of NAT for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 holds L1 // L2 proof let n be Element of NAT ; ::_thesis: for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 holds L1 // L2 let L1, L2 be Element of line_of_REAL n; ::_thesis: ( L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 implies L1 // L2 ) assume that A1: L1,L2 are_coplane and A2: L1 is being_line and A3: L2 is being_line ; ::_thesis: ( not L1 misses L2 or L1 // L2 ) assume A4: L1 misses L2 ; ::_thesis: L1 // L2 then consider x being Element of REAL n such that A5: x in L1 and A6: not x in L2 by Th63; consider P being Element of plane_of_REAL n such that A7: L1 c= P and A8: L2 c= P by A1, Th96; consider L9 being Element of line_of_REAL n such that A9: x in L9 and A10: L9 _|_ L2 and A11: L9 meets L2 by A3, A6, Th62; consider x2 being Element of REAL n such that A12: x2 in L9 and A13: x2 in L2 by A11, Th49; consider L0 being Element of line_of_REAL n such that A14: x in L0 and A15: L0 _|_ L9 and A16: L0 // L2 by A10, Th80; L9 = Line (x2,x) by A6, A9, A12, A13, Th64; then A17: L9 c= P by A5, A7, A8, A13, Th95; then A18: L0 c= P by A8, A9, A10, A14, A16, Th110; A19: L9 is being_line by A15, Th67; consider x1 being Element of REAL n such that A20: x1 <> x and A21: x1 in L1 by A2, Th53; A22: L1 = Line (x,x1) by A5, A20, A21, Th64; A23: L0 meets L1 by A5, A14, Th49; L1 = L0 proof A24: not x1 in L9 by A4, A9, A11, A20, A22, Th64; then consider L being Element of line_of_REAL n such that A25: x1 in L and A26: L9 _|_ L and A27: L9 meets L by A19, Th62; A28: L meets L1 by A21, A25, Th49; assume L1 <> L0 ; ::_thesis: contradiction then A29: L <> L0 by A14, A20, A22, A25, Th64; consider x9 being Element of REAL n such that A30: x9 in L9 and A31: x9 in L by A27, Th49; L = Line (x9,x1) by A24, A25, A30, A31, Th64; then A32: L c= P by A7, A17, A21, A30, Th95; then L // L0 by A17, A15, A18, A26, Th111; hence contradiction by A4, A8, A16, A18, A23, A32, A29, A28, Th112; ::_thesis: verum end; hence L1 // L2 by A16; ::_thesis: verum end; theorem :: EUCLIDLP:114 for n being Element of NAT for x1, x2, y1, y2 being Element of REAL n for P being Element of plane_of_REAL n st x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 holds Line (x1,x2) meets Line (y1,y2) proof let n be Element of NAT ; ::_thesis: for x1, x2, y1, y2 being Element of REAL n for P being Element of plane_of_REAL n st x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 holds Line (x1,x2) meets Line (y1,y2) let x1, x2, y1, y2 be Element of REAL n; ::_thesis: for P being Element of plane_of_REAL n st x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 holds Line (x1,x2) meets Line (y1,y2) let P be Element of plane_of_REAL n; ::_thesis: ( x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 implies Line (x1,x2) meets Line (y1,y2) ) reconsider L1 = Line (x1,x2), L2 = Line (y1,y2) as Element of line_of_REAL n by Th47; assume that A1: ( x1 in P & x2 in P & y1 in P & y2 in P ) and A2: x2 - x1,y2 - y1 are_lindependent2 ; ::_thesis: Line (x1,x2) meets Line (y1,y2) A3: ( x1 in L1 & x2 in L1 ) by EUCLID_4:9; ( L1 c= P & L2 c= P ) by A1, Th95; then A4: L1,L2 are_coplane by Th96; A5: ( y1 in L2 & y2 in L2 ) by EUCLID_4:9; y2 - y1 <> 0* n by A2, Lm2; then A6: y2 <> y1 by Th9; then A7: L2 is being_line by EUCLID_4:def_2; x2 - x1 <> 0* n by A2, Lm2; then A8: x2 <> x1 by Th9; then A9: L1 is being_line by EUCLID_4:def_2; L1 meets L2 proof assume L1 misses L2 ; ::_thesis: contradiction then L1 // L2 by A4, A9, A7, Th113; hence contradiction by A2, A8, A6, A3, A5, Lm3, Th77; ::_thesis: verum end; hence Line (x1,x2) meets Line (y1,y2) ; ::_thesis: verum end;