:: by Akihiro Kubo

::

:: Received May 24, 2005

:: Copyright (c) 2005-2021 Association of Mizar Users

:: Preliminaries

theorem Th1: :: EUCLIDLP:1

for s, t, u being Real

for n being Nat

for x being Element of REAL n holds

( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x )

for n being 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 end;

theorem Th3: :: EUCLIDLP:3

for a being Real

for n being Nat

for x being Element of REAL n holds

( - (a * x) = (- a) * x & - (a * x) = a * (- x) )

for n being Nat

for x being Element of REAL n holds

( - (a * x) = (- a) * x & - (a * x) = a * (- x) )

proof end;

theorem Th7: :: EUCLIDLP:7

for n being Nat

for x, x1, x2, x3 being Element of REAL n holds

( x = (x1 + x2) + x3 iff x - x1 = x2 + x3 )

for x, x1, x2, x3 being Element of REAL n holds

( x = (x1 + x2) + x3 iff x - x1 = x2 + x3 )

proof end;

theorem Th8: :: EUCLIDLP:8

for n being Nat

for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3)

for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3)

proof end;

Lm1: for n being Nat

for x1, x2 being Element of REAL n st x1 <> x2 holds

|.(x1 - x2).| <> 0

proof end;

theorem Th10: :: EUCLIDLP:10

for t being Real

for n being Nat

for x0, x, x1 being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds

t <> 0

for n being Nat

for x0, x, x1 being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds

t <> 0

proof end;

theorem Th11: :: EUCLIDLP:11

for a, b being Real

for n being 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) )

for n being 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 end;

theorem Th12: :: EUCLIDLP:12

for a being Real

for n being 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) )

for n being 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 end;

theorem Th13: :: EUCLIDLP:13

for s, t, u being Real

for n being Nat

for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x)

for n being Nat

for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x)

proof end;

theorem Th14: :: EUCLIDLP:14

for a1, a2, a3 being Real

for n being 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))

for n being 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 end;

theorem :: EUCLIDLP:15

for s, t, u being Real

for n being Nat

for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y)

for n being Nat

for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y)

proof end;

theorem Th16: :: EUCLIDLP:16

for n being Nat

for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2)

for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2)

proof end;

theorem Th17: :: EUCLIDLP:17

for n being 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)

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

theorem Th18: :: EUCLIDLP:18

for n being Nat

for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) - (y1 + y2) = (x1 - y1) + (x2 - y2)

for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) - (y1 + y2) = (x1 - y1) + (x2 - y2)

proof end;

theorem :: EUCLIDLP:19

for n being 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)

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

theorem Th20: :: EUCLIDLP:20

for a being Real

for n being Nat

for x1, x2, x3 being Element of REAL n holds a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3)

for n being Nat

for x1, x2, x3 being Element of REAL n holds a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3)

proof end;

theorem Th21: :: EUCLIDLP:21

for a, b1, b2 being Real

for n being Nat

for x1, x2 being Element of REAL n holds a * ((b1 * x1) + (b2 * x2)) = ((a * b1) * x1) + ((a * b2) * x2)

for n being Nat

for x1, x2 being Element of REAL n holds a * ((b1 * x1) + (b2 * x2)) = ((a * b1) * x1) + ((a * b2) * x2)

proof end;

theorem Th22: :: EUCLIDLP:22

for a, b1, b2, b3 being Real

for n being 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)

for n being 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 end;

theorem Th23: :: EUCLIDLP:23

for a1, a2, b1, b2 being Real

for n being Nat

for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2)) = ((a1 + b1) * x1) + ((a2 + b2) * x2)

for n being 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 end;

theorem Th24: :: EUCLIDLP:24

for a1, a2, a3, b1, b2, b3 being Real

for n being 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)

for n being 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 end;

theorem Th25: :: EUCLIDLP:25

for a1, a2, b1, b2 being Real

for n being Nat

for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2)

for n being 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 end;

theorem Th26: :: EUCLIDLP:26

for a1, a2, a3, b1, b2, b3 being Real

for n being 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)

for n being 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 end;

theorem Th27: :: EUCLIDLP:27

for a1, a2, a3 being Real

for n being 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))

for n being 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 end;

theorem Th28: :: EUCLIDLP:28

for a2, a3 being Real

for n being 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 )

for n being 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 end;

:: Lines

theorem Th30: :: EUCLIDLP:30

for n being 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)

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

theorem Th31: :: EUCLIDLP:31

for n being 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)

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

