:: A Construction of Analytical Projective Space
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received June 15, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem ANPROJ_1:def 1 :
canceled;
:: deftheorem Def2 defines are_Prop ANPROJ_1:def 2 :
theorem :: ANPROJ_1:1
canceled;
theorem :: ANPROJ_1:2
canceled;
theorem :: ANPROJ_1:3
canceled;
theorem :: ANPROJ_1:4
canceled;
theorem Th5: :: ANPROJ_1:5
theorem Th6: :: ANPROJ_1:6
theorem Th7: :: ANPROJ_1:7
:: deftheorem Def3 defines are_LinDep ANPROJ_1:def 3 :
theorem :: ANPROJ_1:8
canceled;
theorem Th9: :: ANPROJ_1:9
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 Th10: :: ANPROJ_1:10
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)
theorem Th11: :: ANPROJ_1:11
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))
theorem :: ANPROJ_1:12
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 :: ANPROJ_1:13
theorem Th14: :: ANPROJ_1:14
theorem Th15: :: ANPROJ_1:15
theorem Th16: :: ANPROJ_1:16
theorem Th17: :: ANPROJ_1:17
theorem Th18: :: ANPROJ_1:18
theorem Th19: :: ANPROJ_1:19
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 :: ANPROJ_1:20
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 )
theorem :: ANPROJ_1:21
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
theorem :: ANPROJ_1:22
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 :: ANPROJ_1:23
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
:: deftheorem Def4 defines Proper_Vectors_of ANPROJ_1:def 4 :
theorem :: ANPROJ_1:24
canceled;
theorem :: ANPROJ_1:25
canceled;
theorem Th26: :: ANPROJ_1:26
definition
let V be
RealLinearSpace;
func Proportionality_as_EqRel_of V -> Equivalence_Relation of
Proper_Vectors_of V means :
Def5:
:: ANPROJ_1:def 5
for
x,
y being
set holds
(
[x,y] in it iff (
x in Proper_Vectors_of V &
y in Proper_Vectors_of V & ex
u,
v being
Element of
V st
(
x = u &
y = v &
are_Prop u,
v ) ) );
existence
ex b1 being Equivalence_Relation of Proper_Vectors_of V st
for x, y being set holds
( [x,y] in b1 iff ( x in Proper_Vectors_of V & y in Proper_Vectors_of 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 Proper_Vectors_of V st ( for x, y being set holds
( [x,y] in b1 iff ( x in Proper_Vectors_of V & y in Proper_Vectors_of 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 Proper_Vectors_of V & y in Proper_Vectors_of V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines Proportionality_as_EqRel_of ANPROJ_1:def 5 :
theorem :: ANPROJ_1:27
canceled;
theorem :: ANPROJ_1:28
theorem Th29: :: ANPROJ_1:29
:: deftheorem defines Dir ANPROJ_1:def 6 :
:: deftheorem Def7 defines ProjectivePoints ANPROJ_1:def 7 :
:: deftheorem Def8 defines trivial ANPROJ_1:def 8 :
theorem :: ANPROJ_1:30
canceled;
theorem :: ANPROJ_1:31
canceled;
theorem :: ANPROJ_1:32
canceled;
theorem :: ANPROJ_1:33
theorem Th34: :: ANPROJ_1:34
theorem Th35: :: ANPROJ_1:35
definition
let V be non
trivial RealLinearSpace;
func ProjectiveCollinearity V -> Relation3 of
ProjectivePoints V means :
Def9:
:: ANPROJ_1:def 9
for
x,
y,
z being
set holds
(
[x,y,z] in it 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 ) );
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;
:: deftheorem Def9 defines ProjectiveCollinearity ANPROJ_1:def 9 :
:: deftheorem defines ProjectiveSpace ANPROJ_1:def 10 :
theorem :: ANPROJ_1:36
canceled;
theorem :: ANPROJ_1:37
canceled;
theorem :: ANPROJ_1:38
canceled;
theorem :: ANPROJ_1:39
theorem :: ANPROJ_1:40
theorem :: ANPROJ_1:41
theorem :: ANPROJ_1:42