begin
Lm1:
for V being RealLinearSpace
for u, v being Element of V st ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) holds
( not u is zero & not v is zero & not are_Prop u,v )
theorem Th2:
for
V being
RealLinearSpace for
u,
v,
u1,
v1 being
Element of
V st ( for
a,
b,
a1,
b1 being
Real st
(((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
(
a = 0 &
b = 0 &
a1 = 0 &
b1 = 0 ) ) holds
( not
u is
zero & not
v is
zero & not
are_Prop u,
v & not
u1 is
zero & not
v1 is
zero & not
are_Prop u1,
v1 & not
u,
v,
u1 are_LinDep & not
u1,
v1,
u are_LinDep )
Lm2:
for V being RealLinearSpace
for v, w, u being Element of V
for a, b, c, d being Real holds a * (((b * v) + (c * w)) + (d * u)) = (((a * b) * v) + ((a * c) * w)) + ((a * d) * u)
Lm3:
for V being RealLinearSpace
for u, v, w, u1, v1, w1 being Element of V holds ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)
theorem Th3:
for
V being
RealLinearSpace for
p,
q,
r being
Element of
V st ( for
w being
Element of
V ex
a,
b,
c being
Real st
w = ((a * p) + (b * q)) + (c * r) ) & ( for
a,
b,
c being
Real st
((a * p) + (b * q)) + (c * r) = 0. V holds
(
a = 0 &
b = 0 &
c = 0 ) ) holds
for
u,
u1 being
Element of
V ex
y being
Element of
V st
(
p,
q,
y are_LinDep &
u,
u1,
y are_LinDep & not
y is
zero )
Lm4:
for V being RealLinearSpace
for v, w, u, y being Element of V
for a, b, c, d, d1 being Real holds a * ((((b * v) + (c * w)) + (d * u)) + (d1 * y)) = ((((a * b) * v) + ((a * c) * w)) + ((a * d) * u)) + ((a * d1) * y)
Lm5:
for V being RealLinearSpace
for u, v, w, y, u1, v1, w1, y1 being Element of V holds (((u + v) + w) + y) + (((u1 + v1) + w1) + y1) = (((u + u1) + (v + v1)) + (w + w1)) + (y + y1)
Lm6:
for V being RealLinearSpace
for v, w, u being Element of V
for a, b, c, d being Real holds a * (((b * v) + (c * w)) + (d * u)) = (((a * b) * v) + ((a * c) * w)) + ((a * d) * u)
Lm7:
for V being RealLinearSpace
for y, p, w, q, r being Element of V
for a1, b1, a, b, c being Real st y = (a1 * p) + (b1 * w) & w = ((a * p) + (b * q)) + (c * r) holds
y = (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r)
theorem Th4:
for
V being
RealLinearSpace for
p,
q,
r,
s being
Element of
V st ( for
w being
Element of
V ex
a,
b,
c,
d being
Real st
w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for
a,
b,
c,
d being
Real st
(((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds
(
a = 0 &
b = 0 &
c = 0 &
d = 0 ) ) holds
for
u,
v being
Element of
V st not
u is
zero & not
v is
zero holds
ex
y,
w being
Element of
V st
(
u,
v,
w are_LinDep &
q,
r,
y are_LinDep &
p,
w,
y are_LinDep & not
y is
zero & not
w is
zero )
theorem Th5:
for
V being
RealLinearSpace for
u,
v,
u1,
v1 being
Element of
V st ( for
a,
b,
a1,
b1 being
Real st
(((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
(
a = 0 &
b = 0 &
a1 = 0 &
b1 = 0 ) ) holds
for
y being
Element of
V holds
(
y is
zero or not
u,
v,
y are_LinDep or not
u1,
v1,
y are_LinDep )
definition
let V be
RealLinearSpace;
let u,
v,
w,
u1,
v1,
w1 be
Element of
V;
pred u,
v,
w,
u1,
v1,
w1 lie_on_a_triangle means :
Def2:
(
u,
v,
w1 are_LinDep &
u,
w,
v1 are_LinDep &
v,
w,
u1 are_LinDep );
end;
::
deftheorem Def2 defines
lie_on_a_triangle ANPROJ_2:def 2 :
for V being RealLinearSpace
for u, v, w, u1, v1, w1 being Element of V holds
( u,v,w,u1,v1,w1 lie_on_a_triangle iff ( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep ) );
definition
let V be
RealLinearSpace;
let o,
u,
v,
w,
u2,
v2,
w2 be
Element of
V;
pred o,
u,
v,
w,
u2,
v2,
w2 are_perspective means :
Def3:
(
o,
u,
u2 are_LinDep &
o,
v,
v2 are_LinDep &
o,
w,
w2 are_LinDep );
end;
::
deftheorem Def3 defines
are_perspective ANPROJ_2:def 3 :
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2 being Element of V holds
( o,u,v,w,u2,v2,w2 are_perspective iff ( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep ) );
Lm8:
for V being RealLinearSpace
for o being Element of V
for a being Real holds - (a * o) = (- a) * o
theorem Th6:
for
V being
RealLinearSpace for
o,
u,
u2 being
Element of
V st
o,
u,
u2 are_LinDep & not
are_Prop o,
u & not
are_Prop o,
u2 & not
are_Prop u,
u2 &
o,
u,
u2 are_Prop_Vect holds
( ex
a1,
b1 being
Real st
(
b1 * u2 = o + (a1 * u) &
a1 <> 0 &
b1 <> 0 ) & ex
a2,
c2 being
Real st
(
u2 = (c2 * o) + (a2 * u) &
c2 <> 0 &
a2 <> 0 ) )
Lm9:
for V being RealLinearSpace
for u2, w2 being Element of V
for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds
are_Prop u2,w2
Lm10:
for V being RealLinearSpace
for q, o, p, r, s being Element of V
for a, b being Real st q = o + (a * p) & r = o + (b * s) & are_Prop q,r & a <> 0 holds
o,p,s are_LinDep
Lm11:
for V being RealLinearSpace
for p, q being Element of V
for a being Real st a * p = q & a <> 0 & not p is zero holds
not q is zero
Lm12:
for V being RealLinearSpace
for r, u2, v2, o, u, v being Element of V
for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds
r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
Lm13:
for V being RealLinearSpace
for r, p, q, o being Element of V
for a, b being Real st r = (a * p) + (b * q) holds
r = ((0 * o) + (a * p)) + (b * q)
Lm14:
for V being RealLinearSpace
for p, q being Element of V holds (0 * p) + (0 * q) = 0. V
Lm15:
for V being RealLinearSpace
for o, v, w being Element of V
for b, a2, a3 being Real holds ((0 * o) + ((b * a2) * v)) + (((- b) * a3) * w) = b * ((a2 * v) - (a3 * w))
theorem Th8:
for
V being
RealLinearSpace for
o,
u,
v,
w,
u2,
v2,
w2,
u1,
v1,
w1 being
Element of
V st not
o is
zero &
u,
v,
w are_Prop_Vect &
u2,
v2,
w2 are_Prop_Vect &
u1,
v1,
w1 are_Prop_Vect &
o,
u,
v,
w,
u2,
v2,
w2 are_perspective & not
are_Prop o,
u2 & not
are_Prop o,
v2 & not
are_Prop o,
w2 & not
are_Prop u,
u2 & not
are_Prop v,
v2 & not
are_Prop w,
w2 & not
o,
u,
v are_LinDep & not
o,
u,
w are_LinDep & not
o,
v,
w are_LinDep &
u,
v,
w,
u1,
v1,
w1 lie_on_a_triangle &
u2,
v2,
w2,
u1,
v1,
w1 lie_on_a_triangle holds
u1,
v1,
w1 are_LinDep
definition
let V be
RealLinearSpace;
let o,
u,
v,
w,
u2,
v2,
w2 be
Element of
V;
pred o,
u,
v,
w,
u2,
v2,
w2 lie_on_an_angle means :
Def4:
( not
o,
u,
u2 are_LinDep &
o,
u,
v are_LinDep &
o,
u,
w are_LinDep &
o,
u2,
v2 are_LinDep &
o,
u2,
w2 are_LinDep );
end;
::
deftheorem Def4 defines
lie_on_an_angle ANPROJ_2:def 4 :
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2 being Element of V holds
( o,u,v,w,u2,v2,w2 lie_on_an_angle iff ( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep ) );
definition
let V be
RealLinearSpace;
let o,
u,
v,
w,
u2,
v2,
w2 be
Element of
V;
pred o,
u,
v,
w,
u2,
v2,
w2 are_half_mutually_not_Prop means :
Def5:
( not
are_Prop o,
v & not
are_Prop o,
w & not
are_Prop o,
v2 & not
are_Prop o,
w2 & not
are_Prop u,
v & not
are_Prop u,
w & not
are_Prop u2,
v2 & not
are_Prop u2,
w2 & not
are_Prop v,
w & not
are_Prop v2,
w2 );
end;
::
deftheorem Def5 defines
are_half_mutually_not_Prop ANPROJ_2:def 5 :
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2 being Element of V holds
( o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop iff ( not are_Prop o,v & not are_Prop o,w & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,v & not are_Prop u,w & not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v,w & not are_Prop v2,w2 ) );
Lm16:
for V being RealLinearSpace
for u2, w2 being Element of V
for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds
are_Prop u2,w2
Lm17:
for V being RealLinearSpace
for p, q, y being Element of V
for a being Real st not are_Prop p,q & y = a * q & a <> 0 holds
not are_Prop p,y
Lm18:
for V being RealLinearSpace
for w1, u, v2, o, u2 being Element of V
for a, b, c2 being Real st w1 = (a * u) + (b * v2) & v2 = o + (c2 * u2) holds
w1 = ((b * o) + (a * u)) + ((b * c2) * u2)
Lm19:
for V being RealLinearSpace
for w1, u2, v1, o, u being Element of V
for a, b, a2 being Real st w1 = (a * u2) + (b * v1) & v1 = o + (a2 * u) holds
w1 = ((b * o) + ((b * a2) * u)) + (a * u2)
Lm20:
for V being RealLinearSpace
for p, q being Element of V
for a being Real st a * p = q & a <> 0 & not p is zero holds
not q is zero
Lm21:
for V being RealLinearSpace
for p, q, y, s being Element of V
for a, b being Real st not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 holds
not are_Prop s,y
Lm22:
for V being RealLinearSpace
for r, u2, v2, o, u, v being Element of V
for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds
r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
Lm23:
for a2, a3, c2 being Real st a2 <> a3 & c2 <> 0 holds
(a3 * c2) - (a2 * c2) <> 0
Lm24:
for a2, a3, c3, c2, A1, A19, B1, B19 being Real st A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 & B1 * c3 = B19 * c2 & a2 <> a3 & c2 <> 0 holds
A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1
Lm25:
for c2, a2, a3, B1 being Real st c2 <> 0 & a2 <> a3 & B1 <> 0 holds
B1 * (((a3 * c2) - (a2 * c2)) ") <> 0
Lm26:
for V being RealLinearSpace
for u1, o, u, u2 being Element of V
for a3, c3, c2, a2, A1, B1 being Real st A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 & c2 <> 0 & a2 <> a3 & u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) holds
u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
Lm27:
for V being RealLinearSpace
for p, q, r, u, u2, u1 being Element of V holds ((p + q) + r) + ((u + u2) + u1) = ((p + u) + (q + u2)) + (r + u1)
Lm28:
for V being RealLinearSpace
for u1, o, u, u2, v1, w2 being Element of V
for a3, c3, a2, c2, C2, C3 being Real st u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) & v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) & C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) holds
((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V
Lm29:
for V being RealLinearSpace
for w2, o, u, u2, w1 being Element of V
for a2, c2, A3, A39, B3, B39 being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B39 & A3 = B39 * a2 holds
w1 = B3 * w2
theorem Th9:
for
V being
RealLinearSpace for
o,
u,
v,
w,
u2,
v2,
w2,
u1,
v1,
w1 being
Element of
V st not
o is
zero &
u,
v,
w are_Prop_Vect &
u2,
v2,
w2 are_Prop_Vect &
u1,
v1,
w1 are_Prop_Vect &
o,
u,
v,
w,
u2,
v2,
w2 lie_on_an_angle &
o,
u,
v,
w,
u2,
v2,
w2 are_half_mutually_not_Prop &
u,
v2,
w1 are_LinDep &
u2,
v,
w1 are_LinDep &
u,
w2,
v1 are_LinDep &
w,
u2,
v1 are_LinDep &
v,
w2,
u1 are_LinDep &
w,
v2,
u1 are_LinDep holds
u1,
v1,
w1 are_LinDep
theorem Th11:
for
A being non
empty set for
f,
g,
h being
Element of
Funcs (
A,
REAL)
for
x1,
x2,
x3 being
Element of
A st
x1 <> x2 &
x1 <> x3 &
x2 <> x3 &
f . x1 = 1 & ( for
z being
set st
z in A &
z <> x1 holds
f . z = 0 ) &
g . x2 = 1 & ( for
z being
set st
z in A &
z <> x2 holds
g . z = 0 ) &
h . x3 = 1 & ( for
z being
set st
z in A &
z <> x3 holds
h . z = 0 ) holds
for
a,
b,
c being
Real st
(RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),
((RealFuncExtMult A) . [c,h]))
= RealFuncZero A holds
(
a = 0 &
b = 0 &
c = 0 )
theorem
for
A being non
empty set for
x1,
x2,
x3 being
Element of
A st
x1 <> x2 &
x1 <> x3 &
x2 <> x3 holds
ex
f,
g,
h being
Element of
Funcs (
A,
REAL) st
for
a,
b,
c being
Real st
(RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),
((RealFuncExtMult A) . [c,h]))
= RealFuncZero A holds
(
a = 0 &
b = 0 &
c = 0 )
theorem Th13:
for
A being non
empty set for
f,
g,
h being
Element of
Funcs (
A,
REAL)
for
x1,
x2,
x3 being
Element of
A st
A = {x1,x2,x3} &
x1 <> x2 &
x1 <> x3 &
x2 <> x3 &
f . x1 = 1 & ( for
z being
set st
z in A &
z <> x1 holds
f . z = 0 ) &
g . x2 = 1 & ( for
z being
set st
z in A &
z <> x2 holds
g . z = 0 ) &
h . x3 = 1 & ( for
z being
set st
z in A &
z <> x3 holds
h . z = 0 ) holds
for
h9 being
Element of
Funcs (
A,
REAL) ex
a,
b,
c being
Real st
h9 = (RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),
((RealFuncExtMult A) . [c,h]))
theorem
for
A being non
empty set for
x1,
x2,
x3 being
Element of
A st
A = {x1,x2,x3} &
x1 <> x2 &
x1 <> x3 &
x2 <> x3 holds
ex
f,
g,
h being
Element of
Funcs (
A,
REAL) st
for
h9 being
Element of
Funcs (
A,
REAL) ex
a,
b,
c being
Real st
h9 = (RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),
((RealFuncExtMult A) . [c,h]))
theorem Th15:
for
A being non
empty set for
x1,
x2,
x3 being
Element of
A st
A = {x1,x2,x3} &
x1 <> x2 &
x1 <> x3 &
x2 <> x3 holds
ex
f,
g,
h being
Element of
Funcs (
A,
REAL) st
( ( for
a,
b,
c being
Real st
(RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),
((RealFuncExtMult A) . [c,h]))
= RealFuncZero A holds
(
a = 0 &
b = 0 &
c = 0 ) ) & ( for
h9 being
Element of
Funcs (
A,
REAL) ex
a,
b,
c being
Real st
h9 = (RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),
((RealFuncExtMult A) . [c,h])) ) )
Lm30:
ex A being non empty set ex x1, x2, x3 being Element of A st
( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )
theorem Th17:
for
A being non
empty set for
f,
g,
h,
f1 being
Element of
Funcs (
A,
REAL)
for
x1,
x2,
x3,
x4 being
Element of
A st
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 &
f . x1 = 1 & ( for
z being
set st
z in A &
z <> x1 holds
f . z = 0 ) &
g . x2 = 1 & ( for
z being
set st
z in A &
z <> x2 holds
g . z = 0 ) &
h . x3 = 1 & ( for
z being
set st
z in A &
z <> x3 holds
h . z = 0 ) &
f1 . x4 = 1 & ( for
z being
set st
z in A &
z <> x4 holds
f1 . z = 0 ) holds
for
a,
b,
c,
d being
Real st
(RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),
((RealFuncExtMult A) . [d,f1]))
= RealFuncZero A holds
(
a = 0 &
b = 0 &
c = 0 &
d = 0 )
theorem
for
A being non
empty set for
x1,
x2,
x3,
x4 being
Element of
A st
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 holds
ex
f,
g,
h,
f1 being
Element of
Funcs (
A,
REAL) st
for
a,
b,
c,
d being
Real st
(RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),
((RealFuncExtMult A) . [d,f1]))
= RealFuncZero A holds
(
a = 0 &
b = 0 &
c = 0 &
d = 0 )
theorem Th19:
for
A being non
empty set for
f,
g,
h,
f1 being
Element of
Funcs (
A,
REAL)
for
x1,
x2,
x3,
x4 being
Element of
A st
A = {x1,x2,x3,x4} &
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 &
f . x1 = 1 & ( for
z being
set st
z in A &
z <> x1 holds
f . z = 0 ) &
g . x2 = 1 & ( for
z being
set st
z in A &
z <> x2 holds
g . z = 0 ) &
h . x3 = 1 & ( for
z being
set st
z in A &
z <> x3 holds
h . z = 0 ) &
f1 . x4 = 1 & ( for
z being
set st
z in A &
z <> x4 holds
f1 . z = 0 ) holds
for
h9 being
Element of
Funcs (
A,
REAL) ex
a,
b,
c,
d being
Real st
h9 = (RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),
((RealFuncExtMult A) . [d,f1]))
theorem
for
A being non
empty set for
x1,
x2,
x3,
x4 being
Element of
A st
A = {x1,x2,x3,x4} &
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 holds
ex
f,
g,
h,
f1 being
Element of
Funcs (
A,
REAL) st
for
h9 being
Element of
Funcs (
A,
REAL) ex
a,
b,
c,
d being
Real st
h9 = (RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),
((RealFuncExtMult A) . [d,f1]))
theorem Th21:
for
A being non
empty set for
x1,
x2,
x3,
x4 being
Element of
A st
A = {x1,x2,x3,x4} &
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 holds
ex
f,
g,
h,
f1 being
Element of
Funcs (
A,
REAL) st
( ( for
a,
b,
c,
d being
Real st
(RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),
((RealFuncExtMult A) . [d,f1]))
= RealFuncZero A holds
(
a = 0 &
b = 0 &
c = 0 &
d = 0 ) ) & ( for
h9 being
Element of
Funcs (
A,
REAL) ex
a,
b,
c,
d being
Real st
h9 = (RealFuncAdd A) . (
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),
((RealFuncExtMult A) . [d,f1])) ) )
Lm31:
ex A being non empty set ex x1, x2, x3, x4 being Element of A st
( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )
definition
let CS be non
empty CollStr ;
compatibility
( CS is reflexive iff for p, q, r being Element of CS holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear ) )
redefine attr CS is
transitive means :
Def8:
for
p,
q,
r,
r1,
r2 being
Element of
CS st
p <> q &
p,
q,
r is_collinear &
p,
q,
r1 is_collinear &
p,
q,
r2 is_collinear holds
r,
r1,
r2 is_collinear ;
compatibility
( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear )
end;
::
deftheorem Def8 defines
transitive ANPROJ_2:def 8 :
for CS being non empty CollStr holds
( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear );
definition
let IT be non
empty CollStr ;
attr IT is
Vebleian means :
Def9:
for
p,
p1,
p2,
r,
r1 being
Element of
IT st
p,
p1,
r is_collinear &
p1,
p2,
r1 is_collinear holds
ex
r2 being
Element of
IT st
(
p,
p2,
r2 is_collinear &
r,
r1,
r2 is_collinear );
end;
::
deftheorem Def9 defines
Vebleian ANPROJ_2:def 9 :
for IT being non empty CollStr holds
( IT is Vebleian iff for p, p1, p2, r, r1 being Element of IT st p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of IT st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear ) );
Lm32:
for V being non trivial RealLinearSpace holds ProjectiveSpace V is reflexive
Lm33:
for V being non trivial RealLinearSpace holds ProjectiveSpace V is transitive
theorem Th24:
for
V being non
trivial RealLinearSpace for
p,
q,
r being
Element of
(ProjectiveSpace V) st
p,
q,
r is_collinear holds
(
p,
r,
q is_collinear &
q,
p,
r is_collinear &
r,
q,
p is_collinear &
r,
p,
q is_collinear &
q,
r,
p is_collinear )
Lm34:
for V being non trivial RealLinearSpace
for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st p,p1,p2 is_collinear & p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
Lm35:
for V being non trivial RealLinearSpace
for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st not p,p1,p2 is_collinear & p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
Lm36:
for V being non trivial RealLinearSpace holds ProjectiveSpace V is Vebleian
Lm37:
for V being non trivial RealLinearSpace st V is up-3-dimensional holds
ProjectiveSpace V is proper
Lm38:
for V being non trivial RealLinearSpace st V is up-3-dimensional holds
ProjectiveSpace V is at_least_3rank
definition
let IT be
CollProjectiveSpace;
attr IT is
Fanoian means :
Def11:
for
p1,
r2,
q,
r1,
q1,
p,
r being
Element of
IT st
p1,
r2,
q is_collinear &
r1,
q1,
q is_collinear &
p1,
r1,
p is_collinear &
r2,
q1,
p is_collinear &
p1,
q1,
r is_collinear &
r2,
r1,
r is_collinear &
p,
q,
r is_collinear & not
p1,
r2,
q1 is_collinear & not
p1,
r2,
r1 is_collinear & not
p1,
r1,
q1 is_collinear holds
r2,
r1,
q1 is_collinear ;
attr IT is
Desarguesian means
for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Element of
IT st
o <> q1 &
p1 <> q1 &
o <> q2 &
p2 <> q2 &
o <> q3 &
p3 <> q3 & not
o,
p1,
p2 is_collinear & not
o,
p1,
p3 is_collinear & not
o,
p2,
p3 is_collinear &
p1,
p2,
r3 is_collinear &
q1,
q2,
r3 is_collinear &
p2,
p3,
r1 is_collinear &
q2,
q3,
r1 is_collinear &
p1,
p3,
r2 is_collinear &
q1,
q3,
r2 is_collinear &
o,
p1,
q1 is_collinear &
o,
p2,
q2 is_collinear &
o,
p3,
q3 is_collinear holds
r1,
r2,
r3 is_collinear ;
attr IT is
Pappian means
for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Element of
IT st
o <> p2 &
o <> p3 &
p2 <> p3 &
p1 <> p2 &
p1 <> p3 &
o <> q2 &
o <> q3 &
q2 <> q3 &
q1 <> q2 &
q1 <> q3 & not
o,
p1,
q1 is_collinear &
o,
p1,
p2 is_collinear &
o,
p1,
p3 is_collinear &
o,
q1,
q2 is_collinear &
o,
q1,
q3 is_collinear &
p1,
q2,
r3 is_collinear &
q1,
p2,
r3 is_collinear &
p1,
q3,
r2 is_collinear &
p3,
q1,
r2 is_collinear &
p2,
q3,
r1 is_collinear &
p3,
q2,
r1 is_collinear holds
r1,
r2,
r3 is_collinear ;
end;
::
deftheorem Def11 defines
Fanoian ANPROJ_2:def 11 :
for IT being CollProjectiveSpace holds
( IT is Fanoian iff for p1, r2, q, r1, q1, p, r being Element of IT st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear );
::
deftheorem defines
Desarguesian ANPROJ_2:def 12 :
for IT being CollProjectiveSpace holds
( IT is Desarguesian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear );
::
deftheorem defines
Pappian ANPROJ_2:def 13 :
for IT being CollProjectiveSpace holds
( IT is Pappian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear );
definition
let IT be
CollProjectiveSpace;
attr IT is
at_most-3-dimensional means :
Def15:
for
p,
p1,
q,
q1,
r2 being
Element of
IT ex
r,
r1 being
Element of
IT st
(
p,
q,
r is_collinear &
p1,
q1,
r1 is_collinear &
r2,
r,
r1 is_collinear );
end;
::
deftheorem Def15 defines
at_most-3-dimensional ANPROJ_2:def 15 :
for IT being CollProjectiveSpace holds
( IT is at_most-3-dimensional iff for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) );
theorem Th26:
for
V being non
trivial RealLinearSpace for
p1,
r2,
q,
r1,
q1,
p,
r being
Element of
(ProjectiveSpace V) st
p1,
r2,
q is_collinear &
r1,
q1,
q is_collinear &
p1,
r1,
p is_collinear &
r2,
q1,
p is_collinear &
p1,
q1,
r is_collinear &
r2,
r1,
r is_collinear &
p,
q,
r is_collinear & not
p1,
r2,
q1 is_collinear & not
p1,
r2,
r1 is_collinear & not
p1,
r1,
q1 is_collinear holds
r2,
r1,
q1 is_collinear
Lm39:
for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Fanoian
Lm40:
for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Desarguesian
Lm41:
for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Pappian
theorem Th27:
for
V being non
trivial RealLinearSpace st ex
u,
v,
w being
Element of
V st
( ( for
a,
b,
c being
Real st
((a * u) + (b * v)) + (c * w) = 0. V holds
(
a = 0 &
b = 0 &
c = 0 ) ) & ( for
y being
Element of
V ex
a,
b,
c being
Real st
y = ((a * u) + (b * v)) + (c * w) ) ) holds
ex
x1,
x2 being
Element of
(ProjectiveSpace V) st
(
x1 <> x2 & ( for
r1,
r2 being
Element of
(ProjectiveSpace V) ex
q being
Element of
(ProjectiveSpace V) st
(
x1,
x2,
q is_collinear &
r1,
r2,
q is_collinear ) ) )
theorem Th28:
for
V being non
trivial RealLinearSpace st ex
x1,
x2 being
Element of
(ProjectiveSpace V) st
(
x1 <> x2 & ( for
r1,
r2 being
Element of
(ProjectiveSpace V) ex
q being
Element of
(ProjectiveSpace V) st
(
x1,
x2,
q is_collinear &
r1,
r2,
q is_collinear ) ) ) holds
for
p,
p1,
q,
q1 being
Element of
(ProjectiveSpace V) ex
r being
Element of
(ProjectiveSpace V) st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
Lm42:
for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st
for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds
V is up-3-dimensional
Lm43:
for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st
for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds
( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank )
theorem Th30:
for
V being non
trivial RealLinearSpace st ex
y,
u,
v,
w being
Element of
V st
( ( for
w1 being
Element of
V ex
a,
b,
a1,
b1 being
Real st
w1 = (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) ) & ( for
a,
b,
a1,
b1 being
Real st
(((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
(
a = 0 &
b = 0 &
a1 = 0 &
b1 = 0 ) ) ) holds
ex
p,
q1,
q2 being
Element of
(ProjectiveSpace V) st
( not
p,
q1,
q2 is_collinear & ( for
r1,
r2 being
Element of
(ProjectiveSpace V) ex
q3,
r3 being
Element of
(ProjectiveSpace V) st
(
r1,
r2,
r3 is_collinear &
q1,
q2,
q3 is_collinear &
p,
r3,
q3 is_collinear ) ) )
Lm44:
for V being non trivial RealLinearSpace
for x, d, b, b9, d9, q being Element of (ProjectiveSpace V) st not q,b,d is_collinear & b,d,x is_collinear & q,b9,b is_collinear & q,d9,d is_collinear holds
ex o being Element of (ProjectiveSpace V) st
( b9,d9,o is_collinear & q,x,o is_collinear )
theorem Th31:
for
V being non
trivial RealLinearSpace st
ProjectiveSpace V is
proper &
ProjectiveSpace V is
at_least_3rank & ex
p,
q1,
q2 being
Element of
(ProjectiveSpace V) st
( not
p,
q1,
q2 is_collinear & ( for
r1,
r2 being
Element of
(ProjectiveSpace V) ex
q3,
r3 being
Element of
(ProjectiveSpace V) st
(
r1,
r2,
r3 is_collinear &
q1,
q2,
q3 is_collinear &
p,
r3,
q3 is_collinear ) ) ) holds
ex
CS being
CollProjectiveSpace st
(
CS = ProjectiveSpace V &
CS is
at_most-3-dimensional )