:: Lines on Planes in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received May 24, 2005
:: Copyright (c) 2005-2011 Association of Mizar Users

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

theorem :: EUCLIDLP:2

canceled;

theorem :: EUCLIDLP:3

canceled;

theorem :: EUCLIDLP:4

canceled;

theorem :: EUCLIDLP:5

canceled;

theorem :: EUCLIDLP:6

canceled;

theorem Th7: :: EUCLIDLP:7

for n being Element of NAT
for x being Element of REAL n holds
( x - x = 0* n & x + (- x) = 0* n )

proof end;

theorem Th8: :: EUCLIDLP:8

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

theorem Th9: :: EUCLIDLP:9

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

proof end;

theorem Th10: :: EUCLIDLP:10

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

proof end;

theorem Th11: :: EUCLIDLP:11

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

proof end;

theorem Th12: :: EUCLIDLP:12

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

theorem Th13: :: EUCLIDLP:13

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

proof end;

Lm1: for n being Element of NAT
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0

proof end;

theorem Th14: :: EUCLIDLP:14

for n being Element of NAT
for x1, x2 being Element of REAL n holds
( x1 = x2 iff x1 - x2 = 0* n )

proof end;

theorem Th15: :: EUCLIDLP:15

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

theorem Th16: :: EUCLIDLP:16

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

theorem Th17: :: EUCLIDLP:17

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

theorem Th18: :: EUCLIDLP:18

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

theorem Th19: :: EUCLIDLP:19

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

theorem :: EUCLIDLP:20

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

theorem Th21: :: EUCLIDLP:21

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

theorem Th22: :: EUCLIDLP:22

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

theorem Th23: :: EUCLIDLP:23

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

theorem :: EUCLIDLP:24

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

theorem Th25: :: EUCLIDLP:25

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

theorem Th26: :: EUCLIDLP:26

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

theorem Th27: :: EUCLIDLP:27

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

theorem Th28: :: EUCLIDLP:28

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

theorem Th29: :: EUCLIDLP:29

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

theorem Th30: :: EUCLIDLP:30

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

theorem Th31: :: EUCLIDLP:31

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

theorem Th32: :: EUCLIDLP:32

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

theorem Th33: :: EUCLIDLP:33

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

theorem :: EUCLIDLP:34

for n being Element of NAT st n >= 1 holds
1* n <> 0* n

proof end;

theorem Th35: :: EUCLIDLP:35

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

theorem Th36: :: EUCLIDLP:36

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

definition

let n be Element of NAT ;
let x1, x2 be Element of REAL n;
pred x1 // 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 Th37: :: EUCLIDLP:37

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

definition

let n be Element of NAT ;
let x1, x2 be Element of REAL n;
:: original: //
redefine pred x1 // x2;
symmetry
for x1, x2 being Element of REAL n st x1 // x2 holds
x2 // x1

proof end;

end;

theorem Th38: :: EUCLIDLP:38

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

proof end;

definition

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

theorem :: EUCLIDLP:39

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 Th40: :: EUCLIDLP:40

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

theorem Th41: :: EUCLIDLP:41

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

theorem Th42: :: EUCLIDLP:42

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

proof end;

theorem :: EUCLIDLP:43

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

theorem :: EUCLIDLP:44

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

theorem Th45: :: EUCLIDLP:45

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

theorem :: EUCLIDLP:46

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

theorem :: EUCLIDLP:47

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 Th48: :: EUCLIDLP:48

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

definition

let n be Element of NAT ;
let x1, x2 be Element of REAL n;
pred x1 _|_ 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 Th49: :: EUCLIDLP:49

for n being Element of NAT
for x, y0, y1 being Element of REAL n st x _|_ y0 & y0 // y1 holds
x _|_ y1

proof end;

theorem Th50: :: EUCLIDLP:50

for n being Element of NAT
for x, y being Element of REAL n st x _|_ y holds
x,y are_lindependent2

proof end;

theorem :: EUCLIDLP:51

for n being Element of NAT
for x1, x2 being Element of REAL n st x1 // x2 holds
not x1 _|_ x2

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

