:: Analytical Metric Affine Spaces and Planes :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received August 10, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for V being RealLinearSpace for v1, w, y, v2 being VECTOR of V for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds ( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) ) proofend; Lm2: for V being RealLinearSpace for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V proofend; Lm3: for V being RealLinearSpace for v, w, y being VECTOR of V for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds a * v = ((a * b1) * w) + ((a * b2) * y) proofend; definition let V be RealLinearSpace; let w, y be VECTOR of V; pred Gen w,y means :Def1: :: ANALMETR:def 1 ( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds ( a1 = 0 & a2 = 0 ) ) ); end; :: deftheorem Def1 defines Gen ANALMETR:def_1_:_ for V being RealLinearSpace for w, y being VECTOR of V holds ( Gen w,y iff ( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds ( a1 = 0 & a2 = 0 ) ) ) ); definition let V be RealLinearSpace; let u, v, w, y be VECTOR of V; predu,v are_Ort_wrt w,y means :Def2: :: ANALMETR:def 2 ex a1, a2, b1, b2 being Real st ( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ); end; :: deftheorem Def2 defines are_Ort_wrt ANALMETR:def_2_:_ for V being RealLinearSpace for u, v, w, y being VECTOR of V holds ( u,v are_Ort_wrt w,y iff ex a1, a2, b1, b2 being Real st ( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ) ); Lm4: for V being RealLinearSpace for w, y being VECTOR of V for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds ( a1 = b1 & a2 = b2 ) proofend; theorem Th1: :: ANALMETR:1 for V being RealLinearSpace for u, v, w, y being VECTOR of V st Gen w,y holds ( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds (a1 * b1) + (a2 * b2) = 0 ) proofend; Lm5: for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds ( w <> 0. V & y <> 0. V ) proofend; theorem :: ANALMETR:2 for V being RealLinearSpace for w, y being VECTOR of V holds w,y are_Ort_wrt w,y proofend; theorem Th3: :: ANALMETR:3 ex V being RealLinearSpace ex w, y being VECTOR of V st Gen w,y proofend; theorem Th4: :: ANALMETR:4 for V being RealLinearSpace for u, v, w, y being VECTOR of V st u,v are_Ort_wrt w,y holds v,u are_Ort_wrt w,y proofend; theorem Th5: :: ANALMETR:5 for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds for u, v being VECTOR of V holds ( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y ) proofend; theorem Th6: :: ANALMETR:6 for V being RealLinearSpace for u, v, w, y being VECTOR of V for a, b being Real st u,v are_Ort_wrt w,y holds a * u,b * v are_Ort_wrt w,y proofend; theorem Th7: :: ANALMETR:7 for V being RealLinearSpace for u, v, w, y being VECTOR of V for a, b being Real st u,v are_Ort_wrt w,y holds ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) proofend; theorem Th8: :: ANALMETR:8 for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds for u being VECTOR of V ex v being VECTOR of V st ( u,v are_Ort_wrt w,y & v <> 0. V ) proofend; theorem Th9: :: ANALMETR:9 for V being RealLinearSpace for w, y, v, u1, u2 being VECTOR of V st Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V holds ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) proofend; theorem Th10: :: ANALMETR:10 for V being RealLinearSpace for w, y, u, v1, v2 being VECTOR of V st Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y holds ( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y ) proofend; theorem Th11: :: ANALMETR:11 for V being RealLinearSpace for w, y, u being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds u = 0. V proofend; theorem Th12: :: ANALMETR:12 for V being RealLinearSpace for w, y, u, u1, u2 being VECTOR of V st Gen w,y & u,u1 - u2 are_Ort_wrt w,y & u1,u2 - u are_Ort_wrt w,y holds u2,u - u1 are_Ort_wrt w,y proofend; theorem Th13: :: ANALMETR:13 for V being RealLinearSpace for w, y, u, v being VECTOR of V st Gen w,y & u <> 0. V holds ex a being Real st v - (a * u),u are_Ort_wrt w,y proofend; theorem Th14: :: ANALMETR:14 for V being RealLinearSpace for u, v, u1, v1 being VECTOR of V holds ( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) proofend; theorem Th15: :: ANALMETR:15 for V being RealLinearSpace for u, v, u1, v1 being VECTOR of V holds ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) proofend; definition let V be RealLinearSpace; let u, u1, v, v1, w, y be VECTOR of V; predu,u1,v,v1 are_Ort_wrt w,y means :Def3: :: ANALMETR:def 3 u1 - u,v1 - v are_Ort_wrt w,y; end; :: deftheorem Def3 defines are_Ort_wrt ANALMETR:def_3_:_ for V being RealLinearSpace for u, u1, v, v1, w, y being VECTOR of V holds ( u,u1,v,v1 are_Ort_wrt w,y iff u1 - u,v1 - v are_Ort_wrt w,y ); definition let V be RealLinearSpace; let w, y be VECTOR of V; func Orthogonality (V,w,y) -> Relation of [: the carrier of V, the carrier of V:] means :Def4: :: ANALMETR:def 4 for x, z being set holds ( [x,z] in it iff ex u, u1, v, v1 being VECTOR of V st ( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ); existence ex b1 being Relation of [: the carrier of V, the carrier of V:] st for x, z being set holds ( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V st ( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) proofend; uniqueness for b1, b2 being Relation of [: the carrier of V, the carrier of V:] st ( for x, z being set holds ( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V st ( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) & ( for x, z being set holds ( [x,z] in b2 iff ex u, u1, v, v1 being VECTOR of V st ( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines Orthogonality ANALMETR:def_4_:_ for V being RealLinearSpace for w, y being VECTOR of V for b4 being Relation of [: the carrier of V, the carrier of V:] holds ( b4 = Orthogonality (V,w,y) iff for x, z being set holds ( [x,z] in b4 iff ex u, u1, v, v1 being VECTOR of V st ( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ); theorem Th16: :: ANALMETR:16 for V being RealLinearSpace holds the carrier of (Lambda (OASpace V)) = the carrier of V proofend; theorem Th17: :: ANALMETR:17 for V being RealLinearSpace holds the CONGR of (Lambda (OASpace V)) = lambda (DirPar V) proofend; theorem :: ANALMETR:18 for V being RealLinearSpace for u, v, u1, v1 being VECTOR of V for p, q, p1, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds ( p,q // p1,q1 iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) proofend; definition attrc1 is strict ; struct ParOrtStr -> AffinStruct ; aggrParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ; sel orthogonality c1 -> Relation of [: the carrier of c1, the carrier of c1:]; end; registration cluster non empty for ParOrtStr ; existence not for b1 being ParOrtStr holds b1 is empty proofend; end; definition let POS be non empty ParOrtStr ; let a, b, c, d be Element of POS; preda,b _|_ c,d means :Def5: :: ANALMETR:def 5 [[a,b],[c,d]] in the orthogonality of POS; end; :: deftheorem Def5 defines _|_ ANALMETR:def_5_:_ for POS being non empty ParOrtStr for a, b, c, d being Element of POS holds ( a,b _|_ c,d iff [[a,b],[c,d]] in the orthogonality of POS ); definition let V be RealLinearSpace; let w, y be VECTOR of V; func AMSpace (V,w,y) -> strict ParOrtStr equals :: ANALMETR:def 6 ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #); correctness coherence ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #) is strict ParOrtStr ; ; end; :: deftheorem defines AMSpace ANALMETR:def_6_:_ for V being RealLinearSpace for w, y being VECTOR of V holds AMSpace (V,w,y) = ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #); registration let V be RealLinearSpace; let w, y be VECTOR of V; cluster AMSpace (V,w,y) -> non empty strict ; coherence not AMSpace (V,w,y) is empty ; end; theorem :: ANALMETR:19 for V being RealLinearSpace for w, y being VECTOR of V holds ( the carrier of (AMSpace (V,w,y)) = the carrier of V & the CONGR of (AMSpace (V,w,y)) = lambda (DirPar V) & the orthogonality of (AMSpace (V,w,y)) = Orthogonality (V,w,y) ) ; definition let POS be non empty ParOrtStr ; func Af POS -> strict AffinStruct equals :: ANALMETR:def 7 AffinStruct(# the carrier of POS, the CONGR of POS #); correctness coherence AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct ; ; end; :: deftheorem defines Af ANALMETR:def_7_:_ for POS being non empty ParOrtStr holds Af POS = AffinStruct(# the carrier of POS, the CONGR of POS #); registration let POS be non empty ParOrtStr ; cluster Af POS -> non empty strict ; coherence not Af POS is empty ; end; theorem Th20: :: ANALMETR:20 for V being RealLinearSpace for w, y being VECTOR of V holds Af (AMSpace (V,w,y)) = Lambda (OASpace V) proofend; theorem Th21: :: ANALMETR:21 for V being RealLinearSpace for u, u1, v, v1, w, y being VECTOR of V for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p = u & p1 = u1 & q = v & q1 = v1 holds ( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y ) proofend; theorem Th22: :: ANALMETR:22 for V being RealLinearSpace for w, y, u, v, u1, v1 being VECTOR of V for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p = u & q = v & p1 = u1 & q1 = v1 holds ( p,q // p1,q1 iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) proofend; theorem Th23: :: ANALMETR:23 for V being RealLinearSpace for w, y being VECTOR of V for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds p1,q1 _|_ p,q proofend; theorem Th24: :: ANALMETR:24 for V being RealLinearSpace for w, y being VECTOR of V for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds p,q _|_ q1,p1 proofend; theorem Th25: :: ANALMETR:25 for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds for p, q, r being Element of (AMSpace (V,w,y)) holds p,q _|_ r,r proofend; theorem Th26: :: ANALMETR:26 for V being RealLinearSpace for w, y being VECTOR of V for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 holds q,q1 _|_ r,r1 proofend; theorem Th27: :: ANALMETR:27 for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds for p, q, r being Element of (AMSpace (V,w,y)) ex r1 being Element of (AMSpace (V,w,y)) st ( p,q _|_ r,r1 & r <> r1 ) proofend; theorem Th28: :: ANALMETR:28 for V being RealLinearSpace for w, y being VECTOR of V for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 holds q,q1 // r,r1 proofend; theorem Th29: :: ANALMETR:29 for V being RealLinearSpace for w, y being VECTOR of V for p, q, r, r1, r2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 holds p,q _|_ r1,r2 proofend; theorem Th30: :: ANALMETR:30 for V being RealLinearSpace for w, y being VECTOR of V for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds p = q proofend; theorem :: ANALMETR:31 for V being RealLinearSpace for w, y being VECTOR of V for p, q, p1, p2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds p2,q _|_ p,p1 proofend; theorem Th32: :: ANALMETR:32 for V being RealLinearSpace for w, y being VECTOR of V for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st ( p,p1 // p,q1 & p,p1 _|_ q1,q ) proofend; consider V0 being RealLinearSpace such that Lm6: ex w, y being VECTOR of V0 st Gen w,y by Th3; consider w0, y0 being VECTOR of V0 such that Lm7: Gen w0,y0 by Lm6; Lm8: now__::_thesis:_(_AffinStruct(#_the_carrier_of_(AMSpace_(V0,w0,y0)),_the_CONGR_of_(AMSpace_(V0,w0,y0))_#)_is_AffinSpace_&_(_for_a,_b,_c,_d,_p,_q,_r,_s_being_Element_of_(AMSpace_(V0,w0,y0))_holds_ (_(_a,b__|__a,b_implies_a_=_b_)_&_a,b__|__c,c_&_(_a,b__|__c,d_implies_(_a,b__|__d,c_&_c,d__|__a,b_)_)_&_(_a,b__|__p,q_&_a,b_//_r,s_&_not_p,q__|__r,s_implies_a_=_b_)_&_(_a,b__|__p,q_&_a,b__|__p,s_implies_a,b__|__q,s_)_)_)_&_(_for_a,_b,_c_being_Element_of_(AMSpace_(V0,w0,y0))_st_a_<>_b_holds_ ex_x_being_Element_of_(AMSpace_(V0,w0,y0))_st_ (_a,b_//_a,x_&_a,b__|__x,c_)_)_&_(_for_a,_b,_c_being_Element_of_(AMSpace_(V0,w0,y0))_ex_x_being_Element_of_(AMSpace_(V0,w0,y0))_st_ (_a,b__|__c,x_&_c_<>_x_)_)_) set X = AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #); AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Af (AMSpace (V0,w0,y0)) ; then A1: AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Lambda (OASpace V0) by Th20; for a, b being Real st (a * w0) + (b * y0) = 0. V0 holds ( a = 0 & b = 0 ) by Def1, Lm7; then OASpace V0 is OAffinSpace by ANALOAF:26; hence ( AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V0,w0,y0)) holds ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of (AMSpace (V0,w0,y0)) st a <> b holds ex x being Element of (AMSpace (V0,w0,y0)) st ( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of (AMSpace (V0,w0,y0)) ex x being Element of (AMSpace (V0,w0,y0)) st ( a,b _|_ c,x & c <> x ) ) ) by A1, Lm7, Th23, Th24, Th25, Th26, Th27, Th29, Th30, Th32, DIRAF:41; ::_thesis: verum end; definition let IT be non empty ParOrtStr ; attrIT is OrtAfSp-like means :Def8: :: ANALMETR:def 8 ( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of IT holds ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of IT st a <> b holds ex x being Element of IT st ( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of IT ex x being Element of IT st ( a,b _|_ c,x & c <> x ) ) ); end; :: deftheorem Def8 defines OrtAfSp-like ANALMETR:def_8_:_ for IT being non empty ParOrtStr holds ( IT is OrtAfSp-like iff ( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of IT holds ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of IT st a <> b holds ex x being Element of IT st ( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of IT ex x being Element of IT st ( a,b _|_ c,x & c <> x ) ) ) ); registration cluster non empty strict OrtAfSp-like for ParOrtStr ; existence ex b1 being non empty ParOrtStr st ( b1 is strict & b1 is OrtAfSp-like ) proofend; end; definition mode OrtAfSp is non empty OrtAfSp-like ParOrtStr ; end; theorem :: ANALMETR:33 for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds AMSpace (V,w,y) is OrtAfSp proofend; consider V0 being RealLinearSpace such that Lm9: ex w, y being VECTOR of V0 st Gen w,y by Th3; consider w0, y0 being VECTOR of V0 such that Lm10: Gen w0,y0 by Lm9; Lm11: now__::_thesis:_(_AffinStruct(#_the_carrier_of_(AMSpace_(V0,w0,y0)),_the_CONGR_of_(AMSpace_(V0,w0,y0))_#)_is_AffinPlane_&_(_for_a,_b,_c,_d,_p,_q,_r,_s_being_Element_of_(AMSpace_(V0,w0,y0))_holds_ (_(_a,b__|__a,b_implies_a_=_b_)_&_a,b__|__c,c_&_(_a,b__|__c,d_implies_(_a,b__|__d,c_&_c,d__|__a,b_)_)_&_(_a,b__|__p,q_&_a,b_//_r,s_&_not_p,q__|__r,s_implies_a_=_b_)_&_(_a,b__|__p,q_&_a,b__|__r,s_&_not_p,q_//_r,s_implies_a_=_b_)_)_)_&_(_for_a,_b,_c_being_Element_of_(AMSpace_(V0,w0,y0))_ex_x_being_Element_of_(AMSpace_(V0,w0,y0))_st_ (_a,b__|__c,x_&_c_<>_x_)_)_) set X = AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #); AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Af (AMSpace (V0,w0,y0)) ; then A1: AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Lambda (OASpace V0) by Th20; ( ( for a, b being Real st (a * w0) + (b * y0) = 0. V0 holds ( a = 0 & b = 0 ) ) & ( for w1 being VECTOR of V0 ex a, b being Real st w1 = (a * w0) + (b * y0) ) ) by Def1, Lm10; then OASpace V0 is OAffinPlane by ANALOAF:28; hence ( AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V0,w0,y0)) holds ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of (AMSpace (V0,w0,y0)) ex x being Element of (AMSpace (V0,w0,y0)) st ( a,b _|_ c,x & c <> x ) ) ) by A1, Lm10, Th23, Th24, Th25, Th26, Th27, Th28, Th30, DIRAF:45; ::_thesis: verum end; definition let IT be non empty ParOrtStr ; attrIT is OrtAfPl-like means :Def9: :: ANALMETR:def 9 ( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of IT holds ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of IT ex x being Element of IT st ( a,b _|_ c,x & c <> x ) ) ); end; :: deftheorem Def9 defines OrtAfPl-like ANALMETR:def_9_:_ for IT being non empty ParOrtStr holds ( IT is OrtAfPl-like iff ( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of IT holds ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of IT ex x being Element of IT st ( a,b _|_ c,x & c <> x ) ) ) ); registration cluster non empty strict OrtAfPl-like for ParOrtStr ; existence ex b1 being non empty ParOrtStr st ( b1 is strict & b1 is OrtAfPl-like ) proofend; end; definition mode OrtAfPl is non empty OrtAfPl-like ParOrtStr ; end; theorem :: ANALMETR:34 for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds AMSpace (V,w,y) is OrtAfPl proofend; theorem :: ANALMETR:35 for POS being non empty ParOrtStr for x being set holds ( x is Element of POS iff x is Element of (Af POS) ) ; theorem Th36: :: ANALMETR:36 for POS being non empty ParOrtStr for a, b, c, d being Element of POS for a9, b9, c9, d9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 & d = d9 holds ( a,b // c,d iff a9,b9 // c9,d9 ) proofend; registration let POS be OrtAfSp; cluster Af POS -> non trivial strict AffinSpace-like ; correctness coherence ( Af POS is AffinSpace-like & not Af POS is trivial ); by Def8; end; registration let POS be OrtAfPl; cluster Af POS -> non trivial strict AffinSpace-like 2-dimensional ; correctness coherence ( Af POS is 2-dimensional & Af POS is AffinSpace-like & not Af POS is trivial ); by Def9; end; theorem Th37: :: ANALMETR:37 for POS being OrtAfPl holds POS is OrtAfSp proofend; registration cluster non empty OrtAfPl-like -> non empty OrtAfSp-like for ParOrtStr ; coherence for b1 being non empty ParOrtStr st b1 is OrtAfPl-like holds b1 is OrtAfSp-like by Th37; end; theorem :: ANALMETR:38 for POS being OrtAfSp st Af POS is AffinPlane holds POS is OrtAfPl proofend; theorem :: ANALMETR:39 for POS being non empty ParOrtStr holds ( POS is OrtAfPl-like iff ( ex a, b being Element of POS st a <> b & ( for a, b, c, d, p, q, r, s being Element of POS holds ( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st ( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st ( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st ( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st ( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st ( a,b // a,x & c,d // c,x ) ) ) ) ) ) proofend; definition let POS be non empty ParOrtStr ; let a, b, c be Element of POS; pred LIN a,b,c means :Def10: :: ANALMETR:def 10 a,b // a,c; end; :: deftheorem Def10 defines LIN ANALMETR:def_10_:_ for POS being non empty ParOrtStr for a, b, c being Element of POS holds ( LIN a,b,c iff a,b // a,c ); definition let POS be non empty ParOrtStr ; let a, b be Element of POS; func Line (a,b) -> Subset of POS means :Def11: :: ANALMETR:def 11 for x being Element of POS holds ( x in it iff LIN a,b,x ); existence ex b1 being Subset of POS st for x being Element of POS holds ( x in b1 iff LIN a,b,x ) proofend; uniqueness for b1, b2 being Subset of POS st ( for x being Element of POS holds ( x in b1 iff LIN a,b,x ) ) & ( for x being Element of POS holds ( x in b2 iff LIN a,b,x ) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines Line ANALMETR:def_11_:_ for POS being non empty ParOrtStr for a, b being Element of POS for b4 being Subset of POS holds ( b4 = Line (a,b) iff for x being Element of POS holds ( x in b4 iff LIN a,b,x ) ); definition let POS be non empty ParOrtStr ; let A be Subset of POS; attrA is being_line means :Def12: :: ANALMETR:def 12 ex a, b being Element of POS st ( a <> b & A = Line (a,b) ); end; :: deftheorem Def12 defines being_line ANALMETR:def_12_:_ for POS being non empty ParOrtStr for A being Subset of POS holds ( A is being_line iff ex a, b being Element of POS st ( a <> b & A = Line (a,b) ) ); theorem Th40: :: ANALMETR:40 for POS being OrtAfSp for a, b, c being Element of POS for a9, b9, c9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 holds ( LIN a,b,c iff LIN a9,b9,c9 ) proofend; theorem Th41: :: ANALMETR:41 for POS being OrtAfSp for a, b being Element of POS for a9, b9 being Element of (Af POS) st a = a9 & b = b9 holds Line (a,b) = Line (a9,b9) proofend; theorem :: ANALMETR:42 for POS being non empty ParOrtStr for X being set holds ( X is Subset of POS iff X is Subset of (Af POS) ) ; theorem Th43: :: ANALMETR:43 for POS being OrtAfSp for X being Subset of POS for Y being Subset of (Af POS) st X = Y holds ( X is being_line iff Y is being_line ) proofend; definition let POS be non empty ParOrtStr ; let a, b be Element of POS; let K be Subset of POS; preda,b _|_ K means :Def13: :: ANALMETR:def 13 ex p, q being Element of POS st ( p <> q & K = Line (p,q) & a,b _|_ p,q ); end; :: deftheorem Def13 defines _|_ ANALMETR:def_13_:_ for POS being non empty ParOrtStr for a, b being Element of POS for K being Subset of POS holds ( a,b _|_ K iff ex p, q being Element of POS st ( p <> q & K = Line (p,q) & a,b _|_ p,q ) ); definition let POS be non empty ParOrtStr ; let K, M be Subset of POS; predK _|_ M means :Def14: :: ANALMETR:def 14 ex p, q being Element of POS st ( p <> q & K = Line (p,q) & p,q _|_ M ); end; :: deftheorem Def14 defines _|_ ANALMETR:def_14_:_ for POS being non empty ParOrtStr for K, M being Subset of POS holds ( K _|_ M iff ex p, q being Element of POS st ( p <> q & K = Line (p,q) & p,q _|_ M ) ); definition let POS be non empty ParOrtStr ; let K, M be Subset of POS; predK // M means :Def15: :: ANALMETR:def 15 ex a, b, c, d being Element of POS st ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b // c,d ); end; :: deftheorem Def15 defines // ANALMETR:def_15_:_ for POS being non empty ParOrtStr for K, M being Subset of POS holds ( K // M iff ex a, b, c, d being Element of POS st ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b // c,d ) ); theorem Th44: :: ANALMETR:44 for POS being non empty ParOrtStr for a, b being Element of POS for K, M being Subset of POS holds ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) ) proofend; theorem Th45: :: ANALMETR:45 for POS being non empty ParOrtStr for K, M being Subset of POS holds ( K _|_ M iff ex a, b, c, d being Element of POS st ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) ) proofend; theorem Th46: :: ANALMETR:46 for POS being OrtAfSp for M, N being Subset of POS for M9, N9 being Subset of (Af POS) st M = M9 & N = N9 holds ( M // N iff M9 // N9 ) proofend; theorem :: ANALMETR:47 for POS being OrtAfSp for K being Subset of POS for a being Element of POS st K is being_line holds a,a _|_ K proofend; theorem :: ANALMETR:48 for POS being OrtAfSp for K being Subset of POS for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds c,d _|_ K proofend; theorem :: ANALMETR:49 for POS being OrtAfSp for K being Subset of POS for a, b being Element of POS st a,b _|_ K holds b,a _|_ K proofend; definition let POS be OrtAfSp; let K, M be Subset of POS; :: original:// redefine predK // M; symmetry for K, M being Subset of POS st (POS,b1,b2) holds (POS,b2,b1) proofend; end; theorem Th50: :: ANALMETR:50 for POS being OrtAfSp for K, M being Subset of POS for r, s being Element of POS st r,s _|_ K & K // M holds r,s _|_ M proofend; theorem Th51: :: ANALMETR:51 for POS being OrtAfSp for K being Subset of POS for a, b being Element of POS st a in K & b in K & a,b _|_ K holds a = b proofend; definition let POS be OrtAfSp; let K, M be Subset of POS; :: original:_|_ redefine predK _|_ M; irreflexivity for K being Subset of POS holds (POS,b1,b1) proofend; symmetry for K, M being Subset of POS st (POS,b1,b2) holds (POS,b2,b1) proofend; end; theorem Th52: :: ANALMETR:52 for POS being OrtAfSp for K, M, N being Subset of POS st K _|_ M & K // N holds N _|_ M proofend; theorem :: ANALMETR:53 for POS being OrtAfSp for K being Subset of POS for a, b, c, d being Element of POS st a in K & b in K & c,d _|_ K holds ( c,d _|_ a,b & a,b _|_ c,d ) proofend; theorem Th54: :: ANALMETR:54 for POS being OrtAfSp for K being Subset of POS for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds K = Line (a,b) proofend; theorem :: ANALMETR:55 for POS being OrtAfSp for K being Subset of POS for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds c,d _|_ K proofend; theorem Th56: :: ANALMETR:56 for POS being OrtAfSp for M, N being Subset of POS for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds a,b _|_ c,d proofend; theorem :: ANALMETR:57 for POS being OrtAfSp for M, N, K, A being Subset of POS for p, a, b being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds A _|_ K proofend; theorem Th58: :: ANALMETR:58 for POS being OrtAfSp for b, c, a being Element of POS holds ( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c ) proofend; theorem Th59: :: ANALMETR:59 for POS being OrtAfSp for a, b, c, d being Element of POS st a,b // c,d holds ( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a ) proofend; theorem :: ANALMETR:60 for POS being OrtAfSp for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) holds a,b // c,d proofend; theorem Th61: :: ANALMETR:61 for POS being OrtAfSp for a, b, c, d being Element of POS st a,b _|_ c,d holds ( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a ) proofend; theorem Th62: :: ANALMETR:62 for POS being OrtAfSp for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) holds a,b _|_ c,d proofend; theorem Th63: :: ANALMETR:63 for POS being OrtAfPl for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q _|_ a,b & p,q _|_ c,d ) or ( p,q _|_ a,b & c,d _|_ p,q ) or ( a,b _|_ p,q & c,d _|_ p,q ) or ( a,b _|_ p,q & p,q _|_ c,d ) ) holds a,b // c,d proofend; theorem :: ANALMETR:64 for POS being OrtAfPl for M, N being Subset of POS for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds M // N proofend; theorem :: ANALMETR:65 for POS being OrtAfPl for M, K, N being Subset of POS st M _|_ K & N _|_ K holds M // N proofend; theorem Th66: :: ANALMETR:66 for POS being OrtAfPl for M, N being Subset of POS st M _|_ N holds ex p being Element of POS st ( p in M & p in N ) proofend; theorem Th67: :: ANALMETR:67 for POS being OrtAfPl for a, b, c, d being Element of POS st a,b _|_ c,d holds ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) proofend; theorem :: ANALMETR:68 for POS being OrtAfPl for K being Subset of POS for a, b being Element of POS st a,b _|_ K holds ex p being Element of POS st ( LIN a,b,p & p in K ) proofend; theorem Th69: :: ANALMETR:69 for POS being OrtAfPl for a, p, q being Element of POS ex x being Element of POS st ( a,x _|_ p,q & LIN p,q,x ) proofend; theorem :: ANALMETR:70 for POS being OrtAfPl for K being Subset of POS for a being Element of POS st K is being_line holds ex x being Element of POS st ( a,x _|_ K & x in K ) proofend;