:: A Construction of Analytical Projective Space :: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski :: :: Received June 15, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let V be RealLinearSpace; let p, q be Element of V; pred are_Prop p,q means :Def1: :: 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 ) proofend; 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 Def1 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 ) ) proofend; theorem Th2: :: ANPROJ_1:2 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 proofend; 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 ) proofend; definition let V be RealLinearSpace; let u, v, w be Element of V; predu,v,w are_LinDep means :Def2: :: 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 Def2 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, 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 proofend; 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 ) proofend; 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 proofend; 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) proofend; theorem Th6: :: ANPROJ_1:6 for V being RealLinearSpace for v, w, u 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) ) proofend; 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) proofend; 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) proofend; 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)) proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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) proofend; theorem :: ANPROJ_1:15 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 ) proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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) proofend; theorem :: ANPROJ_1:18 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 proofend; 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 set 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 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 ) ) ) proofend; 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 proofend; 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 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 ) ) ) ); theorem :: ANPROJ_1:19 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 ) proofend; 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 ) ) proofend; 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 V79() V80() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V112() for RLSStruct ; existence ex b1 being RealLinearSpace st ( b1 is strict & not b1 is trivial ) proofend; end; registration let V be non trivial RealLinearSpace; cluster ProjectivePoints V -> non empty ; coherence not ProjectivePoints V is empty proofend; 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 proofend; 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 ) proofend; 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 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 ) ) proofend; 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 proofend; 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 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 ) ) ); 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 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 & 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 ) proofend; theorem :: ANPROJ_1:26 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 ( not u is zero & x = Dir u ) ) proofend;