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


begin

:: Preliminaries
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 )
proofend;

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

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

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

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

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

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

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

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

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

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 &amp; x1 <> x0 holds
t <> 0
proofend;

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) &amp; (a - b) * x = (a * x) + (- (b * x)) &amp; (a - b) * x = (a * x) - (b * x) )
proofend;

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)) &amp; a * (x - y) = (a * x) + ((- a) * y) &amp; a * (x - y) = (a * x) - (a * y) )
proofend;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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) &amp; (a1 + a2) + a3 = 1 )
proofend;

theorem :: EUCLIDLP:29
for n being Element of NAT st n >= 1 holds
1* n <> 0* n
proofend;

:: Lines
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 &amp; x1 in A &amp; x2 in A &amp; x1 <> x2 holds
A = Line (x1,x2)
proofend;

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) &amp; y2 in Line (x1,x2) holds
ex a being Real st y2 - y1 = a * (x2 - x1)
proofend;

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 &amp; x2 <> 0* n &amp; 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 &amp; x2 <> 0* n &amp; 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 &amp; x1 = a * x2 )
proofend;

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

theorem Th33: :: EUCLIDLP:33
for n being Element of NAT
for x1, x2, x3 being Element of REAL n st x1 // x2 &amp; x2 // x3 holds
x1 // x3
proofend;

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 &amp; 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 &amp; a2 = 0 ) ) holds
for a1, a2 being Real st (a1 * x2) + (a2 * x1) = 0* n holds
( a1 = 0 &amp; 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 &amp; 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
proofend;

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 &amp; 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 &amp; (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) holds
( a1 = b1 &amp; a2 = b2 )
proofend;

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 &amp; y1 = (a1 * x1) + (a2 * x2) &amp; y2 = (b1 * x1) + (b2 * x2) holds
ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) &amp; x2 = (d1 * y1) + (d2 * y2) )
proofend;

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

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

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 &amp; y0 in Line (x0,x1) &amp; y1 in Line (x0,x1) &amp; y0 <> y1 &amp; y2 in Line (x2,x3) &amp; y3 in Line (x2,x3) &amp; y2 <> y3 holds
y1 - y0,y3 - y2 are_lindependent2
proofend;

Lm3:  for n being Element of NAT
for x1, x2 being Element of REAL n st x1 // x2 holds
x1,x2 are_ldependent2
proofend;

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 &amp; x1 <> 0* n &amp; 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 &amp; x1 <> 0* n &amp; x2 <> 0* n holds
x1 // x2
proofend;

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) &amp; x1 - x2,y1 - y2 are_orthogonal )
proofend;

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 &amp; x2 <> 0* n &amp; x1,x2 are_orthogonal );
symmetry
 for x1, x2 being Element of REAL n st x1 <> 0* n &amp; x2 <> 0* n &amp; x1,x2 are_orthogonal holds
