:: ANPROJ_1 semantic presentation

notation

let V be RealLinearSpace;
let p be Element of V;
synonym p is_Prop_Vect for non-zero p;

end;

definition

let V be RealLinearSpace;
let p, q be Element of V;
canceled;
pred are_Prop p,q means :Def2: :: ANPROJ_1:def 2
ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 );
reflexivity

proof end;

symmetry ;

end;

:: deftheorem ANPROJ_1:def 1 :

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

for V being RealLinearSpace
for p, q being Element of V holds
( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) )

proof end;

theorem Th6: :: ANPROJ_1:6

for V being RealLinearSpace
for p, u, q being Element of V st are_Prop p,u & are_Prop u,q holds
are_Prop p,q

proof end;

theorem Th7: :: ANPROJ_1:7

for V being RealLinearSpace
for p being Element of V holds
( are_Prop p, 0. V iff p = 0. V )

proof end;

definition

let V be RealLinearSpace;
let u, v, w be Element of V;
pred u,v,w are_LinDep means :Def3: :: ANPROJ_1:def 3
ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) );

end;

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

proof end;

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 )

proof end;

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

proof end;

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)

proof end;

theorem Th11: :: ANPROJ_1:11

for V being RealLinearSpace
for v, w, u being Element of V st v is_Prop_Vect & w is_Prop_Vect & not are_Prop v,w holds
( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )

proof end;

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)

proof end;

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)

proof end;

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

proof end;

theorem :: ANPROJ_1:12

for V being RealLinearSpace
for p, q being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & p is_Prop_Vect & q is_Prop_Vect holds
( a1 = a2 & b1 = b2 )

proof end;

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

proof end;

theorem :: ANPROJ_1:13

for V being RealLinearSpace
for u, v, w being Element of V
for a1, b1, c1, a2, b2, c2 being Real st not u,v,w are_LinDep & ((a1 * u) + (b1 * v)) + (c1 * w) = ((a2 * u) + (b2 * v)) + (c2 * w) holds
( a1 = a2 & b1 = b2 & c1 = c2 )

proof end;

theorem Th14: :: ANPROJ_1:14

for V being RealLinearSpace
for p, q, u, v being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & u = (a1 * p) + (b1 * q) & v = (a2 * p) + (b2 * q) & (a1 * b2) - (a2 * b1) = 0 & p is_Prop_Vect & q is_Prop_Vect & not are_Prop u,v & not u = 0. V holds
v = 0. V

proof end;

theorem Th15: :: ANPROJ_1:15

for V being RealLinearSpace
for u, v, w being Element of V st ( u = 0. V or v = 0. V or w = 0. V ) holds
u,v,w are_LinDep

proof end;

theorem Th16: :: ANPROJ_1:16

for V being RealLinearSpace
for u, v, w being Element of V st ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) holds
w,u,v are_LinDep

proof end;

theorem Th17: :: ANPROJ_1:17

for V being RealLinearSpace
for u, v, w being Element of V st not u,v,w are_LinDep holds
( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )

proof end;

theorem Th18: :: ANPROJ_1:18

for V being RealLinearSpace
for p, q being Element of V st p + q = 0. V holds
are_Prop p,q

proof end;

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 & p is_Prop_Vect & q is_Prop_Vect holds
u,v,w are_LinDep

proof end;

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)

proof end;

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 & y is_Prop_Vect )

proof end;

theorem :: ANPROJ_1:21

for V being RealLinearSpace
for p, q being Element of V st not are_Prop p,q & p is_Prop_Vect & q is_Prop_Vect holds
for u, v being Element of V ex y being Element of V st
( y is_Prop_Vect & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y )

proof end;

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 u is_Prop_Vect & v is_Prop_Vect & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep

proof end;

theorem :: ANPROJ_1:22

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 u is_Prop_Vect & v is_Prop_Vect & not are_Prop u,v holds
ex y being Element of V st
( y is_Prop_Vect & not u,v,y are_LinDep )

proof end;

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)

proof end;

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 & p is_Prop_Vect & q is_Prop_Vect & r is_Prop_Vect & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds
v,w,y are_LinDep

proof end;

definition

let V be RealLinearSpace;
func Proper_Vectors_of V -> set means :Def4: :: ANPROJ_1:def 4
for u being set holds
( u in it iff ( u <> 0. V & u is Element of V ) );
existence

proof end;

uniqueness

proof end;

end;

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