:: deftheorem Def1 defines // EUCLIDLP:def 1 :

for n being 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 ) );

for n being 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 Nat

for x1, x2 being Element of REAL n st x1 // x2 holds

ex a being Real st

( a <> 0 & x1 = a * x2 )

for x1, x2 being Element of REAL n st x1 // x2 holds

ex a being Real st

( a <> 0 & x1 = a * x2 )

proof end;

definition

let n be Nat;

let x1, x2 be Element of REAL n;

:: original: //

redefine pred x1 // x2;

symmetry

for x1, x2 being Element of REAL n st (n,b_{1},b_{2}) holds

(n,b_{2},b_{1})

end;
let x1, x2 be Element of REAL n;

:: original: //

redefine pred x1 // x2;

symmetry

for x1, x2 being Element of REAL n st (n,b

(n,b

proof end;

definition

let n be Nat;

let x1, x2 be Element of REAL n;

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;
let x1, x2 be Element of REAL n;

pred x1,x2 are_lindependent2 means :: EUCLIDLP:def 2

for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds

( a1 = 0 & a2 = 0 );

symmetry for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds

( a1 = 0 & a2 = 0 );

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

:: deftheorem defines are_lindependent2 EUCLIDLP:def 2 :

for n being 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 ) );

for n being 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 Nat;

let x1, x2 be Element of REAL n;

antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2 ;

end;
let x1, x2 be Element of REAL n;

antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2 ;

Lm2: for n being Nat

for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds

x1 <> 0* n

proof end;

theorem :: EUCLIDLP:34

theorem Th35: :: EUCLIDLP:35

for a1, a2, b1, b2 being Real

for n being 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 )

for n being 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 end;

theorem Th36: :: EUCLIDLP:36

for a1, a2, b1, b2 being Real

for n being 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) )

for n being 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 end;

theorem :: EUCLIDLP:38

theorem :: EUCLIDLP:39

for t being Real

for n being Nat

for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds

x1 + (t * x2),x2 are_lindependent2

for n being Nat

for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds

x1 + (t * x2),x2 are_lindependent2

proof end;

theorem Th40: :: EUCLIDLP:40

for n being Nat

for x0, x1, x2, x3, 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

for x0, x1, x2, x3, 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 end;

Lm3: for n being Nat

for x1, x2 being Element of REAL n st x1 // x2 holds

x1,x2 are_ldependent2

proof end;

theorem :: EUCLIDLP:41

Lm4: for n being Nat

for x1, x2 being Element of REAL n st x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n holds

x1 // x2

proof end;

theorem :: EUCLIDLP:42

theorem Th43: :: EUCLIDLP:43

for n being 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 )

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

definition

let n be Nat;

let x1, x2 be Element of REAL n;

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;
let x1, x2 be Element of REAL n;

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

:: deftheorem defines _|_ EUCLIDLP:def 3 :

for n being Nat

for x1, x2 being Element of REAL n holds

( x1 _|_ x2 iff ( x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal ) );

for n being Nat

for x1, x2 being Element of REAL n holds

( x1 _|_ x2 iff ( x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal ) );

definition

let n be Nat;

coherence

{ (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } is Subset-Family of (REAL n);

end;
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 { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ;

coherence

{ (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } is Subset-Family of (REAL n);

proof end;

:: deftheorem defines line_of_REAL EUCLIDLP:def 4 :

for n being Nat holds line_of_REAL n = { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ;

for n being Nat holds line_of_REAL n = { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ;

theorem Th48: :: EUCLIDLP:48

for n being 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

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

theorem Th49: :: EUCLIDLP:49

for n being 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 ) )

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

theorem :: EUCLIDLP:50

theorem Th51: :: EUCLIDLP:51

for n being Nat

for L being Element of line_of_REAL n ex x1, x2 being Element of REAL n st L = Line (x1,x2)

for L being Element of line_of_REAL n ex x1, x2 being Element of REAL n st L = Line (x1,x2)

proof end;

theorem Th53: :: EUCLIDLP:53

for n being 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 )

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

theorem Th54: :: EUCLIDLP:54

for n being 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 )

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

theorem Th55: :: EUCLIDLP:55

for n being 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 )

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

definition

let n be Nat;

let x be Element of REAL n;

let L be Element of line_of_REAL n;

coherence

{ |.(x - x0).| where x0 is Element of REAL n : x0 in L } is Subset of REAL;