( x2 <> 0* n &amp; x1 <> 0* n &amp; 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 &amp; x2 <> 0* n &amp; 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 &amp; y0 // y1 holds
x _|_ y1
proofend;

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

theorem :: EUCLIDLP:46
for n being Element of NAT
for x1, x2 being Element of REAL n st x1 // x2 holds
not x1 _|_ x2
proofend;

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);
proofend;
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
proofend;
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 &amp; x2 in L holds
Line (x1,x2) c= L
proofend;

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 &amp; x in L2 ) )
proofend;

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 &amp; 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)
proofend;

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

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 &amp; x1 in L )
proofend;

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 &amp; L is being_line holds
ex x1, x2 being Element of REAL n st
( L = Line (x1,x2) &amp; x - x1 _|_ x2 - x1 )
proofend;

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 &amp; L is being_line holds
ex x1, x2 being Element of REAL n st
( L = Line (x1,x2) &amp; x - x1,x2 - x1 are_lindependent2 )
proofend;

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;
proofend;
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 &amp; |.(x - x0).| = dist (x,L) )
proofend;

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

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

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) &amp; L2 = Line (y1,y2) &amp; 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) &amp; L2 = Line (y1,y2) &amp; x2 - x1 // y2 - y1 ) holds
ex x1, x2, y1, y2 being Element of REAL n st
( L2 = Line (x1,x2) &amp; L1 = Line (y1,y2) &amp; 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) &amp; L2 = Line (y1,y2) &amp; 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 &amp; L1 // L2 holds
L0 // L2
proofend;

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) &amp; L2 = Line (y1,y2) &amp; 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) &amp; L2 = Line (y1,y2) &amp; x2 - x1 _|_ y2 - y1 ) holds
ex x1, x2, y1, y2 being Element of REAL n st
( L2 = Line (x1,x2) &amp; L1 = Line (y1,y2) &amp; 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) &amp; L2 = Line (y1,y2) &amp; 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 &amp; L1 // L2 holds
L0 _|_ L2
proofend;

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 &amp; L is being_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 &amp; L0 _|_ L &amp; L0 meets L )
proofend;

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 &amp; not x in L2 )
proofend;

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 &amp; x2 in L &amp; x1 <> x2 holds
( Line (x1,x2) = L &amp; L is being_line )
proofend;

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 &amp; L1 = L2 holds
L1 // L2
proofend;

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 &amp; L2 is being_line )
proofend;

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 &amp; L2 is being_line )
proofend;

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 &amp; a <> 1 &amp; a * x in L holds
0* n in L
proofend;

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 &amp; x2 in L holds
ex x3 being Element of REAL n st
( x3 in L &amp; x3 - x1 = a * (x2 - x1) )
proofend;

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 &amp; x2 in L &amp; x3 in L &amp; x1 <> x2 holds
ex a being Real st x3 - x1 = a * (x2 - x1)
proofend;

theorem Th71: :: EUCLIDLP:71
for n being Element of NAT
for L1, L2 being Element of line_of_REAL n st L1 // L2 &amp; L1 <> L2 holds
L1 misses L2
proofend;

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 &amp; L0 // L )
proofend;

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 &amp; L is being_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 &amp; L0 // L &amp; L0 <> L )
proofend;

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 &amp; x1 in L1 &amp; x0 <> x1 &amp; y0 in L2 &amp; y1 in L2 &amp; y0 <> y1 &amp; L1 _|_ L2 holds
x1 - x0 _|_ y1 - y0
proofend;

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

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 &amp; L = Line (x1,x2) holds
x1 <> x2
proofend;

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 &amp; x1 in L1 &amp; x0 <> x1 &amp; y0 in L2 &amp; y1 in L2 &amp; y0 <> y1 &amp; L1 // L2 holds
x1 - x0 // y1 - y0
proofend;

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 &amp; y2 in Line (x1,x2) &amp; y3 in Line (x1,x3) &amp; L1 = Line (x2,x3) &amp; L2 = Line (y2,y3) holds
( L1 // L2 iff ex a being Real st
( a <> 0 &amp; y2 - x1 = a * (x2 - x1) &amp; y3 - x1 = a * (x3 - x1) ) )
proofend;

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 &amp; L2 is being_line &amp; L1 <> L2 holds
ex x being Element of REAL n st
( x in L1 &amp; not x in L2 )
proofend;

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 &amp; L0 _|_ L2 &amp; L0 // L1 )
proofend;

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 &amp; L1 _|_ L2 holds
ex x0 being Element of REAL n st
( x <> x0 &amp; x0 in L1 &amp; not x0 in L2 )
proofend;

