begin
theorem Th4:
for
V being
RealLinearSpace for
u,
u1,
v,
v1,
w,
w1 being
Element of
V st
are_Prop u,
u1 &
are_Prop v,
v1 &
are_Prop w,
w1 &
u,
v,
w are_LinDep holds
u1,
v1,
w1 are_LinDep
theorem Th5:
for
V being
RealLinearSpace for
u,
v,
w being
Element of
V st
u,
v,
w are_LinDep holds
(
u,
w,
v are_LinDep &
v,
u,
w are_LinDep &
w,
v,
u are_LinDep &
w,
u,
v are_LinDep &
v,
w,
u are_LinDep )
Lm1:
for V being RealLinearSpace
for v, w being Element of V
for a, b being Real st (a * v) + (b * w) = 0. V holds
a * v = (- b) * w
Lm2:
for V being RealLinearSpace
for u, v, w being Element of V
for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V & a <> 0 holds
u = ((- ((a ") * b)) * v) + ((- ((a ") * c)) * w)
Lm3:
for V being RealLinearSpace
for p being Element of V
for a, b, c being Real holds ((a + b) + c) * p = ((a * p) + (b * p)) + (c * p)
Lm4:
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)
Lm5:
for V being RealLinearSpace
for p, q being Element of V
for a, a1, b1 being Real holds ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
Lm6:
for V being RealLinearSpace
for p, v, q being Element of V
for a, b being Real st p + (a * v) = q + (b * v) holds
((a - b) * v) + p = q
theorem Th14:
for
V being
RealLinearSpace for
p,
q,
u,
v,
w being
Element of
V st not
are_Prop p,
q &
p,
q,
u are_LinDep &
p,
q,
v are_LinDep &
p,
q,
w are_LinDep & not
p is
zero & not
q is
zero holds
u,
v,
w are_LinDep
Lm7:
for V being RealLinearSpace
for v, w being Element of V
for a, b, c being Real holds a * ((b * v) + (c * w)) = ((a * b) * v) + ((a * c) * w)
theorem
for
V being
RealLinearSpace for
u,
v,
w,
p,
q being
Element of
V st not
u,
v,
w are_LinDep &
u,
v,
p are_LinDep &
v,
w,
q are_LinDep holds
ex
y being
Element of
V st
(
u,
w,
y are_LinDep &
p,
q,
y are_LinDep & not
y is
zero )
Lm8:
for V being RealLinearSpace
for p, q, r being Element of V st not p,q,r are_LinDep holds
for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep
Lm9:
for V being RealLinearSpace
for u, w, y being Element of V
for a, b, c, d, e, f, A, B, C being Real holds ((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y))) = ((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)
theorem
for
V being
RealLinearSpace for
u,
v,
q,
w,
y,
p,
r being
Element of
V st
u,
v,
q are_LinDep &
w,
y,
q are_LinDep &
u,
w,
p are_LinDep &
v,
y,
p are_LinDep &
u,
y,
r are_LinDep &
v,
w,
r are_LinDep &
p,
q,
r are_LinDep & not
p is
zero & not
q is
zero & not
r is
zero & not
u,
v,
y are_LinDep & not
u,
v,
w are_LinDep & not
u,
w,
y are_LinDep holds
v,
w,
y are_LinDep
definition
let V be
RealLinearSpace;
existence
ex b1 being Equivalence_Relation of (NonZero V) st
for x, y being set holds
( [x,y] in b1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) )
uniqueness
for b1, b2 being Equivalence_Relation of (NonZero V) st ( for x, y being set holds
( [x,y] in b1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) holds
b1 = b2
end;
definition
let V be non
trivial RealLinearSpace;
existence
ex b1 being Relation3 of ProjectivePoints V st
for x, y, z being set holds
( [x,y,z] in b1 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) )
uniqueness
for b1, b2 being Relation3 of ProjectivePoints V st ( for x, y, z being set holds
( [x,y,z] in b1 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) & ( for x, y, z being set holds
( [x,y,z] in b2 iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) ) holds
b1 = b2
end;