:: EUCLIDLP semantic presentation

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 )

proof end;

theorem Th2: :: EUCLIDLP:2

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

proof end;

theorem Th3: :: EUCLIDLP:3

for n being Nat
for x being Element of REAL n holds x - (0* n) = x

proof end;

theorem Th4: :: EUCLIDLP:4

for n being Nat
for x being Element of REAL n holds (0* n) - x = - x

proof end;

theorem Th5: :: EUCLIDLP:5

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

proof end;

theorem Th6: :: EUCLIDLP:6

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

proof end;

theorem Th7: :: EUCLIDLP:7

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

proof end;

Lm1: for n being Nat
for x being Element of REAL n holds (- 1) * x = - x

proof end;

theorem Th8: :: EUCLIDLP:8

for a being Real
for n being 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 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 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 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 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 Nat
for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3)

proof end;

Lm2: for n being 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Nat st n >= 1 holds
1* n <> 0* n

proof end;

theorem Th35: :: EUCLIDLP:35

for n being Nat
for A being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line x1,x2

proof end;

theorem Th36: :: EUCLIDLP:36

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)

proof end;

definition

let n be 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 :

theorem Th37: :: EUCLIDLP:37

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 )

proof end;

definition

let n be Nat;
let x1, x2 be Element of REAL n;
:: original: //
redefine pred x1 // x2;
symmetry

proof end;

end;

theorem Th38: :: EUCLIDLP:38

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

proof end;

definition

let n be 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 ;

end;

:: deftheorem Def2 defines are_lindependent2 EUCLIDLP:def 2 :

notation

let n be Nat;
let x1, x2 be Element of REAL n;
antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2 ;

end;

Lm3: 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:39

for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
( x1 <> 0* n & x2 <> 0* n ) by Lm3;

theorem Th40: :: EUCLIDLP:40

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 )

proof end;

theorem Th41: :: EUCLIDLP:41

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

proof end;

theorem Th42: :: EUCLIDLP:42

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

Lm4: for n being 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 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, Lm4;

Lm5: 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:47

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

theorem Th48: :: EUCLIDLP:48

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 )

proof end;

definition

let n be 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 ;

end;

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

theorem Th49: :: EUCLIDLP:49

for n being 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 Nat
for x, y being Element of REAL n st x _|_ y holds
x,y are_lindependent2

proof end;

theorem Th51: :: EUCLIDLP:51

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

proof end;

theorem :: EUCLIDLP:52

for n being Nat
for x1, x2 being Element of REAL n st x1 _|_ x2 holds
not x1 // x2 by Th51;

definition

let n be Nat;
func line_of_REAL n -> Subset-Family of (REAL n) equals :: EUCLIDLP:def 4
{ L where L is Subset of (REAL n) : ex x1, x2 being Element of REAL n st L = Line x1,x2 } ;
correctness

proof end;

end;

:: deftheorem defines line_of_REAL EUCLIDLP:def 4 :

registration

let n be Nat;
cluster line_of_REAL n -> non empty ;
coherence

proof end;

end;

theorem Th53: :: EUCLIDLP:53

for n being Nat
for x1, x2 being Element of REAL n holds Line x1,x2 in line_of_REAL n ;

theorem Th54: :: EUCLIDLP:54

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

proof end;

theorem Th55: :: EUCLIDLP:55

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

proof end;

theorem :: EUCLIDLP:56

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

theorem Th57: :: EUCLIDLP:57

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

proof end;

theorem Th58: :: EUCLIDLP:58

for n being Nat
for L being Element of line_of_REAL n ex x being Element of REAL n st x in L

proof end;

theorem Th59: :: EUCLIDLP:59

for n being Nat
for x0 being Element of REAL n
for L being Element of line_of_REAL n st x0 in L & L is_line holds
ex x1 being Element of REAL n st
( x1 <> x0 & x1 in L )

proof end;

theorem Th60: :: EUCLIDLP:60

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

proof end;

theorem Th61: :: EUCLIDLP:61

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

proof end;

end;

:: deftheorem defines dist_v EUCLIDLP:def 5 :

definition

let n be 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 ;

end;

:: deftheorem defines dist EUCLIDLP:def 6 :

theorem :: EUCLIDLP:62

for n being 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 Th63: :: EUCLIDLP:63

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 )

proof end;

theorem :: EUCLIDLP:64

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

proof end;

theorem :: EUCLIDLP:65

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 )

proof end;

definition

let n be 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 ;

end;

:: deftheorem Def7 defines // EUCLIDLP:def 7 :

theorem Th66: :: EUCLIDLP:66

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

end;

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

theorem Th67: :: EUCLIDLP:67

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

proof end;

theorem Th68: :: EUCLIDLP:68

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

proof end;

theorem Th69: :: EUCLIDLP:69

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 )

proof end;

theorem Th70: :: EUCLIDLP:70

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

proof end;

theorem Th71: :: EUCLIDLP:71

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is_line & L2 is_line & L1 = L2 holds
L1 // L2