:: Planes
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 &amp; 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 &amp; x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) )  }  is Subset of (REAL n);
proofend;
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 &amp; 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
proofend;
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 &amp; 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 &amp; 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) &amp; x2 in plane (x1,x2,x3) &amp; x3 in plane (x1,x2,x3) )
proofend;

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) &amp; x2 in plane (y1,y2,y3) &amp; x3 in plane (y1,y2,y3) holds
plane (x1,x2,x3) c= plane (y1,y2,y3)
proofend;

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) &amp; ex c1, c2, c3 being Real st
( (c1 + c2) + c3 = 0 &amp; x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) holds
0* n in plane (x1,x2,x3)
proofend;

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) &amp; y2 in plane (x1,x2,x3) holds
Line (y1,y2) c= plane (x1,x2,x3)
proofend;

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 &amp; x in A &amp; ex a being Real st
( a <> 1 &amp; a * x in A ) holds
0* n in A
proofend;

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) &amp; x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) &amp; not (a1 + a2) + a3 = 1 holds
0* n in plane (x1,x2,x3)
proofend;

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 &amp; x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) )
proofend;

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 &amp; (a1 + a2) + a3 = 1 &amp; x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) &amp; (b1 + b2) + b3 = 1 &amp; x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds
( a1 = b1 &amp; a2 = b2 &amp; a3 = b3 )
proofend;

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);
proofend;
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
proofend;
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 &amp; x2 in P &amp; x3 in P holds
plane (x1,x2,x3) c= P
proofend;

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 &amp; x2 in P &amp; x3 in P &amp; x2 - x1,x3 - x1 are_lindependent2 holds
P = plane (x1,x2,x3)
proofend;

theorem :: EUCLIDLP:93
for n being Element of NAT
for P1, P2 being Element of plane_of_REAL n st P1 is being_plane &amp; P1 c= P2 holds
P1 = P2
proofend;

:: Lines in the planes
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) &amp; Line (x2,x3) c= plane (x1,x2,x3) &amp; Line (x3,x1) c= plane (x1,x2,x3) )
proofend;

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 &amp; x2 in P holds
Line (x1,x2) c= P
proofend;

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) &amp; 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) &amp; 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 &amp; L2 c= P ) )
proofend;

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

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 &amp; L2 is being_line &amp; L1,L2 are_coplane &amp; L1 misses L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P &amp; L2 c= P &amp; P is being_plane )
proofend;

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 &amp; L c= P )
proofend;

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 &amp; L is being_line holds
ex P being Element of plane_of_REAL n st
( x in P &amp; L c= P &amp; P is being_plane )
proofend;

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 &amp; L c= P &amp; not x in L &amp; L is being_line holds
P is being_plane
proofend;

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 &amp; L is being_line &amp; x in P0 &amp; L c= P0 &amp; x in P1 &amp; L c= P1 holds
P0 = P1
proofend;

theorem :: EUCLIDLP:103
for n being Element of NAT
for L1, L2 being Element of line_of_REAL n st L1 is being_line &amp; L2 is being_line &amp; L1,L2 are_coplane &amp; L1 <> L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P &amp; L2 c= P &amp; P is being_plane )
proofend;

theorem :: EUCLIDLP:104
for n being Element of NAT
for L1, L2 being Element of line_of_REAL n st L1 is being_line &amp; L2 is being_line &amp; L1 <> L2 &amp; L1 meets L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P &amp; L2 c= P &amp; P is being_plane )
proofend;

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 &amp; L2 is being_line &amp; L1 <> L2 &amp; L1 c= P1 &amp; L2 c= P1 &amp; L1 c= P2 &amp; L2 c= P2 holds
P1 = P2
proofend;

theorem Th106: :: EUCLIDLP:106
for n being Element of NAT
for L1, L2 being Element of line_of_REAL n st L1 // L2 &amp; L1 <> L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P &amp; L2 c= P &amp; P is being_plane )
proofend;

theorem Th107: :: EUCLIDLP:107
for n being Element of NAT
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 &amp; L1 meets L2 holds
ex P being Element of plane_of_REAL n st
( P is being_plane &amp; L1 c= P &amp; L2 c= P )
proofend;

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

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 &amp; L1 _|_ L2 holds
L1 meets L2
proofend;

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

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 &amp; L1 c= P &amp; L2 c= P &amp; L _|_ L1 &amp; L _|_ L2 holds
L1 // L2
proofend;

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 &amp; L1 c= P &amp; L2 c= P &amp; L0 // L1 &amp; L1 // L2 &amp; L0 <> L1 &amp; L meets L0 &amp; L meets L1 holds
L meets L2
proofend;

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 &amp; L1 is being_line &amp; L2 is being_line &amp; L1 misses L2 holds
L1 // L2
proofend;

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 &amp; x2 in P &amp; y1 in P &amp; y2 in P &amp; x2 - x1,y2 - y1 are_lindependent2 holds
Line (x1,x2) meets Line (y1,y2)
proofend;