end;
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 { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ;

coherence

{ |.(x - x0).| where x0 is Element of REAL n : x0 in L } is Subset of REAL;

proof end;

:: deftheorem defines dist_v EUCLIDLP:def 5 :

for n being 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 } ;

for n being 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 Nat;

let x be Element of REAL n;

let L be Element of line_of_REAL n;

correctness

coherence

lower_bound (dist_v (x,L)) is Real;

;

end;
let x be Element of REAL n;

let L be Element of line_of_REAL n;

correctness

coherence

lower_bound (dist_v (x,L)) is Real;

;

:: deftheorem defines dist EUCLIDLP:def 6 :

for n being 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));

for n being 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

theorem Th57: :: EUCLIDLP:57

for n being 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) )

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

theorem :: EUCLIDLP:58

for n being Nat

for x being Element of REAL n

for L being Element of line_of_REAL n holds dist (x,L) >= 0

for x being Element of REAL n

for L being Element of line_of_REAL n holds dist (x,L) >= 0

proof end;

theorem :: EUCLIDLP:59

for n being 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 )

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

definition

let n be Nat;

let L1, L2 be Element of line_of_REAL n;

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;
let L1, L2 be Element of line_of_REAL n;

pred L1 // L2 means :: 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 ex x1, x2, y1, y2 being Element of REAL n st

( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 // y2 - y1 );

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

:: deftheorem defines // EUCLIDLP:def 7 :

for n being 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 ) );

for n being 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 Nat

for L0, L1, L2 being Element of line_of_REAL n st L0 // L1 & L1 // L2 holds

L0 // L2

for L0, L1, L2 being Element of line_of_REAL n st L0 // L1 & L1 // L2 holds

L0 // L2

proof end;

definition

let n be Nat;

let L1, L2 be Element of line_of_REAL n;

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;
let L1, L2 be Element of line_of_REAL n;

pred L1 _|_ L2 means :: 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 ex x1, x2, y1, y2 being Element of REAL n st

( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 );

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

:: deftheorem defines _|_ EUCLIDLP:def 8 :

for n being 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 ) );

for n being 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 Nat

for L0, L1, L2 being Element of line_of_REAL n st L0 _|_ L1 & L1 // L2 holds

L0 _|_ L2

for L0, L1, L2 being Element of line_of_REAL n st L0 _|_ L1 & L1 // L2 holds

L0 _|_ L2

proof end;

theorem Th62: :: EUCLIDLP:62

for n being 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 )

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

theorem Th63: :: EUCLIDLP:63

for n being 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 )

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

theorem Th64: :: EUCLIDLP:64

for n being 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 )

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

theorem Th65: :: EUCLIDLP:65

for n being Nat

for L1, L2 being Element of line_of_REAL n st L1 is being_line & L1 = L2 holds

L1 // L2

for L1, L2 being Element of line_of_REAL n st L1 is being_line & L1 = L2 holds

L1 // L2

proof end;

theorem Th66: :: EUCLIDLP:66

for n being Nat

for L1, L2 being Element of line_of_REAL n st L1 // L2 holds

( L1 is being_line & L2 is being_line )

for L1, L2 being Element of line_of_REAL n st L1 // L2 holds

( L1 is being_line & L2 is being_line )

proof end;

theorem Th67: :: EUCLIDLP:67

for n being Nat

for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds

( L1 is being_line & L2 is being_line )

for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds

( L1 is being_line & L2 is being_line )

proof end;

theorem :: EUCLIDLP:68

for a being Real

for n being 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

for n being 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 end;

theorem :: EUCLIDLP:69

for a being Real

for n being 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) )

for n being 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 end;

theorem Th70: :: EUCLIDLP:70

for n being 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)

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

theorem Th71: :: EUCLIDLP:71

for n being Nat

for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds

L1 misses L2

for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds

L1 misses L2

proof end;

theorem Th72: :: EUCLIDLP:72

for n being 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 )

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

theorem :: EUCLIDLP:73

for n being 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 )

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

theorem Th74: :: EUCLIDLP:74

for n being 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

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

theorem Th76: :: EUCLIDLP:76

for n being 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

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

theorem Th77: :: EUCLIDLP:77

for n being 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

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

theorem :: EUCLIDLP:78

for n being Nat

for x1, x2, 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) ) )

for x1, x2, 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 end;

theorem Th79: :: EUCLIDLP:79

for n being 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 )

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

theorem Th80: :: EUCLIDLP:80

for n being 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 )

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

theorem Th81: :: EUCLIDLP:81

for n being 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 )

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

:: Planes

definition

let n be Nat;

