begin
Lm1:
for n being Element of NAT
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
theorem Th24:
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)
theorem Th26:
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)
theorem Th27:
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))
theorem Th28:
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 )
Lm2:
for n being Element of NAT
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 <> 0* n
theorem Th36:
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) )
theorem Th40:
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
Lm3:
for n being Element of NAT
for x1, x2 being Element of REAL n st x1 // x2 holds
x1,x2 are_ldependent2
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
definition
let n be
Element of
NAT ;
let L1,
L2 be
Element of
line_of_REAL n;
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;
definition
let n be
Element of
NAT ;
let L1,
L2 be
Element of
line_of_REAL n;
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;
theorem
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) ) )
theorem Th83:
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)
theorem Th85:
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)
theorem
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) )