:: 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;