let x1, x2, x3 be Element of REAL n;

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

end;
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 { 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) ) } ;

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

:: deftheorem defines plane EUCLIDLP:def 9 :

for n being 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) ) } ;

for n being 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 Nat;

let x1, x2, x3 be Element of REAL n;

coherence

not plane (x1,x2,x3) is empty

end;
let x1, x2, x3 be Element of REAL n;

coherence

not plane (x1,x2,x3) is empty

proof end;

definition

let n be Nat;

let A be Subset of (REAL n);

end;
let A be Subset of (REAL n);

attr A is being_plane means :: EUCLIDLP:def 10

ex x1, x2, x3 being Element of REAL n st

( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) );

ex x1, x2, x3 being Element of REAL n st

( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) );

:: deftheorem defines being_plane EUCLIDLP:def 10 :

for n being 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) ) );

for n being 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 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) )

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

theorem Th83: :: EUCLIDLP:83

for n being Nat

for x1, x2, x3, y1, y2, y3 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)

for x1, x2, x3, y1, y2, y3 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 end;

theorem :: EUCLIDLP:84

for n being 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)

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

theorem Th85: :: EUCLIDLP:85

for n being Nat

for x1, x2, x3, y1, 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)

for x1, x2, x3, y1, 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 end;

theorem :: EUCLIDLP:86

for n being 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

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

theorem :: EUCLIDLP:87

for a1, a2, a3 being Real

for n being 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)

for n being 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 end;

theorem Th88: :: EUCLIDLP:88

for n being 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) ) )

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

theorem :: EUCLIDLP:89

for a1, a2, a3, b1, b2, b3 being Real

for n being Nat

for x, x1, x2, x3 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 )

for n being Nat

for x, x1, x2, x3 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 end;

definition

let n be Nat;

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

end;
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 { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ;

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

:: deftheorem defines plane_of_REAL EUCLIDLP:def 11 :

for n being 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) } ;

for n being 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) } ;

theorem Th91: :: EUCLIDLP:91

for n being 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

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

theorem Th92: :: EUCLIDLP:92

for n being 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)

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

theorem :: EUCLIDLP:93

for n being Nat

for P1, P2 being Element of plane_of_REAL n st P1 is being_plane & P1 c= P2 holds

P1 = P2

for P1, P2 being Element of plane_of_REAL n st P1 is being_plane & P1 c= P2 holds

P1 = P2

proof end;

:: Lines in the planes

theorem :: EUCLIDLP:94

for n being 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) )

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

theorem Th95: :: EUCLIDLP:95

for n being 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

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

definition

let n be Nat;

let L1, L2 be Element of line_of_REAL n;

end;
let L1, L2 be Element of line_of_REAL n;

pred L1,L2 are_coplane means :: 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) );

ex x1, x2, x3 being Element of REAL n st

( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) );

:: deftheorem defines are_coplane EUCLIDLP:def 12 :

for n being 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) ) );

for n being 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 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 ) )

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

theorem Th98: :: EUCLIDLP:98

for n being 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 )

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

theorem Th99: :: EUCLIDLP:99

for n being 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 )

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

theorem Th100: :: EUCLIDLP:100

for n being 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 )

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

theorem Th101: :: EUCLIDLP:101

for n being 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

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

theorem Th102: :: EUCLIDLP:102

for n being 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

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

theorem :: EUCLIDLP:103

for n being 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 )

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

theorem :: EUCLIDLP:104

for n being 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 )

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

theorem :: EUCLIDLP:105

for n being 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

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

theorem Th106: :: EUCLIDLP:106

for n being 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 )

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

theorem Th107: :: EUCLIDLP:107

for n being 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 )

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

theorem Th108: :: EUCLIDLP:108

for n being 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

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

theorem Th109: :: EUCLIDLP:109

for n being Nat

for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 _|_ L2 holds

L1 meets L2

for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 _|_ L2 holds

L1 meets L2

proof end;

theorem Th110: :: EUCLIDLP:110

for n being 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 L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds

( L0 c= P & L0 _|_ L1 )

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 L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds

( L0 c= P & L0 _|_ L1 )

proof end;

theorem Th111: :: EUCLIDLP:111

for n being 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

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

theorem Th112: :: EUCLIDLP:112

for n being Nat

for L, 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 & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds

L meets L2

for L, 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 & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds

L meets L2

proof end;

theorem Th113: :: EUCLIDLP:113

for n being 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

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

theorem :: EUCLIDLP:114

for n being 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)

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