:: 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 b1 being Equivalence_Relation of (NonZero V) st
for x, y being object 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 ) ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of (NonZero V) st ( for x, y being object 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 object 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
proof end;
end;

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

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 b1 being set ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b1 = Y );
uniqueness
for b1, b2 being set st ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b1 = Y ) & ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b2 = Y ) holds
b1 = b2;
;
end;

:: deftheorem Def5 defines ProjectivePoints ANPROJ_1:def 5 :
for V being RealLinearSpace
for b2 being set holds
( b2 = ProjectivePoints V iff ex Y being Subset-Family of (NonZero V) st
( Y = Class (Proportionality_as_EqRel_of V) & b2 = 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 b1 being RealLinearSpace st
( b1 is strict & not b1 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 b1 being Relation3 of ProjectivePoints V st
for x, y, z being object 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 ) )
proof end;
uniqueness
for b1, b2 being Relation3 of ProjectivePoints V st ( for x, y, z being object 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 object 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
proof end;
end;

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

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;