for V being RealLinearSpace
for u being Element of V holds
( u in Proper_Vectors_of V iff u is_Prop_Vect )

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Proportionality_as_EqRel_of ANPROJ_1:def 5 :

theorem :: ANPROJ_1:27

canceled;

theorem :: ANPROJ_1:28

for V being RealLinearSpace
for x, y being set st [x,y] in Proportionality_as_EqRel_of V holds
( x is Element of V & y is Element of V )

proof end;

theorem Th29: :: ANPROJ_1:29

for V being RealLinearSpace
for u, v being Element of V holds
( [u,v] in Proportionality_as_EqRel_of V iff ( u is_Prop_Vect & v is_Prop_Vect & are_Prop u,v ) )

proof end;

definition

let V be RealLinearSpace;
let v be Element of V;
func Dir v -> Subset of (Proper_Vectors_of V) equals :: ANPROJ_1:def 6
Class (Proportionality_as_EqRel_of V),v;
correctness ;

end;

:: deftheorem defines Dir ANPROJ_1:def 6 :

definition

let V be RealLinearSpace;
func ProjectivePoints V -> set means :Def7: :: ANPROJ_1:def 7
ex Y being Subset-Family of (Proper_Vectors_of V) st
( Y = Class (Proportionality_as_EqRel_of V) & it = Y );
correctness ;

end;

:: deftheorem Def7 defines ProjectivePoints ANPROJ_1:def 7 :

definition

let V be non empty ZeroStr ;
redefine attr V is trivial means :Def8: :: ANPROJ_1:def 8
for u being Element of V holds u = 0. V;
compatibility

proof end;

end;

:: deftheorem Def8 defines trivial ANPROJ_1:def 8 :

registration

cluster strict non trivial RLSStruct ;
existence

proof end;

end;

theorem :: ANPROJ_1:30

canceled;

theorem :: ANPROJ_1:31

canceled;

theorem :: ANPROJ_1:32

canceled;

theorem :: ANPROJ_1:33

for V being RealLinearSpace holds
( V is non trivial RealLinearSpace iff ex u being Element of V st u in Proper_Vectors_of V )

proof end;

registration

let V be non trivial RealLinearSpace;
cluster Proper_Vectors_of V -> non empty ;
coherence

proof end;

cluster ProjectivePoints V -> non empty ;
coherence

proof end;

end;

theorem Th34: :: ANPROJ_1:34

for V being non trivial RealLinearSpace
for p being Element of V st p is_Prop_Vect holds
Dir p is Element of ProjectivePoints V

proof end;

theorem Th35: :: ANPROJ_1:35

for V being non trivial RealLinearSpace
for p, q being Element of V st p is_Prop_Vect & q is_Prop_Vect holds
( Dir p = Dir q iff are_Prop p,q )

proof end;

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 & p is_Prop_Vect & q is_Prop_Vect & r is_Prop_Vect & p,q,r are_LinDep ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines ProjectiveCollinearity ANPROJ_1:def 9 :

definition

let V be non trivial RealLinearSpace;
func ProjectiveSpace V -> strict CollStr equals :: ANPROJ_1:def 10
CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);
correctness ;

end;

:: deftheorem defines ProjectiveSpace ANPROJ_1:def 10 :

registration

let V be non trivial RealLinearSpace;
cluster ProjectiveSpace V -> non empty strict ;
coherence

proof end;

end;

theorem :: ANPROJ_1:36

canceled;

theorem :: ANPROJ_1:37

canceled;

theorem :: ANPROJ_1:38

canceled;

theorem :: ANPROJ_1:39

for V being non trivial RealLinearSpace holds
( the carrier of (ProjectiveSpace V) = ProjectivePoints V & the Collinearity of (ProjectiveSpace V) = ProjectiveCollinearity V ) ;

theorem :: ANPROJ_1:40

for x, y, z being set
for V being non trivial RealLinearSpace st [x,y,z] in the Collinearity of (ProjectiveSpace V) holds
ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & p is_Prop_Vect & q is_Prop_Vect & r is_Prop_Vect & p,q,r are_LinDep ) by Def9;

theorem :: ANPROJ_1:41

for V being non trivial RealLinearSpace
for u, v, w being Element of V st u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect holds
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )

proof end;

theorem :: ANPROJ_1:42

for x being set
for V being non trivial RealLinearSpace holds
( x is Element of (ProjectiveSpace V) iff ex u being Element of V st
( u is_Prop_Vect & x = Dir u ) )

proof end;