proof end;

theorem Th72: :: EUCLIDLP:72

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 // L2 holds
( L1 is_line & L2 is_line )

proof end;

theorem Th73: :: EUCLIDLP:73

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds
( L1 is_line & L2 is_line )

proof end;

theorem :: EUCLIDLP:74

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

proof end;

theorem :: EUCLIDLP:75

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

proof end;

theorem Th76: :: EUCLIDLP:76

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)

proof end;

theorem Th77: :: EUCLIDLP:77

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

proof end;

theorem :: EUCLIDLP:78

for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( not L1 // L2 or L1 = L2 or L1 misses L2 ) by Th77;

theorem :: EUCLIDLP:79

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 meets L2 holds
L1 = L2 by Th77;

theorem Th80: :: EUCLIDLP:80

for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st L is_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L )

proof end;

theorem :: EUCLIDLP:81

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

proof end;

theorem Th82: :: EUCLIDLP:82

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

proof end;

theorem Th83: :: EUCLIDLP:83

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

proof end;

theorem Th84: :: EUCLIDLP:84

for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st L is_line & L = Line x1,x2 holds
x1 <> x2

proof end;

theorem Th85: :: EUCLIDLP:85

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

proof end;

theorem :: EUCLIDLP:86

for n being 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 Th87: :: EUCLIDLP:87

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is_line & L2 is_line & L1 <> L2 holds
ex x being Element of REAL n st
( x in L1 & not x in L2 )

proof end;

theorem Th88: :: EUCLIDLP:88

for n being Nat
for x being Element of REAL n
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & x in L2 holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L2 & L0 // L1 )

proof end;

theorem Th89: :: EUCLIDLP:89

for n being Nat
for x being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x in L1 & 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 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

proof end;

end;

:: deftheorem defines plane EUCLIDLP:def 9 :

registration

let n be Nat;
let x1, x2, x3 be Element of REAL n;
cluster plane x1,x2,x3 -> non empty ;
coherence

proof end;

end;

definition

let n be 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 :

theorem Th90: :: EUCLIDLP:90

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 )

proof end;

theorem Th91: :: EUCLIDLP:91

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

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

proof end;

theorem Th93: :: EUCLIDLP:93

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

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

proof end;

theorem :: EUCLIDLP:95

for a1, a2, a3 being Real
for n being Nat
for x1, x3, x, x2 being Element of REAL n st x1 - x1,x3 - x1 are_lindependent2 & 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 Th96: :: EUCLIDLP:96

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

proof end;

theorem :: EUCLIDLP:97

for a1, a2, a3, b1, b2, b3 being Real
for n being Nat
for x2, x1, x3, x being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & (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;
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

proof end;

end;

:: deftheorem defines plane_of_REAL EUCLIDLP:def 11 :

registration

let n be Nat;
cluster plane_of_REAL n -> non empty ;
coherence

proof end;

end;

theorem Th98: :: EUCLIDLP:98

for n being Nat
for x1, x2, x3 being Element of REAL n holds plane x1,x2,x3 in plane_of_REAL n ;

theorem Th99: :: EUCLIDLP:99

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

proof end;

theorem Th100: :: EUCLIDLP:100

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

proof end;

theorem :: EUCLIDLP:101

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

proof end;

theorem :: EUCLIDLP:102

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 )

proof end;

theorem Th103: :: EUCLIDLP:103

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

proof end;

definition

let n be 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 :

theorem Th104: :: EUCLIDLP:104

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

proof end;

theorem Th105: :: EUCLIDLP:105

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

proof end;

theorem Th106: :: EUCLIDLP:106

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is_line & L2 is_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 Th107: :: EUCLIDLP:107

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 )

proof end;

theorem Th108: :: EUCLIDLP:108

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_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 Th109: :: EUCLIDLP:109

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_line holds
P is being_plane

proof end;

theorem Th110: :: EUCLIDLP:110

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_line & x in P0 & L c= P0 & x in P1 & L c= P1 holds
P0 = P1

proof end;

theorem :: EUCLIDLP:111

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is_line & L2 is_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:112

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is_line & L2 is_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:113

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_line & L2 is_line & L1 <> L2 & L1 meets L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds
P1 = P2

proof end;

theorem Th114: :: EUCLIDLP:114

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 )

proof end;

theorem Th115: :: EUCLIDLP:115

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 )

proof end;

theorem Th116: :: EUCLIDLP:116

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

proof end;

theorem Th117: :: EUCLIDLP:117

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

proof end;

theorem Th118: :: EUCLIDLP:118

for n being 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 Th119: :: EUCLIDLP:119

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

proof end;

theorem Th120: :: EUCLIDLP:120

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

proof end;

theorem Th121: :: EUCLIDLP:121

for n being Nat
for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 is_line & L2 is_line & L1 misses L2 holds
L1 // L2

proof end;

theorem :: EUCLIDLP:122

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

proof end;