:: A Construction of Analytical Projective Space
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received June 15, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let V be RealLinearSpace;
let p, q be Element of V;

pred are_Prop p,q means :: ANPROJ_1:def 1
ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 );

reflexivity
for p being Element of V ex a, b being Real st
( a * p = b * p & a <> 0 & b <> 0 )

proof end;

symmetry
for p, q being Element of V st ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 ) holds
ex a, b being Real st
( a * q = b * p & a <> 0 & b <> 0 ) ;

end;

:: deftheorem defines are_Prop ANPROJ_1:def 1 :
for V being RealLinearSpace
for p, q being Element of V holds
( are_Prop p,q iff ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 ) );

theorem Th1: :: ANPROJ_1:1

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 Th2: :: ANPROJ_1:2

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

proof end;

theorem Th3: :: ANPROJ_1:3

for V being RealLinearSpace
for p being Element of V holds
( are_Prop p, 0. V iff p = 0. V ) by RLVECT_1:11;

definition

let V be RealLinearSpace;
let u, v, w be Element of V;

pred u,v,w are_LinDep means :: ANPROJ_1:def 2
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 defines are_LinDep ANPROJ_1:def 2 :
for V being RealLinearSpace
for u, v, w being Element of V holds
( u,v,w are_LinDep iff ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) );

theorem Th4: :: ANPROJ_1:4

for V being RealLinearSpace
for u, v, w, u1, v1, 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 Th5: :: ANPROJ_1:5

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 Th6: :: ANPROJ_1:6

for V being RealLinearSpace
for u, v, w being Element of V st not v is zero & not w is zero & 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:7

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) & not p is zero & not q is zero holds
( a1 = a2 & b1 = b2 )

proof end;

Lm6: for V being RealLinearSpace
for p, q, v 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:8

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 Th9: :: ANPROJ_1:9

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 & not p is zero & not q is zero & not are_Prop u,v & not u = 0. V holds
v = 0. V

proof end;

theorem Th10: :: ANPROJ_1:10

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 Th11: :: ANPROJ_1:11

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 Th12: :: ANPROJ_1:12

for V being RealLinearSpace
for u, v, w being Element of V st not u,v,w are_LinDep holds
( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u ) by Th10, Th11;

theorem Th13: :: ANPROJ_1:13

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

proof end;

theorem Th14: :: ANPROJ_1:14

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

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

for V being RealLinearSpace
for p, q, u, v, w 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 )

proof end;

theorem :: ANPROJ_1:16

for V being RealLinearSpace
for p, q being Element of V st not are_Prop p,q & not p is zero & not q is zero holds
for u, v being Element of V ex y being Element of V st
( not y is zero & 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 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

proof end;

theorem :: ANPROJ_1:17

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 y is zero & 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:18

for V being RealLinearSpace
for p, q, r, u, v, w, y 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

proof end;

definition

let V be RealLinearSpace;

func Proportionality_as_EqRel_of V -> Equivalence_Relation of (NonZero V) means :Def3: :: ANPROJ_1:def 3
for x, y being object holds
( [x,y] in it 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 ) ) );

existence
ex b₁ being Equivalence_Relation of (NonZero V) st
for x, y being object holds
( [x,y] in b₁ 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 ) ) )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of (NonZero V) st ( for x, y being object holds
( [x,y] in b₁ 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 object holds
( [x,y] in b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Proportionality_as_EqRel_of ANPROJ_1:def 3 :
for V being RealLinearSpace
for b₂ being Equivalence_Relation of (NonZero V) holds
( b₂ = Proportionality_as_EqRel_of V iff for x, y being object holds
( [x,y] in b₂ 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 ) ) ) );

theorem :: ANPROJ_1:19

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

proof end;

theorem Th20: :: ANPROJ_1:20

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

proof end;

definition

let V be RealLinearSpace;
let v be Element of V;

func Dir v -> Subset of (NonZero V) equals :: ANPROJ_1:def 4
Class ((Proportionality_as_EqRel_of V),v);

correctness
coherence
Class ((Proportionality_as_EqRel_of V),v) is Subset of (NonZero V);
;

end;

:: deftheorem defines Dir ANPROJ_1:def 4 :
for V being RealLinearSpace
for v being Element of V holds Dir v = Class ((Proportionality_as_EqRel_of V),v);

definition

let V be RealLinearSpace;

func ProjectivePoints V -> set means :Def5: :: ANPROJ_1:def 5
ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & it = Y );

correctness
existence
ex b₁ being set ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b₁ = Y );
uniqueness
for b₁, b₂ being set st ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b₁ = Y ) & ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b₂ = Y ) holds
b₁ = b₂;
;

end;

:: deftheorem Def5 defines ProjectivePoints ANPROJ_1:def 5 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = ProjectivePoints V iff ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b₂ = Y ) );

registration

cluster non empty non trivial V81() V82() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() for RLSStruct ;

existence
ex b₁ being RealLinearSpace st
( b₁ is strict & not b₁ is trivial )

proof end;

end;

registration

let V be non trivial RealLinearSpace;

cluster ProjectivePoints V -> non empty ;

coherence
not ProjectivePoints V is empty

proof end;

end;

theorem Th21: :: ANPROJ_1:21

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

proof end;

theorem Th22: :: ANPROJ_1:22

for V being non trivial RealLinearSpace
for p, q being Element of V st not p is zero & not q is zero 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 :Def6: :: ANPROJ_1:def 6
for x, y, z being object 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 b₁ being Relation3 of ProjectivePoints V st
for x, y, z being object holds
( [x,y,z] in b₁ 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 ) )

proof end;

uniqueness
for b₁, b₂ being Relation3 of ProjectivePoints V st ( for x, y, z being object holds
( [x,y,z] in b₁ 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 object holds
( [x,y,z] in b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ProjectiveCollinearity ANPROJ_1:def 6 :
for V being non trivial RealLinearSpace
for b₂ being Relation3 of ProjectivePoints V holds
( b₂ = ProjectiveCollinearity V iff for x, y, z being object holds
( [x,y,z] in b₂ 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 ) ) );

definition

let V be non trivial RealLinearSpace;

func ProjectiveSpace V -> strict CollStr equals :: ANPROJ_1:def 7
CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);

correctness
coherence
CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #) is strict CollStr ;
;

end;

:: deftheorem defines ProjectiveSpace ANPROJ_1:def 7 :
for V being non trivial RealLinearSpace holds ProjectiveSpace V = CollStr(# (ProjectivePoints V),(ProjectiveCollinearity V) #);

registration

let V be non trivial RealLinearSpace;

cluster ProjectiveSpace V -> non empty strict ;

coherence
not ProjectiveSpace V is empty ;

end;

theorem :: ANPROJ_1:23

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

theorem :: ANPROJ_1:24

for x, y, z being object
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 & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) by Def6;

theorem :: ANPROJ_1:25

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

proof end;

theorem :: ANPROJ_1:26

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

proof end;