end;

theorem Th52: :: EUCLIDLP:52

for n being Element of NAT
for x1, x2 being Element of REAL n holds Line (x1,x2) in line_of_REAL n ;

theorem Th53: :: EUCLIDLP:53

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

theorem Th54: :: EUCLIDLP:54

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

theorem :: EUCLIDLP:55

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

theorem Th56: :: EUCLIDLP:56

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

theorem Th57: :: EUCLIDLP:57

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

theorem Th58: :: EUCLIDLP:58

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

theorem Th59: :: EUCLIDLP:59

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

theorem Th60: :: EUCLIDLP:60

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

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 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 ex x0 being Element of REAL n st
( x0 in L & |.(x - x0).| = dist (x,L) )

proof end;

theorem :: EUCLIDLP:63

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

theorem :: EUCLIDLP:64

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

definition

let n be Element of NAT ;
let L1, L2 be Element of line_of_REAL n;
pred L1 // 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:65

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

definition

let n be Element of NAT ;
let L1, L2 be Element of line_of_REAL n;
pred L1 _|_ 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 Th66: :: EUCLIDLP:66

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

theorem Th67: :: EUCLIDLP:67

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

theorem Th68: :: EUCLIDLP:68

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

theorem Th69: :: EUCLIDLP:69

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

theorem Th70: :: EUCLIDLP:70

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

theorem Th71: :: EUCLIDLP:71

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

theorem Th72: :: EUCLIDLP:72

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

theorem :: EUCLIDLP:73

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

theorem :: EUCLIDLP:74

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

theorem Th75: :: EUCLIDLP:75

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

theorem Th76: :: EUCLIDLP:76

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

theorem Th77: :: EUCLIDLP:77

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

theorem :: EUCLIDLP:78

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

theorem Th79: :: EUCLIDLP:79

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

theorem Th80: :: EUCLIDLP:80

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

proof end;

theorem Th81: :: EUCLIDLP:81

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

theorem Th82: :: EUCLIDLP:82

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

theorem :: EUCLIDLP:83

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

theorem Th84: :: EUCLIDLP:84

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

theorem Th85: :: EUCLIDLP:85

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

theorem Th86: :: EUCLIDLP:86

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

end;

definition

let n be Element of NAT ;
let A be Subset of (REAL n);
attr A 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 Th87: :: EUCLIDLP:87

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

theorem Th88: :: EUCLIDLP:88

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

theorem :: EUCLIDLP:89

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

theorem Th90: :: EUCLIDLP:90

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

theorem :: EUCLIDLP:91

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

theorem :: EUCLIDLP:92

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

theorem Th93: :: EUCLIDLP:93

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

theorem :: EUCLIDLP:94

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

end;

theorem Th95: :: EUCLIDLP:95

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 Th96: :: EUCLIDLP:96

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

theorem Th97: :: EUCLIDLP:97

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

theorem :: EUCLIDLP:98

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

theorem :: EUCLIDLP:99

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

theorem Th100: :: EUCLIDLP:100

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

definition

let n be Element of NAT ;
let L1, L2 be Element of line_of_REAL n;
pred L1,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 Th101: :: EUCLIDLP:101

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

theorem Th102: :: EUCLIDLP:102

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

theorem Th103: :: 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 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 Th104: :: EUCLIDLP:104

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

theorem Th105: :: EUCLIDLP:105

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

theorem Th106: :: EUCLIDLP:106

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

theorem Th107: :: EUCLIDLP:107

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

theorem :: EUCLIDLP:108

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

theorem :: EUCLIDLP:109

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

theorem :: EUCLIDLP:110

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

theorem Th111: :: EUCLIDLP:111

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

theorem Th112: :: EUCLIDLP:112

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

theorem Th113: :: EUCLIDLP:113

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

theorem Th114: :: EUCLIDLP:114

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

theorem Th115: :: EUCLIDLP:115

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

theorem Th116: :: EUCLIDLP:116

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

theorem Th117: :: EUCLIDLP:117

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

theorem Th118: :: EUCLIDLP:118

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

theorem :: EUCLIDLP:119

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