:: ANALMETR semantic presentation 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) ) proof let V be RealLinearSpace; ::_thesis: 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) ) let v1, w, y, v2 be VECTOR of V; ::_thesis: 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) ) let b1, b2, c1, c2 be Real; ::_thesis: ( v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) implies ( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) ) ) assume A1: ( v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) ) ; ::_thesis: ( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) ) hence v1 + v2 = (((b1 * w) + (b2 * y)) + (c1 * w)) + (c2 * y) by RLVECT_1:def_3 .= (((b1 * w) + (c1 * w)) + (b2 * y)) + (c2 * y) by RLVECT_1:def_3 .= (((b1 + c1) * w) + (b2 * y)) + (c2 * y) by RLVECT_1:def_6 .= ((b1 + c1) * w) + ((b2 * y) + (c2 * y)) by RLVECT_1:def_3 .= ((b1 + c1) * w) + ((b2 + c2) * y) by RLVECT_1:def_6 ; ::_thesis: v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) thus v1 - v2 = ((b1 * w) + (b2 * y)) + ((- (c1 * w)) + (- (c2 * y))) by A1, RLVECT_1:31 .= ((b1 * w) + (b2 * y)) + ((c1 * (- w)) + (- (c2 * y))) by RLVECT_1:25 .= ((b1 * w) + (b2 * y)) + ((c1 * (- w)) + (c2 * (- y))) by RLVECT_1:25 .= ((b1 * w) + (b2 * y)) + (((- c1) * w) + (c2 * (- y))) by RLVECT_1:24 .= ((b1 * w) + (b2 * y)) + (((- c1) * w) + ((- c2) * y)) by RLVECT_1:24 .= (((b1 * w) + (b2 * y)) + ((- c1) * w)) + ((- c2) * y) by RLVECT_1:def_3 .= (((b1 * w) + ((- c1) * w)) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def_3 .= (((b1 + (- c1)) * w) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def_6 .= ((b1 + (- c1)) * w) + ((b2 * y) + ((- c2) * y)) by RLVECT_1:def_3 .= ((b1 - c1) * w) + ((b2 + (- c2)) * y) by RLVECT_1:def_6 .= ((b1 - c1) * w) + ((b2 - c2) * y) ; ::_thesis: verum end; Lm2: for V being RealLinearSpace for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V proof let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V let w, y be VECTOR of V; ::_thesis: (0 * w) + (0 * y) = 0. V thus (0 * w) + (0 * y) = (0. V) + (0 * y) by RLVECT_1:10 .= (0. V) + (0. V) by RLVECT_1:10 .= 0. V by RLVECT_1:4 ; ::_thesis: verum end; 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) proof let V be RealLinearSpace; ::_thesis: 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) let v, w, y be VECTOR of V; ::_thesis: for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds a * v = ((a * b1) * w) + ((a * b2) * y) let b1, b2, a be Real; ::_thesis: ( v = (b1 * w) + (b2 * y) implies a * v = ((a * b1) * w) + ((a * b2) * y) ) assume v = (b1 * w) + (b2 * y) ; ::_thesis: a * v = ((a * b1) * w) + ((a * b2) * y) hence a * v = (a * (b1 * w)) + (a * (b2 * y)) by RLVECT_1:def_5 .= ((a * b1) * w) + (a * (b2 * y)) by RLVECT_1:def_7 .= ((a * b1) * w) + ((a * b2) * y) by RLVECT_1:def_7 ; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let w, y be VECTOR of V; ::_thesis: for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds ( a1 = b1 & a2 = b2 ) let a1, a2, b1, b2 be Real; ::_thesis: ( Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) implies ( a1 = b1 & a2 = b2 ) ) assume that A1: Gen w,y and A2: (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) ; ::_thesis: ( a1 = b1 & a2 = b2 ) 0. V = ((a1 * w) + (a2 * y)) - ((b1 * w) + (b2 * y)) by A2, RLVECT_1:15 .= ((a1 - b1) * w) + ((a2 - b2) * y) by Lm1 ; then ( (- b1) + a1 = 0 & (- b2) + a2 = 0 ) by A1, Def1; hence ( a1 = b1 & a2 = b2 ) ; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let u, v, w, y be VECTOR of V; ::_thesis: ( Gen w,y implies ( 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 ) ) assume A1: Gen w,y ; ::_thesis: ( 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 ) hereby ::_thesis: ( ( for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds (a1 * b1) + (a2 * b2) = 0 ) implies u,v are_Ort_wrt w,y ) assume u,v are_Ort_wrt w,y ; ::_thesis: for a19, a29, b19, b29 being Real st u = (a19 * w) + (a29 * y) & v = (b19 * w) + (b29 * y) holds 0 = (a19 * b19) + (a29 * b29) then consider a1, a2, b1, b2 being Real such that A2: u = (a1 * w) + (a2 * y) and A3: v = (b1 * w) + (b2 * y) and A4: (a1 * b1) + (a2 * b2) = 0 by Def2; let a19, a29, b19, b29 be Real; ::_thesis: ( u = (a19 * w) + (a29 * y) & v = (b19 * w) + (b29 * y) implies 0 = (a19 * b19) + (a29 * b29) ) assume that A5: u = (a19 * w) + (a29 * y) and A6: v = (b19 * w) + (b29 * y) ; ::_thesis: 0 = (a19 * b19) + (a29 * b29) A7: b1 = b19 by A1, A3, A6, Lm4; ( a1 = a19 & a2 = a29 ) by A1, A2, A5, Lm4; hence 0 = (a19 * b19) + (a29 * b29) by A1, A3, A4, A6, A7, Lm4; ::_thesis: verum end; consider a1, a2 being Real such that A8: u = (a1 * w) + (a2 * y) by A1, Def1; consider b1, b2 being Real such that A9: v = (b1 * w) + (b2 * y) by A1, Def1; assume for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds (a1 * b1) + (a2 * b2) = 0 ; ::_thesis: u,v are_Ort_wrt w,y then (a1 * b1) + (a2 * b2) = 0 by A8, A9; hence u,v are_Ort_wrt w,y by A8, A9, Def2; ::_thesis: verum end; Lm5: for V being RealLinearSpace for w, y being VECTOR of V st Gen w,y holds ( w <> 0. V & y <> 0. V ) proof let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds ( w <> 0. V & y <> 0. V ) let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies ( w <> 0. V & y <> 0. V ) ) assume A1: Gen w,y ; ::_thesis: ( w <> 0. V & y <> 0. V ) thus w <> 0. V ::_thesis: y <> 0. V proof assume w = 0. V ; ::_thesis: contradiction then 0. V = 1 * w by RLVECT_1:def_8 .= (1 * w) + (0. V) by RLVECT_1:4 .= (1 * w) + (0 * y) by RLVECT_1:10 ; hence contradiction by A1, Def1; ::_thesis: verum end; thus y <> 0. V ::_thesis: verum proof assume y = 0. V ; ::_thesis: contradiction then 0. V = 1 * y by RLVECT_1:def_8 .= (0. V) + (1 * y) by RLVECT_1:4 .= (0 * w) + (1 * y) by RLVECT_1:10 ; hence contradiction by A1, Def1; ::_thesis: verum end; end; theorem :: ANALMETR:2 for V being RealLinearSpace for w, y being VECTOR of V holds w,y are_Ort_wrt w,y proof let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V holds w,y are_Ort_wrt w,y let w, y be VECTOR of V; ::_thesis: w,y are_Ort_wrt w,y A1: y = (0. V) + y by RLVECT_1:4 .= (0. V) + (1 * y) by RLVECT_1:def_8 .= (0 * w) + (1 * y) by RLVECT_1:10 ; A2: (1 * 0) + (0 * 1) = 0 ; w = w + (0. V) by RLVECT_1:4 .= (1 * w) + (0. V) by RLVECT_1:def_8 .= (1 * w) + (0 * y) by RLVECT_1:10 ; hence w,y are_Ort_wrt w,y by A1, A2, Def2; ::_thesis: verum end; theorem Th3: :: ANALMETR:3 ex V being RealLinearSpace ex w, y being VECTOR of V st Gen w,y proof consider V being RealLinearSpace such that A1: ex u, v being VECTOR of V st ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds ( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23; take V ; ::_thesis: ex w, y being VECTOR of V st Gen w,y consider u, v being VECTOR of V such that A2: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds ( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by A1; take u ; ::_thesis: ex y being VECTOR of V st Gen u,y take v ; ::_thesis: Gen u,v thus Gen u,v by A2, Def1; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let u, v, w, y be VECTOR of V; ::_thesis: ( u,v are_Ort_wrt w,y implies v,u are_Ort_wrt w,y ) assume u,v are_Ort_wrt w,y ; ::_thesis: v,u are_Ort_wrt w,y then ex a1, a2, b1, b2 being Real st ( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ) by Def2; hence v,u are_Ort_wrt w,y by Def2; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for u, v being VECTOR of V holds ( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y ) ) assume A1: Gen w,y ; ::_thesis: for u, v being VECTOR of V holds ( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y ) let u, v be VECTOR of V; ::_thesis: ( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y ) consider a1, a2 being Real such that A2: u = (a1 * w) + (a2 * y) by A1, Def1; consider b1, b2 being Real such that A3: v = (b1 * w) + (b2 * y) by A1, Def1; A4: 0. V = (0. V) + (0. V) by RLVECT_1:4 .= (0 * w) + (0. V) by RLVECT_1:10 .= (0 * w) + (0 * y) by RLVECT_1:10 ; (a1 * 0) + (a2 * 0) = 0 ; hence u, 0. V are_Ort_wrt w,y by A2, A4, Def2; ::_thesis: 0. V,v are_Ort_wrt w,y (0 * b1) + (0 * b2) = 0 ; hence 0. V,v are_Ort_wrt w,y by A3, A4, Def2; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let u, v, w, y be VECTOR of V; ::_thesis: for a, b being Real st u,v are_Ort_wrt w,y holds a * u,b * v are_Ort_wrt w,y let a, b be Real; ::_thesis: ( u,v are_Ort_wrt w,y implies a * u,b * v are_Ort_wrt w,y ) assume u,v are_Ort_wrt w,y ; ::_thesis: a * u,b * v are_Ort_wrt w,y then consider a1, a2, b1, b2 being Real such that A1: u = (a1 * w) + (a2 * y) and A2: v = (b1 * w) + (b2 * y) and A3: (a1 * b1) + (a2 * b2) = 0 by Def2; A4: b * v = (b * (b1 * w)) + (b * (b2 * y)) by A2, RLVECT_1:def_5 .= ((b * b1) * w) + (b * (b2 * y)) by RLVECT_1:def_7 .= ((b * b1) * w) + ((b * b2) * y) by RLVECT_1:def_7 ; A5: ((a * a1) * (b * b1)) + ((a * a2) * (b * b2)) = (b * a) * ((a1 * b1) + (a2 * b2)) .= 0 by A3 ; a * u = (a * (a1 * w)) + (a * (a2 * y)) by A1, RLVECT_1:def_5 .= ((a * a1) * w) + (a * (a2 * y)) by RLVECT_1:def_7 .= ((a * a1) * w) + ((a * a2) * y) by RLVECT_1:def_7 ; hence a * u,b * v are_Ort_wrt w,y by A4, A5, Def2; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let u, v, w, y be VECTOR of V; ::_thesis: 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 ) let a, b be Real; ::_thesis: ( u,v are_Ort_wrt w,y implies ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) ) A1: ( v = 1 * v & u = 1 * u ) by RLVECT_1:def_8; assume u,v are_Ort_wrt w,y ; ::_thesis: ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) hence ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) by A1, Th6; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for u being VECTOR of V ex v being VECTOR of V st ( u,v are_Ort_wrt w,y & v <> 0. V ) ) assume A1: Gen w,y ; ::_thesis: for u being VECTOR of V ex v being VECTOR of V st ( u,v are_Ort_wrt w,y & v <> 0. V ) let u be VECTOR of V; ::_thesis: ex v being VECTOR of V st ( u,v are_Ort_wrt w,y & v <> 0. V ) consider a1, a2 being Real such that A2: u = (a1 * w) + (a2 * y) by A1, Def1; A3: now__::_thesis:_(_u_<>_0._V_implies_ex_v_being_Element_of_the_carrier_of_V_st_ (_u,v_are_Ort_wrt_w,y_&_v_<>_0._V_)_) set v = (a2 * w) + ((- a1) * y); assume A4: u <> 0. V ; ::_thesis: ex v being Element of the carrier of V st ( u,v are_Ort_wrt w,y & v <> 0. V ) take v = (a2 * w) + ((- a1) * y); ::_thesis: ( u,v are_Ort_wrt w,y & v <> 0. V ) (a1 * a2) + (a2 * (- a1)) = 0 ; hence u,v are_Ort_wrt w,y by A2, Def2; ::_thesis: v <> 0. V v <> 0. V proof assume v = 0. V ; ::_thesis: contradiction then ( a2 = 0 & - a1 = 0 ) by A1, Def1; then u = (0 * w) + (0. V) by A2, RLVECT_1:10 .= 0 * w by RLVECT_1:4 .= 0. V by RLVECT_1:10 ; hence contradiction by A4; ::_thesis: verum end; hence v <> 0. V ; ::_thesis: verum end; now__::_thesis:_(_u_=_0._V_implies_ex_v_being_VECTOR_of_V_st_ (_u,v_are_Ort_wrt_w,y_&_v_<>_0._V_)_) assume A5: u = 0. V ; ::_thesis: ex v being VECTOR of V st ( u,v are_Ort_wrt w,y & v <> 0. V ) take v = w; ::_thesis: ( u,v are_Ort_wrt w,y & v <> 0. V ) thus u,v are_Ort_wrt w,y by A1, A5, Th5; ::_thesis: v <> 0. V thus v <> 0. V by A1, Lm5; ::_thesis: verum end; hence ex v being VECTOR of V st ( u,v are_Ort_wrt w,y & v <> 0. V ) by A3; ::_thesis: verum end; 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 ) ) proof let V be RealLinearSpace; ::_thesis: 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 ) ) let w, y, v, u1, u2 be VECTOR of V; ::_thesis: ( Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V implies ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ) assume that A1: Gen w,y and A2: v,u1 are_Ort_wrt w,y and A3: v,u2 are_Ort_wrt w,y and A4: v <> 0. V ; ::_thesis: ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) consider a1, a2, b1, b2 being Real such that A5: v = (a1 * w) + (a2 * y) and A6: u1 = (b1 * w) + (b2 * y) and A7: (a1 * b1) + (a2 * b2) = 0 by A2, Def2; consider a19, a29, c1, c2 being Real such that A8: v = (a19 * w) + (a29 * y) and A9: u2 = (c1 * w) + (c2 * y) and A10: (a19 * c1) + (a29 * c2) = 0 by A3, Def2; A11: a2 = a29 by A1, A5, A8, Lm4; A12: a1 = a19 by A1, A5, A8, Lm4; A13: now__::_thesis:_(_a1_=_0_implies_ex_a,_b_being_Real_st_ (_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_) assume A14: a1 = 0 ; ::_thesis: ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) then A15: a2 <> 0 by A4, A5, Lm2; then c2 = 0 by A10, A12, A11, A14, XCMPLX_1:6; then u2 = (c1 * w) + (0. V) by A9, RLVECT_1:10; then A16: u2 = c1 * w by RLVECT_1:4; b2 = 0 by A7, A14, A15, XCMPLX_1:6; then A17: u1 = (b1 * w) + (0. V) by A6, RLVECT_1:10; then A18: u1 = b1 * w by RLVECT_1:4; A19: now__::_thesis:_(_b1_=_0_implies_ex_a,_b_being_Real_st_ (_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_) assume b1 = 0 ; ::_thesis: ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) then 1 * u1 = 0 * w by A18, RLVECT_1:def_8 .= 0. V by RLVECT_1:10 .= 0 * u2 by RLVECT_1:10 ; hence ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum end; c1 * u1 = c1 * (b1 * w) by A17, RLVECT_1:4 .= (b1 * c1) * w by RLVECT_1:def_7 .= b1 * u2 by A16, RLVECT_1:def_7 ; hence ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A19; ::_thesis: verum end; now__::_thesis:_(_a1_<>_0_implies_ex_a,_b_being_Real_st_ (_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_) A20: c2 * (((- a2) * b2) * (a1 ")) = b2 * (((- a2) * c2) * (a1 ")) ; assume A21: a1 <> 0 ; ::_thesis: ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) A22: b1 = 1 * b1 .= (a1 * (a1 ")) * b1 by A21, XCMPLX_0:def_7 .= (a1 * b1) * (a1 ") .= ((- a2) * b2) * (a1 ") by A7 ; A23: c1 = 1 * c1 .= (a1 * (a1 ")) * c1 by A21, XCMPLX_0:def_7 .= (a1 * c1) * (a1 ") .= ((- a2) * c2) * (a1 ") by A1, A5, A8, A10, A11, Lm4 ; then A24: b2 * u2 = ((b2 * (((- a2) * c2) * (a1 "))) * w) + ((b2 * c2) * y) by A9, Lm3; A25: now__::_thesis:_(_(_c2_<>_0_or_b2_<>_0_)_implies_ex_a,_b_being_Real_st_ (_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_) assume A26: ( c2 <> 0 or b2 <> 0 ) ; ::_thesis: ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) take a = c2; ::_thesis: ex b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) take b = b2; ::_thesis: ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) thus ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A6, A22, A24, A20, A26, Lm3; ::_thesis: verum end; now__::_thesis:_(_b2_=_0_&_c2_=_0_implies_ex_a,_b_being_Real_st_ (_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_) assume ( b2 = 0 & c2 = 0 ) ; ::_thesis: ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) then 1 * u1 = 1 * u2 by A6, A9, A22, A23; hence ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum end; hence ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A25; ::_thesis: verum end; hence ex a, b being Real st ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A13; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let w, y, u, v1, v2 be VECTOR of V; ::_thesis: ( Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y implies ( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y ) ) assume that A1: Gen w,y and A2: u,v1 are_Ort_wrt w,y and A3: u,v2 are_Ort_wrt w,y ; ::_thesis: ( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y ) consider a1, a2, b1, b2 being Real such that A4: u = (a1 * w) + (a2 * y) and A5: v1 = (b1 * w) + (b2 * y) and A6: (a1 * b1) + (a2 * b2) = 0 by A2, Def2; consider a19, a29, c1, c2 being Real such that A7: u = (a19 * w) + (a29 * y) and A8: v2 = (c1 * w) + (c2 * y) and A9: (a19 * c1) + (a29 * c2) = 0 by A3, Def2; A10: ( a1 = a19 & a2 = a29 ) by A1, A4, A7, Lm4; then A11: (a1 * (b1 + c1)) + (a2 * (b2 + c2)) = 0 by A6, A9; A12: (a1 * (b1 - c1)) + (a2 * (b2 - c2)) = 0 by A6, A9, A10; v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) by A5, A8, Lm1; hence u,v1 + v2 are_Ort_wrt w,y by A4, A11, Def2; ::_thesis: u,v1 - v2 are_Ort_wrt w,y v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) by A5, A8, Lm1; hence u,v1 - v2 are_Ort_wrt w,y by A4, A12, Def2; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: for w, y, u being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds u = 0. V let w, y, u be VECTOR of V; ::_thesis: ( Gen w,y & u,u are_Ort_wrt w,y implies u = 0. V ) A1: now__::_thesis:_for_a_being_Real_st_a_<>_0_holds_ 0_<_a_*_a let a be Real; ::_thesis: ( a <> 0 implies 0 < a * a ) assume A2: a <> 0 ; ::_thesis: 0 < a * a ( 0 < a implies 0 < a * a ) by XREAL_1:129; hence 0 < a * a by A2, XREAL_1:130; ::_thesis: verum end; assume that A3: Gen w,y and A4: u,u are_Ort_wrt w,y ; ::_thesis: u = 0. V consider a1, a2, b1, b2 being Real such that A5: u = (a1 * w) + (a2 * y) and A6: u = (b1 * w) + (b2 * y) and A7: (a1 * b1) + (a2 * b2) = 0 by A4, Def2; A8: ( a1 = b1 & a2 = b2 ) by A3, A5, A6, Lm4; A9: a2 = 0 proof assume a2 <> 0 ; ::_thesis: contradiction then 0 < a2 * a2 by A1; hence contradiction by A7, A8, XREAL_1:29, XREAL_1:63; ::_thesis: verum end; a1 = 0 proof assume a1 <> 0 ; ::_thesis: contradiction then 0 < a1 * a1 by A1; hence contradiction by A7, A8, XREAL_1:29, XREAL_1:63; ::_thesis: verum end; hence u = (0 * w) + (0. V) by A5, A9, RLVECT_1:10 .= 0 * w by RLVECT_1:4 .= 0. V by RLVECT_1:10 ; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y, u, u1, u2 be VECTOR of V; ::_thesis: ( Gen w,y & u,u1 - u2 are_Ort_wrt w,y & u1,u2 - u are_Ort_wrt w,y implies u2,u - u1 are_Ort_wrt w,y ) assume that A1: Gen w,y and A2: u,u1 - u2 are_Ort_wrt w,y and A3: u1,u2 - u are_Ort_wrt w,y ; ::_thesis: u2,u - u1 are_Ort_wrt w,y consider a1, a2 being Real such that A4: u = (a1 * w) + (a2 * y) by A1, Def1; consider c1, c2 being Real such that A5: u2 = (c1 * w) + (c2 * y) by A1, Def1; consider b1, b2 being Real such that A6: u1 = (b1 * w) + (b2 * y) by A1, Def1; A7: u - u1 = ((a1 - b1) * w) + ((a2 - b2) * y) by A4, A6, Lm1; u2 - u = ((c1 - a1) * w) + ((c2 - a2) * y) by A4, A5, Lm1; then A8: (b1 * (c1 - a1)) + (b2 * (c2 - a2)) = 0 by A1, A3, A6, Th1; u1 - u2 = ((b1 - c1) * w) + ((b2 - c2) * y) by A6, A5, Lm1; then (a1 * (b1 - c1)) + (a2 * (b2 - c2)) = 0 by A1, A2, A4, Th1; then 0 = (c1 * (a1 - b1)) + (c2 * (a2 - b2)) by A8; hence u2,u - u1 are_Ort_wrt w,y by A5, A7, Def2; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y, u, v be VECTOR of V; ::_thesis: ( Gen w,y & u <> 0. V implies ex a being Real st v - (a * u),u are_Ort_wrt w,y ) assume that A1: Gen w,y and A2: u <> 0. V ; ::_thesis: ex a being Real st v - (a * u),u are_Ort_wrt w,y consider a1, a2 being Real such that A3: u = (a1 * w) + (a2 * y) by A1, Def1; consider b1, b2 being Real such that A4: v = (b1 * w) + (b2 * y) by A1, Def1; set a = ((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) "); (((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u = (((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1) * w) + (((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2) * y) by A3, Lm3; then A5: v - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u) = ((b1 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) * w) + ((b2 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)) * y) by A4, Lm1; A6: ((b1 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) * a1) + ((b2 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)) * a2) = ((a1 * b1) + (a2 * b2)) + ((- 1) * ((a1 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) + (a2 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)))) ; A7: (a1 * a1) + (a2 * a2) <> 0 proof assume (a1 * a1) + (a2 * a2) = 0 ; ::_thesis: contradiction then u,u are_Ort_wrt w,y by A3, Def2; hence contradiction by A1, A2, Th11; ::_thesis: verum end; (- 1) * ((a1 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) + (a2 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2))) = (- 1) * (((b1 * a1) + (b2 * a2)) * ((((a1 * a1) + (a2 * a2)) ") * ((a1 * a1) + (a2 * a2)))) .= (- 1) * (((b1 * a1) + (b2 * a2)) * 1) by A7, XCMPLX_0:def_7 .= - ((a1 * b1) + (a2 * b2)) ; then v - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u),u are_Ort_wrt w,y by A3, A5, A6, Def2; hence ex a being Real st v - (a * u),u are_Ort_wrt w,y ; ::_thesis: verum end; 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 ) ) ) proof let V be RealLinearSpace; ::_thesis: 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 ) ) ) let u, v, u1, v1 be VECTOR of V; ::_thesis: ( ( 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 ) ) ) A1: now__::_thesis:_for_w,_y,_w1,_y1_being_VECTOR_of_V_st_ex_a,_b_being_Real_st_ (_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_a_=_0_&_b_<>_0_)_holds_ w,y_//_w1,y1 let w, y, w1, y1 be VECTOR of V; ::_thesis: ( ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & a = 0 & b <> 0 ) implies w,y // w1,y1 ) given a, b being Real such that A2: ( a * (y - w) = b * (y1 - w1) & a = 0 ) and A3: b <> 0 ; ::_thesis: w,y // w1,y1 0. V = b * (y1 - w1) by A2, RLVECT_1:10; then y1 - w1 = 0. V by A3, RLVECT_1:11; then y1 = w1 by RLVECT_1:21; hence w,y // w1,y1 by ANALOAF:9; ::_thesis: verum end; A4: now__::_thesis:_for_w,_y,_w1,_y1_being_VECTOR_of_V_st_ex_a,_b_being_Real_st_ (_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_0_<_a_&_b_<_0_)_holds_ w,y_//_y1,w1 let w, y, w1, y1 be VECTOR of V; ::_thesis: ( ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & 0 < a & b < 0 ) implies w,y // y1,w1 ) given a, b being Real such that A5: a * (y - w) = b * (y1 - w1) and A6: 0 < a and A7: b < 0 ; ::_thesis: w,y // y1,w1 A8: a * (y - w) = b * (- (w1 - y1)) by A5, RLVECT_1:33 .= (- b) * (w1 - y1) by RLVECT_1:24 ; 0 < - b by A7, XREAL_1:58; hence w,y // y1,w1 by A6, A8, ANALOAF:def_1; ::_thesis: verum end; A9: now__::_thesis:_(_for_a,_b_being_Real_holds_ (_not_a_*_(v_-_u)_=_b_*_(v1_-_u1)_or_(_not_a_<>_0_&_not_b_<>_0_)_)_or_u,v_//_u1,v1_or_u,v_//_v1,u1_) given a, b being Real such that A10: a * (v - u) = b * (v1 - u1) and A11: ( a <> 0 or b <> 0 ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 ) A12: now__::_thesis:_(_a_<>_0_&_b_<>_0_&_not_u,v_//_u1,v1_implies_u,v_//_v1,u1_) A13: now__::_thesis:_(_a_<_0_&_b_<_0_&_not_u,v_//_u1,v1_implies_u,v_//_v1,u1_) assume ( a < 0 & b < 0 ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 ) then A14: ( 0 < - a & 0 < - b ) by XREAL_1:58; (- a) * (u - v) = a * (- (u - v)) by RLVECT_1:24 .= b * (v1 - u1) by A10, RLVECT_1:33 .= b * (- (u1 - v1)) by RLVECT_1:33 .= (- b) * (u1 - v1) by RLVECT_1:24 ; then v,u // v1,u1 by A14, ANALOAF:def_1; hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; ::_thesis: verum end; A15: now__::_thesis:_(_a_<_0_&_0_<_b_&_not_u,v_//_u1,v1_implies_u,v_//_v1,u1_) assume ( a < 0 & 0 < b ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 ) then u1,v1 // v,u by A4, A10; then v,u // u1,v1 by ANALOAF:12; hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; ::_thesis: verum end; assume A16: ( a <> 0 & b <> 0 ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 ) ( 0 < a & b < 0 & not u,v // u1,v1 implies u,v // v1,u1 ) by A4, A10; hence ( u,v // u1,v1 or u,v // v1,u1 ) by A10, A16, A15, A13, ANALOAF:def_1; ::_thesis: verum end; now__::_thesis:_(_not_b_=_0_or_u,v_//_u1,v1_or_u,v_//_v1,u1_) assume b = 0 ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 ) then u1,v1 // u,v by A1, A10, A11; hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; ::_thesis: verum end; hence ( u,v // u1,v1 or u,v // v1,u1 ) by A1, A10, A12; ::_thesis: verum end; A17: now__::_thesis:_for_w,_y,_w1,_y1_being_VECTOR_of_V_st_w,y_//_w1,y1_holds_ ex_a,_b_being_Real_st_ (_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_(_a_<>_0_or_b_<>_0_)_) let w, y, w1, y1 be VECTOR of V; ::_thesis: ( w,y // w1,y1 implies ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ) assume A18: w,y // w1,y1 ; ::_thesis: ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) A19: now__::_thesis:_(_w_=_y_implies_ex_a,_b_being_Real_st_ (_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_(_a_<>_0_or_b_<>_0_)_)_) assume w = y ; ::_thesis: ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) then 1 * (y - w) = 0. V by RLVECT_1:10, RLVECT_1:15 .= 0 * (y1 - w1) by RLVECT_1:10 ; hence ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum end; A20: now__::_thesis:_(_w1_=_y1_implies_ex_a,_b_being_Real_st_ (_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_(_a_<>_0_or_b_<>_0_)_)_) assume w1 = y1 ; ::_thesis: ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) then 1 * (y1 - w1) = 0. V by RLVECT_1:10, RLVECT_1:15 .= 0 * (y - w) by RLVECT_1:10 ; hence ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum end; ( ex a, b being Real st ( 0 < a & 0 < b & a * (y - w) = b * (y1 - w1) ) implies ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ) ; hence ex a, b being Real st ( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) by A18, A19, A20, ANALOAF:def_1; ::_thesis: verum end; now__::_thesis:_(_u,v_//_v1,u1_implies_ex_a,_b_being_Real_st_ (_a_*_(v_-_u)_=_b_*_(v1_-_u1)_&_(_a_<>_0_or_b_<>_0_)_)_) assume u,v // v1,u1 ; ::_thesis: ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) then consider a, b being Real such that A21: a * (v - u) = b * (u1 - v1) and A22: ( a <> 0 or b <> 0 ) by A17; A23: ( a <> 0 or - b <> 0 ) by A22; (- b) * (v1 - u1) = b * (- (v1 - u1)) by RLVECT_1:24 .= a * (v - u) by A21, RLVECT_1:33 ; hence ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A23; ::_thesis: verum end; hence ( ( 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 ) ) ) by A17, A9; ::_thesis: verum end; 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 ) ) ) proof let V be RealLinearSpace; ::_thesis: 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 ) ) ) let u, v, u1, v1 be VECTOR of V; ::_thesis: ( [[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 ) ) ) ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ( [[u,v],[u1,v1]] in DirPar V or [[u,v],[v1,u1]] in DirPar V ) ) by DIRAF:def_1; then ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ( u,v // u1,v1 or u,v // v1,u1 ) ) by ANALOAF:22; hence ( [[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 ) ) ) by Th14; ::_thesis: verum end; 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 ) ) proof defpred S1[ set , set ] means ex u, u1, v, v1 being VECTOR of V st ( $1 = [u,u1] & $2 = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ); set VV = [: the carrier of V, the carrier of V:]; consider P being Relation of [: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:] such that A1: for x, z being set holds ( [x,z] in P iff ( x in [: the carrier of V, the carrier of V:] & z in [: the carrier of V, the carrier of V:] & S1[x,z] ) ) from RELSET_1:sch_1(); take P ; ::_thesis: for x, z being set holds ( [x,z] in P 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 ) ) let x, z be set ; ::_thesis: ( [x,z] in P 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 ) ) thus ( [x,z] in P implies 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 ) ) by A1; ::_thesis: ( 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 ) implies [x,z] in P ) assume 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 ) ; ::_thesis: [x,z] in P hence [x,z] in P by A1; ::_thesis: verum end; 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 proof let P, Q be Relation of [: the carrier of V, the carrier of V:]; ::_thesis: ( ( for x, z being set holds ( [x,z] in P 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 Q 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 ) ) ) implies P = Q ) assume that A2: for x, z being set holds ( [x,z] in P 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 ) ) and A3: for x, z being set holds ( [x,z] in Q 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 ) ) ; ::_thesis: P = Q for x, z being set holds ( [x,z] in P iff [x,z] in Q ) proof let x, z be set ; ::_thesis: ( [x,z] in P iff [x,z] in Q ) ( [x,z] in P 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 ) ) by A2; hence ( [x,z] in P iff [x,z] in Q ) by A3; ::_thesis: verum end; hence P = Q by RELAT_1:def_2; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: the carrier of (Lambda (OASpace V)) = the carrier of V ( Lambda (OASpace V) = AffinStruct(# the carrier of (OASpace V),(lambda the CONGR of (OASpace V)) #) & OASpace V = AffinStruct(# the carrier of V,(DirPar V) #) ) by ANALOAF:def_4, DIRAF:def_2; hence the carrier of (Lambda (OASpace V)) = the carrier of V ; ::_thesis: verum end; theorem Th17: :: ANALMETR:17 for V being RealLinearSpace holds the CONGR of (Lambda (OASpace V)) = lambda (DirPar V) proof let V be RealLinearSpace; ::_thesis: the CONGR of (Lambda (OASpace V)) = lambda (DirPar V) ( Lambda (OASpace V) = AffinStruct(# the carrier of (OASpace V),(lambda the CONGR of (OASpace V)) #) & OASpace V = AffinStruct(# the carrier of V,(DirPar V) #) ) by ANALOAF:def_4, DIRAF:def_2; hence the CONGR of (Lambda (OASpace V)) = lambda (DirPar V) ; ::_thesis: verum end; 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 ) ) ) proof let V be RealLinearSpace; ::_thesis: 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 ) ) ) let u, v, u1, v1 be VECTOR of V; ::_thesis: 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 ) ) ) let p, q, p1, q1 be Element of (Lambda (OASpace V)); ::_thesis: ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) ) assume A1: ( p = u & q = v & p1 = u1 & q1 = v1 ) ; ::_thesis: ( p,q // p1,q1 iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) hereby ::_thesis: ( ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) implies p,q // p1,q1 ) assume p,q // p1,q1 ; ::_thesis: ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) then [[p,q],[p1,q1]] in the CONGR of (Lambda (OASpace V)) by ANALOAF:def_2; then [[u,v],[u1,v1]] in lambda (DirPar V) by A1, Th17; hence ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by Th15; ::_thesis: verum end; given a, b being Real such that A2: ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: p,q // p1,q1 [[u,v],[u1,v1]] in lambda (DirPar V) by A2, Th15; then [[p,q],[p1,q1]] in the CONGR of (Lambda (OASpace V)) by A1, Th17; hence p,q // p1,q1 by ANALOAF:def_2; ::_thesis: verum end; 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 proof set A = the non empty set ; set C = the Relation of [: the non empty set , the non empty set :]; take ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) ; ::_thesis: not ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) is empty thus not the carrier of ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; 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) proof let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V holds Af (AMSpace (V,w,y)) = Lambda (OASpace V) let w, y be VECTOR of V; ::_thesis: Af (AMSpace (V,w,y)) = Lambda (OASpace V) set Y = OASpace V; the carrier of (Lambda (OASpace V)) = the carrier of V by Th16; hence Af (AMSpace (V,w,y)) = Lambda (OASpace V) by Th17; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let u, u1, v, v1, w, y be VECTOR of V; ::_thesis: 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 ) let p, p1, q, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p = u & p1 = u1 & q = v & q1 = v1 implies ( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y ) ) assume A1: ( p = u & p1 = u1 & q = v & q1 = v1 ) ; ::_thesis: ( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y ) A2: ( p,q _|_ p1,q1 iff [[p,q],[p1,q1]] in the orthogonality of (AMSpace (V,w,y)) ) by Def5; hereby ::_thesis: ( u,v,u1,v1 are_Ort_wrt w,y implies p,q _|_ p1,q1 ) assume p,q _|_ p1,q1 ; ::_thesis: u,v,u1,v1 are_Ort_wrt w,y then consider u9, v9, u19, v19 being VECTOR of V such that A3: [u,v] = [u9,v9] and A4: [u1,v1] = [u19,v19] and A5: u9,v9,u19,v19 are_Ort_wrt w,y by A1, A2, Def4; A6: u1 = u19 by A4, XTUPLE_0:1; ( u = u9 & v = v9 ) by A3, XTUPLE_0:1; hence u,v,u1,v1 are_Ort_wrt w,y by A4, A5, A6, XTUPLE_0:1; ::_thesis: verum end; assume u,v,u1,v1 are_Ort_wrt w,y ; ::_thesis: p,q _|_ p1,q1 hence p,q _|_ p1,q1 by A1, A2, Def4; ::_thesis: verum end; 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 ) ) ) proof let V be RealLinearSpace; ::_thesis: 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 ) ) ) let w, y, u, v, u1, v1 be VECTOR of V; ::_thesis: 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 ) ) ) let p, q, p1, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) ) assume A1: ( p = u & q = v & p1 = u1 & q1 = v1 ) ; ::_thesis: ( p,q // p1,q1 iff ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) hereby ::_thesis: ( ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) implies p,q // p1,q1 ) assume p,q // p1,q1 ; ::_thesis: ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) then [[p,q],[p1,q1]] in the CONGR of (AMSpace (V,w,y)) by ANALOAF:def_2; hence ex a, b being Real st ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A1, Th15; ::_thesis: verum end; given a, b being Real such that A2: ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: p,q // p1,q1 [[u,v],[u1,v1]] in lambda (DirPar V) by A2, Th15; hence p,q // p1,q1 by A1, ANALOAF:def_2; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds p1,q1 _|_ p,q let p, q, p1, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p,q _|_ p1,q1 implies p1,q1 _|_ p,q ) reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of V ; assume p,q _|_ p1,q1 ; ::_thesis: p1,q1 _|_ p,q then u,v,u1,v1 are_Ort_wrt w,y by Th21; then v - u,v1 - u1 are_Ort_wrt w,y by Def3; then v1 - u1,v - u are_Ort_wrt w,y by Th4; then u1,v1,u,v are_Ort_wrt w,y by Def3; hence p1,q1 _|_ p,q by Th21; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds p,q _|_ q1,p1 let p, q, p1, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p,q _|_ p1,q1 implies p,q _|_ q1,p1 ) reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of V ; assume p,q _|_ p1,q1 ; ::_thesis: p,q _|_ q1,p1 then u,v,u1,v1 are_Ort_wrt w,y by Th21; then v - u,v1 - u1 are_Ort_wrt w,y by Def3; then A1: v - u,(- 1) * (v1 - u1) are_Ort_wrt w,y by Th7; (- 1) * (v1 - u1) = - (v1 - u1) by RLVECT_1:16 .= u1 - v1 by RLVECT_1:33 ; then u,v,v1,u1 are_Ort_wrt w,y by A1, Def3; hence p,q _|_ q1,p1 by Th21; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for p, q, r being Element of (AMSpace (V,w,y)) holds p,q _|_ r,r ) assume A1: Gen w,y ; ::_thesis: for p, q, r being Element of (AMSpace (V,w,y)) holds p,q _|_ r,r let p, q, r be Element of (AMSpace (V,w,y)); ::_thesis: p,q _|_ r,r reconsider u = p, v = q, u1 = r as Element of V ; u1 - u1 = 0. V by RLVECT_1:15; then v - u,u1 - u1 are_Ort_wrt w,y by A1, Th5; then u,v,u1,u1 are_Ort_wrt w,y by Def3; hence p,q _|_ r,r by Th21; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: 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 let p, p1, q, q1, r, r1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 implies q,q1 _|_ r,r1 ) assume that A1: p,p1 _|_ q,q1 and A2: p,p1 // r,r1 ; ::_thesis: ( p = p1 or q,q1 _|_ r,r1 ) reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V ; consider a, b being Real such that A3: a * (v - u) = b * (v2 - u2) and A4: ( a <> 0 or b <> 0 ) by A2, Th22; assume A5: p <> p1 ; ::_thesis: q,q1 _|_ r,r1 b <> 0 proof assume A6: b = 0 ; ::_thesis: contradiction then a * (v - u) = 0. V by A3, RLVECT_1:10; then v - u = 0. V by A4, A6, RLVECT_1:11; hence contradiction by A5, RLVECT_1:21; ::_thesis: verum end; then A7: v2 - u2 = (b ") * (a * (v - u)) by A3, ANALOAF:5 .= ((b ") * a) * (v - u) by RLVECT_1:def_7 ; u,v,u1,v1 are_Ort_wrt w,y by A1, Th21; then v - u,v1 - u1 are_Ort_wrt w,y by Def3; then v2 - u2,v1 - u1 are_Ort_wrt w,y by A7, Th7; then v1 - u1,v2 - u2 are_Ort_wrt w,y by Th4; then u1,v1,u2,v2 are_Ort_wrt w,y by Def3; hence q,q1 _|_ r,r1 by Th21; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies 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 ) ) assume A1: Gen w,y ; ::_thesis: 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 ) let p, q, r be Element of (AMSpace (V,w,y)); ::_thesis: ex r1 being Element of (AMSpace (V,w,y)) st ( p,q _|_ r,r1 & r <> r1 ) reconsider u = p, v = q, u1 = r as Element of V ; consider v2 being VECTOR of V such that A2: v - u,v2 are_Ort_wrt w,y and A3: v2 <> 0. V by A1, Th8; set v1 = u1 + v2; reconsider r1 = u1 + v2 as Element of (AMSpace (V,w,y)) ; A4: (u1 + v2) - u1 = v2 + (u1 - u1) by RLVECT_1:def_3 .= v2 + (0. V) by RLVECT_1:15 .= v2 by RLVECT_1:4 ; then u,v,u1,u1 + v2 are_Ort_wrt w,y by A2, Def3; then A5: p,q _|_ r,r1 by Th21; r <> r1 by A3, A4, RLVECT_1:15; hence ex r1 being Element of (AMSpace (V,w,y)) st ( p,q _|_ r,r1 & r <> r1 ) by A5; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: 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 let p, p1, q, q1, r, r1 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 implies q,q1 // r,r1 ) assume that A1: Gen w,y and A2: p,p1 _|_ q,q1 and A3: p,p1 _|_ r,r1 ; ::_thesis: ( p = p1 or q,q1 // r,r1 ) reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V ; u,v,u2,v2 are_Ort_wrt w,y by A3, Th21; then A4: v - u,v2 - u2 are_Ort_wrt w,y by Def3; assume p <> p1 ; ::_thesis: q,q1 // r,r1 then A5: v - u <> 0. V by RLVECT_1:21; u,v,u1,v1 are_Ort_wrt w,y by A2, Th21; then v - u,v1 - u1 are_Ort_wrt w,y by Def3; then ex a, b being Real st ( a * (v1 - u1) = b * (v2 - u2) & ( a <> 0 or b <> 0 ) ) by A1, A4, A5, Th9; hence q,q1 // r,r1 by Th22; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: 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 let p, q, r, r1, r2 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 implies p,q _|_ r1,r2 ) assume that A1: Gen w,y and A2: p,q _|_ r,r1 and A3: p,q _|_ r,r2 ; ::_thesis: p,q _|_ r1,r2 reconsider u = p, v = q, w1 = r, v1 = r1, v2 = r2 as Element of V ; u,v,w1,v2 are_Ort_wrt w,y by A3, Th21; then A4: v - u,v2 - w1 are_Ort_wrt w,y by Def3; A5: (v2 - w1) - (v1 - w1) = v2 - ((v1 - w1) + w1) by RLVECT_1:27 .= v2 - (v1 - (w1 - w1)) by RLVECT_1:29 .= v2 - (v1 - (0. V)) by RLVECT_1:15 .= v2 - v1 by RLVECT_1:13 ; u,v,w1,v1 are_Ort_wrt w,y by A2, Th21; then v - u,v1 - w1 are_Ort_wrt w,y by Def3; then v - u,(v2 - w1) - (v1 - w1) are_Ort_wrt w,y by A1, A4, Th10; then u,v,v1,v2 are_Ort_wrt w,y by A5, Def3; hence p,q _|_ r1,r2 by Th21; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds p = q let p, q be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,q _|_ p,q implies p = q ) assume that A1: Gen w,y and A2: p,q _|_ p,q ; ::_thesis: p = q reconsider u = p, v = q as Element of V ; u,v,u,v are_Ort_wrt w,y by A2, Th21; then v - u,v - u are_Ort_wrt w,y by Def3; then v - u = 0. V by A1, Th11; hence p = q by RLVECT_1:21; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: 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 let w, y be VECTOR of V; ::_thesis: 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 let p, q, p1, p2 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p implies p2,q _|_ p,p1 ) assume that A1: Gen w,y and A2: p,q _|_ p1,p2 and A3: p1,q _|_ p2,p ; ::_thesis: p2,q _|_ p,p1 reconsider u = p, v = q, u1 = p1, u2 = p2 as Element of V ; u,v,u1,u2 are_Ort_wrt w,y by A2, Th21; then A4: v - u,u2 - u1 are_Ort_wrt w,y by Def3; u1,v,u2,u are_Ort_wrt w,y by A3, Th21; then A5: v - u1,u - u2 are_Ort_wrt w,y by Def3; A6: now__::_thesis:_for_u,_v,_w_being_VECTOR_of_V_holds_(u_-_v)_-_(u_-_w)_=_w_-_v let u, v, w be VECTOR of V; ::_thesis: (u - v) - (u - w) = w - v thus (u - v) - (u - w) = (w - u) + (u - v) by RLVECT_1:33 .= w - v by ANALOAF:1 ; ::_thesis: verum end; then A7: (v - u) - (v - u1) = u1 - u ; ( (v - u1) - (v - u2) = u2 - u1 & (v - u2) - (v - u) = u - u2 ) by A6; then v - u2,(v - u) - (v - u1) are_Ort_wrt w,y by A1, A4, A5, Th12; then u2,v,u,u1 are_Ort_wrt w,y by A7, Def3; hence p2,q _|_ p,p1 by Th21; ::_thesis: verum end; 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 ) proof let V be RealLinearSpace; ::_thesis: 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 ) let w, y be VECTOR of V; ::_thesis: 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 ) let p, p1 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p <> p1 implies 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 ) ) assume that A1: Gen w,y and A2: p <> p1 ; ::_thesis: 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 ) let q be Element of (AMSpace (V,w,y)); ::_thesis: ex q1 being Element of (AMSpace (V,w,y)) st ( p,p1 // p,q1 & p,p1 _|_ q1,q ) reconsider u = p, v = q, u1 = p1 as Element of V ; u1 - u <> 0. V by A2, RLVECT_1:21; then consider a being Real such that A3: (v - u) - (a * (u1 - u)),u1 - u are_Ort_wrt w,y by A1, Th13; set v1 = u + (a * (u1 - u)); reconsider q1 = u + (a * (u1 - u)) as Element of (AMSpace (V,w,y)) ; v - (u + (a * (u1 - u))) = (v - u) - (a * (u1 - u)) by RLVECT_1:27; then u1 - u,v - (u + (a * (u1 - u))) are_Ort_wrt w,y by A3, Th4; then u,u1,u + (a * (u1 - u)),v are_Ort_wrt w,y by Def3; then A4: p,p1 _|_ q1,q by Th21; a * (u1 - u) = (a * (u1 - u)) + (0. V) by RLVECT_1:4 .= (a * (u1 - u)) + (u - u) by RLVECT_1:15 .= (u + (a * (u1 - u))) - u by RLVECT_1:def_3 .= 1 * ((u + (a * (u1 - u))) - u) by RLVECT_1:def_8 ; then p,p1 // p,q1 by Th22; hence ex q1 being Element of (AMSpace (V,w,y)) st ( p,p1 // p,q1 & p,p1 _|_ q1,q ) by A4; ::_thesis: verum end; 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 ) proof AMSpace (V0,w0,y0) is OrtAfSp-like by Def8, Lm8; hence ex b1 being non empty ParOrtStr st ( b1 is strict & b1 is OrtAfSp-like ) ; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds AMSpace (V,w,y) is OrtAfSp let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies AMSpace (V,w,y) is OrtAfSp ) set POS = AMSpace (V,w,y); set X = AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #); assume A1: Gen w,y ; ::_thesis: AMSpace (V,w,y) is OrtAfSp then A2: for a, b, c being Element of (AMSpace (V,w,y)) ex x being Element of (AMSpace (V,w,y)) st ( a,b _|_ c,x & c <> x ) by Th27; AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Af (AMSpace (V,w,y)) ; then A3: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V) by Th20; for a, b being Real st (a * w) + (b * y) = 0. V holds ( a = 0 & b = 0 ) by A1, Def1; then OASpace V is OAffinSpace by ANALOAF:26; then A4: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) is AffinSpace by A3, DIRAF:41; ( ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V,w,y)) 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 (V,w,y)) st a <> b holds ex x being Element of (AMSpace (V,w,y)) st ( a,b // a,x & a,b _|_ x,c ) ) ) by A1, Th23, Th24, Th25, Th26, Th29, Th30, Th32; hence AMSpace (V,w,y) is OrtAfSp by A2, A4, Def8; ::_thesis: verum end; 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 ) proof AMSpace (V0,w0,y0) is OrtAfPl-like by Def9, Lm11; hence ex b1 being non empty ParOrtStr st ( b1 is strict & b1 is OrtAfPl-like ) ; ::_thesis: verum end; 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 proof let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds AMSpace (V,w,y) is OrtAfPl let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies AMSpace (V,w,y) is OrtAfPl ) set POS = AMSpace (V,w,y); set X = AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #); AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Af (AMSpace (V,w,y)) ; then A1: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V) by Th20; assume A2: Gen w,y ; ::_thesis: AMSpace (V,w,y) is OrtAfPl then ( ( for a, b being Real st (a * w) + (b * y) = 0. V holds ( a = 0 & b = 0 ) ) & ( for w1 being VECTOR of V ex a, b being Real st w1 = (a * w) + (b * y) ) ) by Def1; then OASpace V is OAffinPlane by ANALOAF:28; then A3: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) is AffinPlane by A1, DIRAF:45; ( ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V,w,y)) 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 (V,w,y)) ex x being Element of (AMSpace (V,w,y)) st ( a,b _|_ c,x & c <> x ) ) ) by A2, Th23, Th24, Th25, Th26, Th27, Th28, Th30; hence AMSpace (V,w,y) is OrtAfPl by A3, Def9; ::_thesis: verum end; 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 ) proof let POS be non empty ParOrtStr ; ::_thesis: 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 ) set AF = Af POS; let a, b, c, d be Element of POS; ::_thesis: 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 ) let a9, b9, c9, d9 be Element of (Af POS); ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a,b // c,d iff a9,b9 // c9,d9 ) ) assume A1: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; ::_thesis: ( a,b // c,d iff a9,b9 // c9,d9 ) hereby ::_thesis: ( a9,b9 // c9,d9 implies a,b // c,d ) assume a,b // c,d ; ::_thesis: a9,b9 // c9,d9 then [[a9,b9],[c9,d9]] in the CONGR of (Af POS) by A1, ANALOAF:def_2; hence a9,b9 // c9,d9 by ANALOAF:def_2; ::_thesis: verum end; assume a9,b9 // c9,d9 ; ::_thesis: a,b // c,d then [[a,b],[c,d]] in the CONGR of POS by A1, ANALOAF:def_2; hence a,b // c,d by ANALOAF:def_2; ::_thesis: verum end; 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 proof let POS be OrtAfPl; ::_thesis: POS is OrtAfSp for a, b, c, d, p, q, r, s being Element of POS st a,b _|_ p,q & a,b _|_ p,s holds a,b _|_ q,s proof let a, b, c, d, p, q, r, s be Element of POS; ::_thesis: ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) assume that A1: a,b _|_ p,q and A2: a,b _|_ p,s ; ::_thesis: a,b _|_ q,s A3: now__::_thesis:_(_a_<>_b_&_p_<>_q_implies_a,b__|__q,s_) reconsider p9 = p, q9 = q, s9 = s as Element of (Af POS) ; assume that A4: a <> b and A5: p <> q ; ::_thesis: a,b _|_ q,s p,q // p,s by A1, A2, A4, Def9; then p9,q9 // p9,s9 by Th36; then q9,p9 // q9,s9 by DIRAF:40; then p9,q9 // q9,s9 by AFF_1:4; then A6: p,q // q,s by Th36; p,q _|_ a,b by A1, Def9; hence a,b _|_ q,s by A5, A6, Def9; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_a,b__|__q,s_) assume a = b ; ::_thesis: a,b _|_ q,s then q,s _|_ a,b by Def9; hence a,b _|_ q,s by Def9; ::_thesis: verum end; hence a,b _|_ q,s by A2, A3; ::_thesis: verum end; then A7: for a, b, c, d, p, q, r, s being Element of POS 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 ) ) by Def9; A8: for a, b, c being Element of POS st a <> b holds ex x being Element of POS st ( a,b // a,x & a,b _|_ x,c ) proof let a, b, c be Element of POS; ::_thesis: ( a <> b implies ex x being Element of POS st ( a,b // a,x & a,b _|_ x,c ) ) assume A9: a <> b ; ::_thesis: ex x being Element of POS st ( a,b // a,x & a,b _|_ x,c ) consider y being Element of POS such that A10: a,b _|_ c,y and A11: c <> y by Def9; reconsider a9 = a, b9 = b, c9 = c, y9 = y as Element of (Af POS) ; not a9,b9 // c9,y9 proof assume a9,b9 // c9,y9 ; ::_thesis: contradiction then a,b // c,y by Th36; then c,y _|_ c,y by A9, A10, Def9; hence contradiction by A11, Def9; ::_thesis: verum end; then consider x9 being Element of (Af POS) such that A12: LIN a9,b9,x9 and A13: LIN c9,y9,x9 by AFF_1:60; reconsider x = x9 as Element of POS ; c9,y9 // c9,x9 by A13, AFF_1:def_1; then A14: c,y // c,x by Th36; c,y _|_ a,b by A10, Def9; then a,b _|_ c,x by A11, A14, Def9; then A15: a,b _|_ x,c by Def9; a9,b9 // a9,x9 by A12, AFF_1:def_1; then a,b // a,x by Th36; hence ex x being Element of POS st ( a,b // a,x & a,b _|_ x,c ) by A15; ::_thesis: verum end; ( Af POS = AffinStruct(# the carrier of POS, the CONGR of POS #) & ( for a, b, c being Element of POS ex x being Element of POS st ( a,b _|_ c,x & c <> x ) ) ) by Def9; hence POS is OrtAfSp by A8, A7, Def8; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: ( Af POS is AffinPlane implies POS is OrtAfPl ) assume A1: Af POS is AffinPlane ; ::_thesis: POS is OrtAfPl A2: now__::_thesis:_for_a,_b,_c,_d,_p,_q,_r,_s_being_Element_of_POS_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_)_) let a, b, c, d, p, q, r, s be Element of POS; ::_thesis: ( ( 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 ) ) thus ( ( 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 ) ) by Def8; ::_thesis: ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) thus ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ::_thesis: verum proof reconsider a9 = a, b9 = b, p9 = p, q9 = q, r9 = r, s9 = s as Element of (Af POS) ; assume that A3: a,b _|_ p,q and A4: a,b _|_ r,s ; ::_thesis: ( p,q // r,s or a = b ) A5: p,q _|_ a,b by A3, Def8; A6: r,s _|_ a,b by A4, Def8; assume A7: ( not p,q // r,s & not a = b ) ; ::_thesis: contradiction then A8: not p9,q9 // r9,s9 by Th36; then A9: p9 <> q9 by AFF_1:3; consider x9 being Element of (Af POS) such that A10: LIN p9,q9,x9 and A11: LIN r9,s9,x9 by A1, A8, AFF_1:60; reconsider x = x9 as Element of POS ; A12: r9 <> s9 by A8, AFF_1:3; LIN s9,r9,x9 by A11, AFF_1:6; then s9,r9 // s9,x9 by AFF_1:def_1; then A13: r9,s9 // x9,s9 by AFF_1:4; then r,s // x,s by Th36; then a,b _|_ x,s by A12, A6, Def8; then A14: x,s _|_ a,b by Def8; LIN q9,p9,x9 by A10, AFF_1:6; then q9,p9 // q9,x9 by AFF_1:def_1; then p9,q9 // x9,q9 by AFF_1:4; then p,q // x,q by Th36; then A15: a,b _|_ x,q by A9, A5, Def8; A16: now__::_thesis:_(_x_<>_q_implies_not_x_<>_s_) consider y9 being Element of (Af POS) such that A17: ( a9,b9 // q9,y9 & q9 <> y9 ) by DIRAF:40; assume that A18: x <> q and A19: x <> s ; ::_thesis: contradiction not q9,y9 // x9,s9 proof assume q9,y9 // x9,s9 ; ::_thesis: contradiction then q9,y9 // r9,s9 by A13, A19, AFF_1:5; then r9,s9 // a9,b9 by A17, AFF_1:5; then r,s // a,b by Th36; then a,b _|_ a,b by A12, A6, Def8; hence contradiction by A7, Def8; ::_thesis: verum end; then consider z9 being Element of (Af POS) such that A20: LIN q9,y9,z9 and A21: LIN x9,s9,z9 by A1, AFF_1:60; reconsider z = z9 as Element of POS ; q9,y9 // q9,z9 by A20, AFF_1:def_1; then a9,b9 // q9,z9 by A17, AFF_1:5; then A22: a,b // q,z by Th36; A23: x9,s9 // x9,z9 by A21, AFF_1:def_1; then x,s // x,z by Th36; then a,b _|_ x,z by A14, A19, Def8; then a,b _|_ q,z by A15, Def8; then q,z _|_ q,z by A7, A22, Def8; then x9,s9 // x9,q9 by A23, Def8; then A24: LIN x9,s9,q9 by AFF_1:def_1; ( LIN x9,s9,x9 & LIN x9,q9,p9 ) by A10, AFF_1:6, AFF_1:7; then LIN x9,s9,p9 by A18, A24, AFF_1:11; then x9,s9 // p9,q9 by A24, AFF_1:10; then p9,q9 // r9,s9 by A13, A19, AFF_1:5; hence contradiction by A7, Th36; ::_thesis: verum end; r9,s9 // r9,x9 by A11, AFF_1:def_1; then A25: r9,s9 // x9,r9 by AFF_1:4; then r,s // x,r by Th36; then a,b _|_ x,r by A12, A6, Def8; then A26: x,r _|_ a,b by Def8; A27: now__::_thesis:_(_x_<>_q_implies_not_x_<>_r_) consider y9 being Element of (Af POS) such that A28: ( a9,b9 // q9,y9 & q9 <> y9 ) by DIRAF:40; assume that A29: x <> q and A30: x <> r ; ::_thesis: contradiction not q9,y9 // x9,r9 proof assume q9,y9 // x9,r9 ; ::_thesis: contradiction then q9,y9 // r9,s9 by A25, A30, AFF_1:5; then r9,s9 // a9,b9 by A28, AFF_1:5; then r,s // a,b by Th36; then a,b _|_ a,b by A12, A6, Def8; hence contradiction by A7, Def8; ::_thesis: verum end; then consider z9 being Element of (Af POS) such that A31: LIN q9,y9,z9 and A32: LIN x9,r9,z9 by A1, AFF_1:60; reconsider z = z9 as Element of POS ; q9,y9 // q9,z9 by A31, AFF_1:def_1; then a9,b9 // q9,z9 by A28, AFF_1:5; then A33: a,b // q,z by Th36; A34: x9,r9 // x9,z9 by A32, AFF_1:def_1; then x,r // x,z by Th36; then a,b _|_ x,z by A26, A30, Def8; then a,b _|_ q,z by A15, Def8; then q,z _|_ q,z by A7, A33, Def8; then x9,r9 // x9,q9 by A34, Def8; then A35: LIN x9,r9,q9 by AFF_1:def_1; ( LIN x9,r9,x9 & LIN x9,q9,p9 ) by A10, AFF_1:6, AFF_1:7; then LIN x9,r9,p9 by A29, A35, AFF_1:11; then x9,r9 // p9,q9 by A35, AFF_1:10; then p9,q9 // r9,s9 by A25, A30, AFF_1:5; hence contradiction by A7, Th36; ::_thesis: verum end; p9,q9 // p9,x9 by A10, AFF_1:def_1; then p9,q9 // x9,p9 by AFF_1:4; then p,q // x,p by Th36; then A36: a,b _|_ x,p by A9, A5, Def8; A37: now__::_thesis:_(_x_<>_p_implies_not_x_<>_s_) consider y9 being Element of (Af POS) such that A38: ( a9,b9 // p9,y9 & p9 <> y9 ) by DIRAF:40; assume that A39: x <> p and A40: x <> s ; ::_thesis: contradiction not p9,y9 // x9,s9 proof assume p9,y9 // x9,s9 ; ::_thesis: contradiction then p9,y9 // r9,s9 by A13, A40, AFF_1:5; then r9,s9 // a9,b9 by A38, AFF_1:5; then r,s // a,b by Th36; then a,b _|_ a,b by A12, A6, Def8; hence contradiction by A7, Def8; ::_thesis: verum end; then consider z9 being Element of (Af POS) such that A41: LIN p9,y9,z9 and A42: LIN x9,s9,z9 by A1, AFF_1:60; reconsider z = z9 as Element of POS ; p9,y9 // p9,z9 by A41, AFF_1:def_1; then a9,b9 // p9,z9 by A38, AFF_1:5; then A43: a,b // p,z by Th36; A44: x9,s9 // x9,z9 by A42, AFF_1:def_1; then x,s // x,z by Th36; then a,b _|_ x,z by A14, A40, Def8; then a,b _|_ p,z by A36, Def8; then p,z _|_ p,z by A7, A43, Def8; then x9,s9 // x9,p9 by A44, Def8; then A45: LIN x9,s9,p9 by AFF_1:def_1; ( LIN x9,s9,x9 & LIN x9,p9,q9 ) by A10, AFF_1:6, AFF_1:7; then LIN x9,s9,q9 by A39, A45, AFF_1:11; then x9,s9 // p9,q9 by A45, AFF_1:10; then p9,q9 // r9,s9 by A13, A40, AFF_1:5; hence contradiction by A7, Th36; ::_thesis: verum end; now__::_thesis:_(_x_<>_p_implies_not_x_<>_r_) consider y9 being Element of (Af POS) such that A46: ( a9,b9 // p9,y9 & p9 <> y9 ) by DIRAF:40; assume that A47: x <> p and A48: x <> r ; ::_thesis: contradiction not p9,y9 // x9,r9 proof assume p9,y9 // x9,r9 ; ::_thesis: contradiction then p9,y9 // r9,s9 by A25, A48, AFF_1:5; then r9,s9 // a9,b9 by A46, AFF_1:5; then r,s // a,b by Th36; then a,b _|_ a,b by A12, A6, Def8; hence contradiction by A7, Def8; ::_thesis: verum end; then consider z9 being Element of (Af POS) such that A49: LIN p9,y9,z9 and A50: LIN x9,r9,z9 by A1, AFF_1:60; reconsider z = z9 as Element of POS ; p9,y9 // p9,z9 by A49, AFF_1:def_1; then a9,b9 // p9,z9 by A46, AFF_1:5; then A51: a,b // p,z by Th36; A52: x9,r9 // x9,z9 by A50, AFF_1:def_1; then x,r // x,z by Th36; then a,b _|_ x,z by A26, A48, Def8; then a,b _|_ p,z by A36, Def8; then p,z _|_ p,z by A7, A51, Def8; then x9,r9 // x9,p9 by A52, Def8; then A53: LIN x9,r9,p9 by AFF_1:def_1; ( LIN x9,r9,x9 & LIN x9,p9,q9 ) by A10, AFF_1:6, AFF_1:7; then LIN x9,r9,q9 by A47, A53, AFF_1:11; then x9,r9 // p9,q9 by A53, AFF_1:10; then p9,q9 // r9,s9 by A25, A48, AFF_1:5; hence contradiction by A7, Th36; ::_thesis: verum end; hence contradiction by A8, A37, A27, A16, AFF_1:3; ::_thesis: verum end; end; for a, b, c being Element of POS ex x being Element of POS st ( a,b _|_ c,x & c <> x ) by Def8; hence POS is OrtAfPl by A1, A2, Def9; ::_thesis: verum end; 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 ) ) ) ) ) ) proof let POS be non empty ParOrtStr ; ::_thesis: ( 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 ) ) ) ) ) ) set P = Af POS; hereby ::_thesis: ( 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 ) ) ) ) implies POS is OrtAfPl-like ) assume A1: POS is OrtAfPl-like ; ::_thesis: ( ex x, y being Element of POS st x <> y & ( 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 ) ) ) ) ) then Af POS is AffinPlane ; hence ex x, y being Element of POS st x <> y by DIRAF:46; ::_thesis: 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 ) ) ) let a, b, c, d, p, q, r, s be Element of POS; ::_thesis: ( 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 ) ) ) reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q, r9 = r, s9 = s as Element of (Af POS) ; consider x9 being Element of (Af POS) such that A2: ( a9,b9 // c9,x9 & a9,c9 // b9,x9 ) by A1, DIRAF:46; ( a9,b9 // b9,a9 & a9,b9 // c9,c9 ) by A1, DIRAF:46; hence ( a,b // b,a & a,b // c,c ) by Th36; ::_thesis: ( ( 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 ) ) ) hereby ::_thesis: ( ( 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 ) ) ) assume ( a,b // p,q & a,b // r,s ) ; ::_thesis: ( p,q // r,s or a = b ) then ( a9,b9 // p9,q9 & a9,b9 // r9,s9 ) by Th36; then ( p9,q9 // r9,s9 or a9 = b9 ) by A1, DIRAF:46; hence ( p,q // r,s or a = b ) by Th36; ::_thesis: verum end; hereby ::_thesis: ( 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 ) ) ) assume a,b // a,c ; ::_thesis: b,a // b,c then a9,b9 // a9,c9 by Th36; then b9,a9 // b9,c9 by A1, DIRAF:46; hence b,a // b,c by Th36; ::_thesis: verum end; reconsider x = x9 as Element of POS ; consider x9, y9, z9 being Element of (Af POS) such that A3: not x9,y9 // x9,z9 by A1, DIRAF:46; ( a,b // c,x & a,c // b,x ) by A2, Th36; hence ex x being Element of POS st ( a,b // c,x & a,c // b,x ) ; ::_thesis: ( 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 ) ) ) reconsider x = x9, y = y9, z = z9 as Element of POS ; consider x9 being Element of (Af POS) such that A4: a9,b9 // c9,x9 and A5: c9 <> x9 by A1, DIRAF:46; not x,y // x,z by A3, Th36; hence not for x, y, z being Element of POS holds x,y // x,z ; ::_thesis: ( 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 ) ) ) reconsider x = x9 as Element of POS ; a,b // c,x by A4, Th36; hence ex x being Element of POS st ( a,b // c,x & c <> x ) by A5; ::_thesis: ( ( 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 ) ) ) hereby ::_thesis: ( ( 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 ) ) ) assume that A6: a,b // b,d and A7: b <> a ; ::_thesis: ex x being Element of POS st ( c,b // b,x & c,a // d,x ) a9,b9 // b9,d9 by A6, Th36; then consider x9 being Element of (Af POS) such that A8: ( c9,b9 // b9,x9 & c9,a9 // d9,x9 ) by A1, A7, DIRAF:46; reconsider x = x9 as Element of POS ; ( c,b // b,x & c,a // d,x ) by A8, Th36; hence ex x being Element of POS st ( c,b // b,x & c,a // d,x ) ; ::_thesis: verum end; thus ( ( 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 ) ) by A1, Def9; ::_thesis: ( not a,b // c,d implies ex x being Element of POS st ( a,b // a,x & c,d // c,x ) ) assume not a,b // c,d ; ::_thesis: ex x being Element of POS st ( a,b // a,x & c,d // c,x ) then not a9,b9 // c9,d9 by Th36; then consider x9 being Element of (Af POS) such that A9: ( a9,b9 // a9,x9 & c9,d9 // c9,x9 ) by A1, DIRAF:46; reconsider x = x9 as Element of POS ; ( a,b // a,x & c,d // c,x ) by A9, Th36; hence ex x being Element of POS st ( a,b // a,x & c,d // c,x ) ; ::_thesis: verum end; given a, b being Element of POS such that A10: a <> b ; ::_thesis: ( ex a, b, c, d, p, q, r, s being Element of POS st ( 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 ) implies ( not a,b // c,d & ( for x being Element of POS holds ( not a,b // a,x or not c,d // c,x ) ) ) ) or POS is OrtAfPl-like ) assume A11: 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 ) ) ) ; ::_thesis: POS is OrtAfPl-like A12: now__::_thesis:_for_x,_y,_z_being_Element_of_(Af_POS)_ex_t_being_Element_of_(Af_POS)_st_ (_x,z_//_y,t_&_y_<>_t_) let x, y, z be Element of (Af POS); ::_thesis: ex t being Element of (Af POS) st ( x,z // y,t & y <> t ) reconsider x9 = x, y9 = y, z9 = z as Element of POS ; consider t9 being Element of POS such that A13: x9,z9 // y9,t9 and A14: y9 <> t9 by A11; reconsider t = t9 as Element of (Af POS) ; x,z // y,t by A13, Th36; hence ex t being Element of (Af POS) st ( x,z // y,t & y <> t ) by A14; ::_thesis: verum end; A15: now__::_thesis:_for_x,_y,_z,_t,_u,_w_being_Element_of_(Af_POS)_holds_ (_x,y_//_y,x_&_x,y_//_z,z_&_(_x_<>_y_&_x,y_//_z,t_&_x,y_//_u,w_implies_z,t_//_u,w_)_&_(_x,y_//_x,z_implies_y,x_//_y,z_)_) let x, y, z, t, u, w be Element of (Af POS); ::_thesis: ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) reconsider a = x, b = y, c = z, d = t, e = u, f = w as Element of POS ; ( a,b // b,a & a,b // c,c ) by A11; hence ( x,y // y,x & x,y // z,z ) by Th36; ::_thesis: ( ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) thus ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) ::_thesis: ( x,y // x,z implies y,x // y,z ) proof assume that A16: x <> y and A17: ( x,y // z,t & x,y // u,w ) ; ::_thesis: z,t // u,w ( a,b // c,d & a,b // e,f ) by A17, Th36; then c,d // e,f by A11, A16; hence z,t // u,w by Th36; ::_thesis: verum end; thus ( x,y // x,z implies y,x // y,z ) ::_thesis: verum proof assume x,y // x,z ; ::_thesis: y,x // y,z then a,b // a,c by Th36; then b,a // b,c by A11; hence y,x // y,z by Th36; ::_thesis: verum end; end; A18: now__::_thesis:_for_x,_y,_z,_t_being_Element_of_(Af_POS)_st_not_x,y_//_z,t_holds_ ex_u_being_Element_of_(Af_POS)_st_ (_x,y_//_x,u_&_z,t_//_z,u_) let x, y, z, t be Element of (Af POS); ::_thesis: ( not x,y // z,t implies ex u being Element of (Af POS) st ( x,y // x,u & z,t // z,u ) ) assume A19: not x,y // z,t ; ::_thesis: ex u being Element of (Af POS) st ( x,y // x,u & z,t // z,u ) reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS ; not x9,y9 // z9,t9 by A19, Th36; then consider u9 being Element of POS such that A20: ( x9,y9 // x9,u9 & z9,t9 // z9,u9 ) by A11; reconsider u = u9 as Element of (Af POS) ; ( x,y // x,u & z,t // z,u ) by A20, Th36; hence ex u being Element of (Af POS) st ( x,y // x,u & z,t // z,u ) ; ::_thesis: verum end; A21: now__::_thesis:_for_x,_y,_z,_t_being_Element_of_(Af_POS)_st_z,x_//_x,t_&_x_<>_z_holds_ ex_u_being_Element_of_(Af_POS)_st_ (_y,x_//_x,u_&_y,z_//_t,u_) let x, y, z, t be Element of (Af POS); ::_thesis: ( z,x // x,t & x <> z implies ex u being Element of (Af POS) st ( y,x // x,u & y,z // t,u ) ) assume that A22: z,x // x,t and A23: x <> z ; ::_thesis: ex u being Element of (Af POS) st ( y,x // x,u & y,z // t,u ) reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS ; z9,x9 // x9,t9 by A22, Th36; then consider u9 being Element of POS such that A24: ( y9,x9 // x9,u9 & y9,z9 // t9,u9 ) by A11, A23; reconsider u = u9 as Element of (Af POS) ; ( y,x // x,u & y,z // t,u ) by A24, Th36; hence ex u being Element of (Af POS) st ( y,x // x,u & y,z // t,u ) ; ::_thesis: verum end; A25: now__::_thesis:_for_x,_y,_z_being_Element_of_(Af_POS)_ex_t_being_Element_of_(Af_POS)_st_ (_x,y_//_z,t_&_x,z_//_y,t_) let x, y, z be Element of (Af POS); ::_thesis: ex t being Element of (Af POS) st ( x,y // z,t & x,z // y,t ) reconsider x9 = x, y9 = y, z9 = z as Element of POS ; consider t9 being Element of POS such that A26: ( x9,y9 // z9,t9 & x9,z9 // y9,t9 ) by A11; reconsider t = t9 as Element of (Af POS) ; ( x,y // z,t & x,z // y,t ) by A26, Th36; hence ex t being Element of (Af POS) st ( x,y // z,t & x,z // y,t ) ; ::_thesis: verum end; not for x, y, z being Element of (Af POS) holds x,y // x,z proof consider x, y, z being Element of POS such that A27: not x,y // x,z by A11; reconsider x9 = x, y9 = y, z9 = z as Element of (Af POS) ; not x9,y9 // x9,z9 by A27, Th36; hence not for x, y, z being Element of (Af POS) holds x,y // x,z ; ::_thesis: verum end; hence AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane by A10, A15, A12, A25, A21, A18, DIRAF:46; :: according to ANALMETR:def_9 ::_thesis: ( ( for a, b, c, d, p, q, r, s being Element of POS 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 POS ex x being Element of POS st ( a,b _|_ c,x & c <> x ) ) ) thus for a, b, c, d, p, q, r, s being Element of POS 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 ) ) by A11; ::_thesis: for a, b, c being Element of POS ex x being Element of POS st ( a,b _|_ c,x & c <> x ) thus for a, b, c being Element of POS ex x being Element of POS st ( a,b _|_ c,x & c <> x ) by A11; ::_thesis: verum end; 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 ) proof defpred S1[ set ] means for y being Element of POS st y = $1 holds LIN a,b,y; consider X being Subset of POS such that A1: for x being set holds ( x in X iff ( x in the carrier of POS & S1[x] ) ) from SUBSET_1:sch_1(); take X ; ::_thesis: for x being Element of POS holds ( x in X iff LIN a,b,x ) let x be Element of POS; ::_thesis: ( x in X iff LIN a,b,x ) thus ( x in X implies LIN a,b,x ) by A1; ::_thesis: ( LIN a,b,x implies x in X ) assume LIN a,b,x ; ::_thesis: x in X then for y being Element of POS st y = x holds LIN a,b,y ; hence x in X by A1; ::_thesis: verum end; 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 proof let X1, X2 be Subset of POS; ::_thesis: ( ( for x being Element of POS holds ( x in X1 iff LIN a,b,x ) ) & ( for x being Element of POS holds ( x in X2 iff LIN a,b,x ) ) implies X1 = X2 ) assume that A2: for x being Element of POS holds ( x in X1 iff LIN a,b,x ) and A3: for x being Element of POS holds ( x in X2 iff LIN a,b,x ) ; ::_thesis: X1 = X2 for x being set holds ( x in X1 iff x in X2 ) proof let x be set ; ::_thesis: ( x in X1 iff x in X2 ) thus ( x in X1 implies x in X2 ) ::_thesis: ( x in X2 implies x in X1 ) proof assume A4: x in X1 ; ::_thesis: x in X2 then reconsider x9 = x as Element of POS ; LIN a,b,x9 by A2, A4; hence x in X2 by A3; ::_thesis: verum end; assume A5: x in X2 ; ::_thesis: x in X1 then reconsider x9 = x as Element of POS ; LIN a,b,x9 by A3, A5; hence x in X1 by A2; ::_thesis: verum end; hence X1 = X2 by TARSKI:1; ::_thesis: verum end; 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 ) proof let POS be OrtAfSp; ::_thesis: 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 ) let a, b, c be Element of POS; ::_thesis: 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 ) let a9, b9, c9 be Element of (Af POS); ::_thesis: ( a = a9 & b = b9 & c = c9 implies ( LIN a,b,c iff LIN a9,b9,c9 ) ) assume A1: ( a = a9 & b = b9 & c = c9 ) ; ::_thesis: ( LIN a,b,c iff LIN a9,b9,c9 ) hereby ::_thesis: ( LIN a9,b9,c9 implies LIN a,b,c ) assume LIN a,b,c ; ::_thesis: LIN a9,b9,c9 then a,b // a,c by Def10; then a9,b9 // a9,c9 by A1, Th36; hence LIN a9,b9,c9 by AFF_1:def_1; ::_thesis: verum end; assume LIN a9,b9,c9 ; ::_thesis: LIN a,b,c then a9,b9 // a9,c9 by AFF_1:def_1; then a,b // a,c by A1, Th36; hence LIN a,b,c by Def10; ::_thesis: verum end; 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) proof let POS be OrtAfSp; ::_thesis: 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) let a, b be Element of POS; ::_thesis: for a9, b9 being Element of (Af POS) st a = a9 & b = b9 holds Line (a,b) = Line (a9,b9) let a9, b9 be Element of (Af POS); ::_thesis: ( a = a9 & b = b9 implies Line (a,b) = Line (a9,b9) ) assume A1: ( a = a9 & b = b9 ) ; ::_thesis: Line (a,b) = Line (a9,b9) set X = Line (a,b); set Y = Line (a9,b9); now__::_thesis:_for_x1_being_set_holds_ (_x1_in_Line_(a,b)_iff_x1_in_Line_(a9,b9)_) let x1 be set ; ::_thesis: ( x1 in Line (a,b) iff x1 in Line (a9,b9) ) A2: now__::_thesis:_(_x1_in_Line_(a9,b9)_implies_x1_in_Line_(a,b)_) assume A3: x1 in Line (a9,b9) ; ::_thesis: x1 in Line (a,b) then reconsider x9 = x1 as Element of (Af POS) ; reconsider x = x9 as Element of POS ; LIN a9,b9,x9 by A3, AFF_1:def_2; then LIN a,b,x by A1, Th40; hence x1 in Line (a,b) by Def11; ::_thesis: verum end; now__::_thesis:_(_x1_in_Line_(a,b)_implies_x1_in_Line_(a9,b9)_) assume A4: x1 in Line (a,b) ; ::_thesis: x1 in Line (a9,b9) then reconsider x = x1 as Element of POS ; reconsider x9 = x as Element of (Af POS) ; LIN a,b,x by A4, Def11; then LIN a9,b9,x9 by A1, Th40; hence x1 in Line (a9,b9) by AFF_1:def_2; ::_thesis: verum end; hence ( x1 in Line (a,b) iff x1 in Line (a9,b9) ) by A2; ::_thesis: verum end; hence Line (a,b) = Line (a9,b9) by TARSKI:1; ::_thesis: verum end; 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 ) proof let POS be OrtAfSp; ::_thesis: 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 ) let X be Subset of the carrier of POS; ::_thesis: for Y being Subset of (Af POS) st X = Y holds ( X is being_line iff Y is being_line ) let Y be Subset of (Af POS); ::_thesis: ( X = Y implies ( X is being_line iff Y is being_line ) ) assume A1: X = Y ; ::_thesis: ( X is being_line iff Y is being_line ) hereby ::_thesis: ( Y is being_line implies X is being_line ) assume X is being_line ; ::_thesis: Y is being_line then consider a, b being Element of POS such that A2: a <> b and A3: X = Line (a,b) by Def12; reconsider a9 = a, b9 = b as Element of (Af POS) ; Y = Line (a9,b9) by A1, A3, Th41; hence Y is being_line by A2, AFF_1:def_3; ::_thesis: verum end; assume Y is being_line ; ::_thesis: X is being_line then consider a9, b9 being Element of (Af POS) such that A4: a9 <> b9 and A5: Y = Line (a9,b9) by AFF_1:def_3; reconsider a = a9, b = b9 as Element of POS ; X = Line (a,b) by A1, A5, Th41; hence X is being_line by A4, Def12; ::_thesis: verum end; 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 ) ) ) proof let POS be non empty ParOrtStr ; ::_thesis: 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 ) ) ) let a, b be Element of POS; ::_thesis: 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 ) ) ) let K, M be Subset of POS; ::_thesis: ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) ) A1: now__::_thesis:_for_a,_b_being_Element_of_POS for_K_being_Subset_of_POS_st_a,b__|__K_holds_ K_is_being_line let a, b be Element of POS; ::_thesis: for K being Subset of POS st a,b _|_ K holds K is being_line let K be Subset of POS; ::_thesis: ( a,b _|_ K implies K is being_line ) assume a,b _|_ K ; ::_thesis: K is being_line then ex p, q being Element of POS st ( p <> q & K = Line (p,q) & a,b _|_ p,q ) by Def13; hence K is being_line by Def12; ::_thesis: verum end; now__::_thesis:_(_K__|__M_implies_(_K_is_being_line_&_M_is_being_line_)_) assume K _|_ M ; ::_thesis: ( K is being_line & M is being_line ) then A2: ex p, q being Element of POS st ( p <> q & K = Line (p,q) & p,q _|_ M ) by Def14; hence K is being_line by Def12; ::_thesis: M is being_line thus M is being_line by A1, A2; ::_thesis: verum end; hence ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) ) by A1; ::_thesis: verum end; 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 ) ) proof let POS be non empty ParOrtStr ; ::_thesis: 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 ) ) let K, M be Subset of POS; ::_thesis: ( 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 ) ) hereby ::_thesis: ( 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 ) implies K _|_ M ) assume K _|_ M ; ::_thesis: 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 ) then consider a, b being Element of POS such that A1: ( a <> b & K = Line (a,b) ) and A2: a,b _|_ M by Def14; ex c, d being Element of POS st ( c <> d & M = Line (c,d) & a,b _|_ c,d ) by A2, Def13; hence 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 ) by A1; ::_thesis: verum end; given a, b, c, d being Element of POS such that A3: a <> b and A4: c <> d and A5: K = Line (a,b) and A6: ( M = Line (c,d) & a,b _|_ c,d ) ; ::_thesis: K _|_ M a,b _|_ M by A4, A6, Def13; hence K _|_ M by A3, A5, Def14; ::_thesis: verum end; 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 ) proof let POS be OrtAfSp; ::_thesis: 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 ) let M, N be Subset of POS; ::_thesis: for M9, N9 being Subset of (Af POS) st M = M9 & N = N9 holds ( M // N iff M9 // N9 ) let M9, N9 be Subset of (Af POS); ::_thesis: ( M = M9 & N = N9 implies ( M // N iff M9 // N9 ) ) assume A1: ( M = M9 & N = N9 ) ; ::_thesis: ( M // N iff M9 // N9 ) hereby ::_thesis: ( M9 // N9 implies M // N ) assume M // N ; ::_thesis: M9 // N9 then consider a, b, c, d being Element of POS such that A2: ( a <> b & c <> d ) and A3: ( M = Line (a,b) & N = Line (c,d) ) and A4: a,b // c,d by Def15; reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ; A5: a9,b9 // c9,d9 by A4, Th36; ( M9 = Line (a9,b9) & N9 = Line (c9,d9) ) by A1, A3, Th41; hence M9 // N9 by A2, A5, AFF_1:37; ::_thesis: verum end; assume M9 // N9 ; ::_thesis: M // N then consider a9, b9, c9, d9 being Element of (Af POS) such that A6: ( a9 <> b9 & c9 <> d9 ) and A7: a9,b9 // c9,d9 and A8: ( M9 = Line (a9,b9) & N9 = Line (c9,d9) ) by AFF_1:37; reconsider a = a9, b = b9, c = c9, d = d9 as Element of POS ; A9: a,b // c,d by A7, Th36; ( M = Line (a,b) & N = Line (c,d) ) by A1, A8, Th41; hence M // N by A6, A9, Def15; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: for K being Subset of POS for a being Element of POS st K is being_line holds a,a _|_ K let K be Subset of POS; ::_thesis: for a being Element of POS st K is being_line holds a,a _|_ K let a be Element of POS; ::_thesis: ( K is being_line implies a,a _|_ K ) assume K is being_line ; ::_thesis: a,a _|_ K then consider p, q being Element of POS such that A1: ( p <> q & K = Line (p,q) ) by Def12; p,q _|_ a,a by Def8; then a,a _|_ p,q by Def8; hence a,a _|_ K by A1, Def13; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: 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 let K be Subset of POS; ::_thesis: 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 let a, b, c, d be Element of POS; ::_thesis: ( a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b implies c,d _|_ K ) assume that A1: a,b _|_ K and A2: ( a,b // c,d or c,d // a,b ) and A3: a <> b ; ::_thesis: c,d _|_ K reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ; consider p, q being Element of POS such that A4: ( p <> q & K = Line (p,q) ) and A5: a,b _|_ p,q by A1, Def13; ( a9,b9 // c9,d9 or c9,d9 // a9,b9 ) by A2, Th36; then a9,b9 // c9,d9 by AFF_1:4; then a,b // c,d by Th36; then p,q _|_ c,d by A3, A5, Def8; then c,d _|_ p,q by Def8; hence c,d _|_ K by A4, Def13; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: for K being Subset of POS for a, b being Element of POS st a,b _|_ K holds b,a _|_ K let K be Subset of POS; ::_thesis: for a, b being Element of POS st a,b _|_ K holds b,a _|_ K let a, b be Element of POS; ::_thesis: ( a,b _|_ K implies b,a _|_ K ) assume a,b _|_ K ; ::_thesis: b,a _|_ K then consider p, q being Element of POS such that A1: ( p <> q & K = Line (p,q) ) and A2: a,b _|_ p,q by Def13; p,q _|_ a,b by A2, Def8; then p,q _|_ b,a by Def8; then b,a _|_ p,q by Def8; hence b,a _|_ K by A1, Def13; ::_thesis: verum end; 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) proof let K, M be Subset of POS; ::_thesis: ( (POS,K,M) implies (POS,M,K) ) assume K // M ; ::_thesis: (POS,M,K) then consider a, b, c, d being Element of POS such that A1: ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) ) and A2: a,b // c,d by Def15; reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ; a9,b9 // c9,d9 by A2, Th36; then c9,d9 // a9,b9 by AFF_1:4; then c,d // a,b by Th36; hence (POS,M,K) by A1, Def15; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: for K, M being Subset of POS for r, s being Element of POS st r,s _|_ K & K // M holds r,s _|_ M let K, M be Subset of POS; ::_thesis: for r, s being Element of POS st r,s _|_ K & K // M holds r,s _|_ M let r, s be Element of POS; ::_thesis: ( r,s _|_ K & K // M implies r,s _|_ M ) assume that A1: r,s _|_ K and A2: K // M ; ::_thesis: r,s _|_ M consider p, q being Element of POS such that A3: p <> q and A4: K = Line (p,q) and A5: r,s _|_ p,q by A1, Def13; consider a, b, c, d being Element of POS such that A6: a <> b and A7: c <> d and A8: K = Line (a,b) and A9: M = Line (c,d) and A10: a,b // c,d by A2, Def15; reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ; A11: K = Line (a9,b9) by A8, Th41; A12: K = Line (p9,q9) by A4, Th41; then q9 in K by AFF_1:15; then A13: LIN a9,b9,q9 by A11, AFF_1:def_2; p9 in K by A12, AFF_1:15; then LIN a9,b9,p9 by A11, AFF_1:def_2; then A14: a9,b9 // p9,q9 by A13, AFF_1:10; A15: p,q _|_ r,s by A5, Def8; a9,b9 // c9,d9 by A10, Th36; then p9,q9 // c9,d9 by A6, A14, AFF_1:5; then p,q // c,d by Th36; then r,s _|_ c,d by A3, A15, Def8; hence r,s _|_ M by A7, A9, Def13; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: 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 let K be Subset of POS; ::_thesis: for a, b being Element of POS st a in K & b in K & a,b _|_ K holds a = b let a, b be Element of POS; ::_thesis: ( a in K & b in K & a,b _|_ K implies a = b ) assume that A1: a in K and A2: b in K and A3: a,b _|_ K ; ::_thesis: a = b consider p, q being Element of POS such that A4: p <> q and A5: K = Line (p,q) and A6: a,b _|_ p,q by A3, Def13; reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of (Af POS) ; set K9 = Line (p9,q9); b9 in Line (p9,q9) by A2, A5, Th41; then A7: LIN p9,q9,b9 by AFF_1:def_2; a9 in Line (p9,q9) by A1, A5, Th41; then LIN p9,q9,a9 by AFF_1:def_2; then p9,q9 // a9,b9 by A7, AFF_1:10; then A8: p,q // a,b by Th36; p,q _|_ a,b by A6, Def8; then a,b _|_ a,b by A4, A8, Def8; hence a = b by Def8; ::_thesis: verum end; 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) proof let K be Subset of POS; ::_thesis: (POS,K,K) assume (POS,K,K) ; ::_thesis: contradiction then consider a, b being Element of POS such that A1: a <> b and A2: K = Line (a,b) and A3: a,b _|_ K by Def14; reconsider a9 = a, b9 = b as Element of (Af POS) ; K = Line (a9,b9) by A2, Th41; then ( a in K & b in K ) by AFF_1:15; hence contradiction by A1, A3, Th51; ::_thesis: verum end; symmetry for K, M being Subset of POS st (POS,b1,b2) holds (POS,b2,b1) proof let K, M be Subset of POS; ::_thesis: ( (POS,K,M) implies (POS,M,K) ) assume K _|_ M ; ::_thesis: (POS,M,K) then consider a, b, c, d being Element of POS such that A4: ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) ) and A5: a,b _|_ c,d by Th45; c,d _|_ a,b by A5, Def8; hence (POS,M,K) by A4, Th45; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: for K, M, N being Subset of POS st K _|_ M & K // N holds N _|_ M let K, M, N be Subset of POS; ::_thesis: ( K _|_ M & K // N implies N _|_ M ) assume that A1: K _|_ M and A2: K // N ; ::_thesis: N _|_ M consider r, s being Element of POS such that A3: ( r <> s & M = Line (r,s) ) and A4: r,s _|_ K by A1, Def14; r,s _|_ N by A2, A4, Th50; hence N _|_ M by A3, Def14; ::_thesis: verum end; 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 ) proof let POS be OrtAfSp; ::_thesis: 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 ) let K be Subset of POS; ::_thesis: 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 ) let a, b, c, d be Element of POS; ::_thesis: ( a in K & b in K & c,d _|_ K implies ( c,d _|_ a,b & a,b _|_ c,d ) ) assume that A1: a in K and A2: b in K and A3: c,d _|_ K ; ::_thesis: ( c,d _|_ a,b & a,b _|_ c,d ) consider p, q being Element of POS such that A4: p <> q and A5: K = Line (p,q) and A6: c,d _|_ p,q by A3, Def13; reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of (Af POS) ; LIN p,q,b by A2, A5, Def11; then A7: LIN p9,q9,b9 by Th40; LIN p,q,a by A1, A5, Def11; then LIN p9,q9,a9 by Th40; then p9,q9 // a9,b9 by A7, AFF_1:10; then A8: p,q // a,b by Th36; p,q _|_ c,d by A6, Def8; hence c,d _|_ a,b by A4, A8, Def8; ::_thesis: a,b _|_ c,d hence a,b _|_ c,d by Def8; ::_thesis: verum end; 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) proof let POS be OrtAfSp; ::_thesis: 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) let K be Subset of POS; ::_thesis: 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) let a, b be Element of POS; ::_thesis: ( a in K & b in K & a <> b & K is being_line implies K = Line (a,b) ) assume that A1: ( a in K & b in K & a <> b ) and A2: K is being_line ; ::_thesis: K = Line (a,b) reconsider a9 = a, b9 = b as Element of (Af POS) ; reconsider K9 = K as Subset of (Af POS) ; K9 is being_line by A2, Th43; then K9 = Line (a9,b9) by A1, AFF_1:57; hence K = Line (a,b) by Th41; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: 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 let K be Subset of POS; ::_thesis: 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 let a, b, c, d be Element of POS; ::_thesis: ( a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) implies c,d _|_ K ) assume that A1: ( a in K & b in K ) and A2: a <> b and A3: ( K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) ) ; ::_thesis: c,d _|_ K ( c,d _|_ a,b & K = Line (a,b) ) by A1, A2, A3, Def8, Th54; hence c,d _|_ K by A2, Def13; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: 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 let M, N be Subset of POS; ::_thesis: 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 let a, b, c, d be Element of POS; ::_thesis: ( a in M & b in M & c in N & d in N & M _|_ N implies a,b _|_ c,d ) assume that A1: a in M and A2: b in M and A3: c in N and A4: d in N and A5: M _|_ N ; ::_thesis: a,b _|_ c,d consider p1, q1, p2, q2 being Element of POS such that A6: p1 <> q1 and A7: p2 <> q2 and A8: M = Line (p1,q1) and A9: N = Line (p2,q2) and A10: p1,q1 _|_ p2,q2 by A5, Th45; reconsider a9 = a, b9 = b, c9 = c, d9 = d, p19 = p1, q19 = q1, p29 = p2, q29 = q2 as Element of (Af POS) ; LIN p1,q1,b by A2, A8, Def11; then A11: LIN p19,q19,b9 by Th40; LIN p1,q1,a by A1, A8, Def11; then LIN p19,q19,a9 by Th40; then p19,q19 // a9,b9 by A11, AFF_1:10; then p1,q1 // a,b by Th36; then A12: p2,q2 _|_ a,b by A6, A10, Def8; LIN p2,q2,d by A4, A9, Def11; then A13: LIN p29,q29,d9 by Th40; LIN p2,q2,c by A3, A9, Def11; then LIN p29,q29,c9 by Th40; then p29,q29 // c9,d9 by A13, AFF_1:10; then p2,q2 // c,d by Th36; hence a,b _|_ c,d by A7, A12, Def8; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: 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 let M, N, K, A be Subset of POS; ::_thesis: 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 let p, a, b be Element of POS; ::_thesis: ( 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 implies A _|_ K ) assume that A1: ( p in M & p in N & a in M & b in N ) and A2: a <> b and A3: ( a in K & b in K ) and A4: A _|_ M and A5: A _|_ N and A6: K is being_line ; ::_thesis: A _|_ K A is being_line by A4, Th44; then consider q, r being Element of POS such that A7: q <> r and A8: A = Line (q,r) by Def12; reconsider q9 = q, r9 = r as Element of (Af POS) ; Line (q,r) = Line (q9,r9) by Th41; then ( q in A & r in A ) by A8, AFF_1:15; then ( q,r _|_ p,a & q,r _|_ p,b ) by A1, A4, A5, Th56; then A9: q,r _|_ a,b by Def8; K = Line (a,b) by A2, A3, A6, Th54; hence A _|_ K by A2, A7, A8, A9, Th45; ::_thesis: verum end; 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 ) proof let POS be OrtAfSp; ::_thesis: 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 ) let b, c, a be Element of POS; ::_thesis: ( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c ) reconsider a9 = a, b9 = b, c9 = c as Element of (Af POS) ; thus b,c _|_ a,a by Def8; ::_thesis: ( a,a _|_ b,c & b,c // a,a & a,a // b,c ) hence a,a _|_ b,c by Def8; ::_thesis: ( b,c // a,a & a,a // b,c ) ( b9,c9 // a9,a9 & a9,a9 // b9,c9 ) by AFF_1:3; hence ( b,c // a,a & a,a // b,c ) by Th36; ::_thesis: verum end; 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 ) proof let POS be OrtAfSp; ::_thesis: 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 ) let a, b, c, d be Element of POS; ::_thesis: ( a,b // c,d implies ( 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 ) ) reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ; assume a,b // c,d ; ::_thesis: ( 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 ) then A1: a9,b9 // c9,d9 by Th36; then A2: ( b9,a9 // d9,c9 & c9,d9 // a9,b9 ) by AFF_1:4; A3: d9,c9 // b9,a9 by A1, AFF_1:4; A4: ( c9,d9 // b9,a9 & d9,c9 // a9,b9 ) by A1, AFF_1:4; ( a9,b9 // d9,c9 & b9,a9 // c9,d9 ) by A1, AFF_1:4; hence ( 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 ) by A2, A4, A3, Th36; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: 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 let p, q, a, b, c, d be Element of POS; ::_thesis: ( 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 ) ) implies a,b // c,d ) assume that A1: p <> q and A2: ( ( 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 ) ) ; ::_thesis: a,b // c,d reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ; ( ( p9,q9 // a9,b9 & p9,q9 // c9,d9 ) or ( p9,q9 // a9,b9 & c9,d9 // p9,q9 ) or ( a9,b9 // p9,q9 & c9,d9 // p9,q9 ) or ( a9,b9 // p9,q9 & p9,q9 // c9,d9 ) ) by A2, Th36; then a9,b9 // c9,d9 by A1, AFF_1:5; hence a,b // c,d by Th36; ::_thesis: verum end; 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 ) proof let POS be OrtAfSp; ::_thesis: 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 ) let a, b, c, d be Element of POS; ::_thesis: ( a,b _|_ c,d implies ( 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 ) ) assume A1: a,b _|_ c,d ; ::_thesis: ( 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 ) then a,b _|_ d,c by Def8; then A2: d,c _|_ a,b by Def8; then d,c _|_ b,a by Def8; then b,a _|_ d,c by Def8; then b,a _|_ c,d by Def8; hence ( 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 ) by A1, A2, Def8; ::_thesis: verum end; 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 proof let POS be OrtAfSp; ::_thesis: 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 let p, q, a, b, c, d be Element of POS; ::_thesis: ( 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 ) ) implies a,b _|_ c,d ) assume that A1: p <> q and A2: ( ( 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 ) ) ; ::_thesis: a,b _|_ c,d A3: now__::_thesis:_(_(_(_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_)_)_implies_a,b__|__c,d_) assume ( ( 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 ) ) ; ::_thesis: a,b _|_ c,d then ( p,q // a,b & p,q _|_ c,d ) by Th59, Th61; then c,d _|_ a,b by A1, Def8; hence a,b _|_ c,d by Th61; ::_thesis: verum end; now__::_thesis:_(_(_(_p,q_//_c,d_&_p,q__|__a,b_)_or_(_p,q_//_c,d_&_a,b__|__p,q_)_or_(_c,d_//_p,q_&_a,b__|__p,q_)_or_(_c,d_//_p,q_&_p,q__|__a,b_)_)_implies_a,b__|__c,d_) assume ( ( p,q // c,d & p,q _|_ a,b ) or ( p,q // c,d & a,b _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( c,d // p,q & p,q _|_ a,b ) ) ; ::_thesis: a,b _|_ c,d then ( p,q // c,d & p,q _|_ a,b ) by Th59, Th61; hence a,b _|_ c,d by A1, Def8; ::_thesis: verum end; hence a,b _|_ c,d by A2, A3; ::_thesis: verum end; 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 proof let POS be OrtAfPl; ::_thesis: 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 let p, q, a, b, c, d be Element of POS; ::_thesis: ( 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 ) ) implies a,b // c,d ) assume that A1: p <> q and A2: ( ( 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 ) ) ; ::_thesis: a,b // c,d ( p,q _|_ a,b & p,q _|_ c,d ) by A2, Th61; hence a,b // c,d by A1, Def9; ::_thesis: verum end; 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 proof let POS be OrtAfPl; ::_thesis: 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 let M, N be Subset of POS; ::_thesis: 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 let a, b, c, d be Element of POS; ::_thesis: ( 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 implies M // N ) assume that A1: ( a in M & b in M ) and A2: a <> b and A3: ( M is being_line & c in N & d in N ) and A4: c <> d and A5: N is being_line and A6: a,b // c,d ; ::_thesis: M // N ( M = Line (a,b) & N = Line (c,d) ) by A1, A2, A3, A4, A5, Th54; hence M // N by A2, A4, A6, Def15; ::_thesis: verum end; theorem :: ANALMETR:65 for POS being OrtAfPl for M, K, N being Subset of POS st M _|_ K & N _|_ K holds M // N proof let POS be OrtAfPl; ::_thesis: for M, K, N being Subset of POS st M _|_ K & N _|_ K holds M // N let M, K, N be Subset of POS; ::_thesis: ( M _|_ K & N _|_ K implies M // N ) assume that A1: M _|_ K and A2: N _|_ K ; ::_thesis: M // N consider p1, q1, a, b being Element of POS such that A3: p1 <> q1 and A4: a <> b and A5: K = Line (p1,q1) and A6: M = Line (a,b) and A7: p1,q1 _|_ a,b by A1, Th45; consider p2, q2, c, d being Element of POS such that A8: p2 <> q2 and A9: c <> d and A10: K = Line (p2,q2) and A11: N = Line (c,d) and A12: p2,q2 _|_ c,d by A2, Th45; reconsider p19 = p1, p29 = p2, q19 = q1, q29 = q2 as Element of (Af POS) ; A13: Line (p19,q19) = Line (p2,q2) by A5, A10, Th41 .= Line (p29,q29) by Th41 ; then q29 in Line (p19,q19) by AFF_1:15; then A14: LIN p19,q19,q29 by AFF_1:def_2; p29 in Line (p19,q19) by A13, AFF_1:15; then LIN p19,q19,p29 by AFF_1:def_2; then p19,q19 // p29,q29 by A14, AFF_1:10; then p1,q1 // p2,q2 by Th36; then a,b _|_ p2,q2 by A3, A7, Th62; then a,b // c,d by A8, A12, Th63; hence M // N by A4, A6, A9, A11, Def15; ::_thesis: verum end; 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 ) proof let POS be OrtAfPl; ::_thesis: for M, N being Subset of POS st M _|_ N holds ex p being Element of POS st ( p in M & p in N ) let M, N be Subset of POS; ::_thesis: ( M _|_ N implies ex p being Element of POS st ( p in M & p in N ) ) reconsider M9 = M, N9 = N as Subset of (Af POS) ; assume A1: M _|_ N ; ::_thesis: ex p being Element of POS st ( p in M & p in N ) then M is being_line by Th44; then A2: M9 is being_line by Th43; N is being_line by A1, Th44; then A3: N9 is being_line by Th43; not M // N by A1, Th52; then not M9 // N9 by Th46; hence ex p being Element of POS st ( p in M & p in N ) by A2, A3, AFF_1:58; ::_thesis: verum end; 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 ) proof let POS be OrtAfPl; ::_thesis: 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 ) let a, b, c, d be Element of POS; ::_thesis: ( a,b _|_ c,d implies ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) ) reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ; assume A1: a,b _|_ c,d ; ::_thesis: ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) A2: now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_ex_p_being_Element_of_POS_st_ (_LIN_a,b,p_&_LIN_c,d,p_)_) set M = Line (a,b); set N = Line (c,d); assume ( a <> b & c <> d ) ; ::_thesis: ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) then Line (a,b) _|_ Line (c,d) by A1, Th45; then consider p being Element of POS such that A3: ( p in Line (a,b) & p in Line (c,d) ) by Th66; ( LIN a,b,p & LIN c,d,p ) by A3, Def11; hence ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) ; ::_thesis: verum end; LIN a9,b9,a9 by AFF_1:7; then A4: LIN a,b,a by Th40; A5: now__::_thesis:_(_c_=_d_implies_ex_p_being_Element_of_POS_st_ (_LIN_a,b,p_&_LIN_c,d,p_)_) assume c = d ; ::_thesis: ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) then c,d // c,a by Th58; then LIN c,d,a by Def10; hence ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) by A4; ::_thesis: verum end; LIN c9,d9,c9 by AFF_1:7; then A6: LIN c,d,c by Th40; now__::_thesis:_(_a_=_b_implies_ex_p_being_Element_of_POS_st_ (_LIN_a,b,p_&_LIN_c,d,p_)_) assume a = b ; ::_thesis: ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) then a,b // a,c by Th58; then LIN a,b,c by Def10; hence ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) by A6; ::_thesis: verum end; hence ex p being Element of POS st ( LIN a,b,p & LIN c,d,p ) by A5, A2; ::_thesis: verum end; 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 ) proof let POS be OrtAfPl; ::_thesis: 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 ) let K be Subset of POS; ::_thesis: 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 ) let a, b be Element of POS; ::_thesis: ( a,b _|_ K implies ex p being Element of POS st ( LIN a,b,p & p in K ) ) assume a,b _|_ K ; ::_thesis: ex p being Element of POS st ( LIN a,b,p & p in K ) then consider p, q being Element of POS such that p <> q and A1: K = Line (p,q) and A2: a,b _|_ p,q by Def13; consider c being Element of POS such that A3: LIN a,b,c and A4: LIN p,q,c by A2, Th67; c in K by A1, A4, Def11; hence ex p being Element of POS st ( LIN a,b,p & p in K ) by A3; ::_thesis: verum end; 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 ) proof let POS be OrtAfPl; ::_thesis: for a, p, q being Element of POS ex x being Element of POS st ( a,x _|_ p,q & LIN p,q,x ) let a, p, q be Element of POS; ::_thesis: ex x being Element of POS st ( a,x _|_ p,q & LIN p,q,x ) A1: now__::_thesis:_(_p_<>_q_implies_ex_x_being_Element_of_POS_st_ (_a,x__|__p,q_&_LIN_p,q,x_)_) assume p <> q ; ::_thesis: ex x being Element of POS st ( a,x _|_ p,q & LIN p,q,x ) then consider x being Element of POS such that A2: ( p,q // p,x & p,q _|_ x,a ) by Def8; take x = x; ::_thesis: ( a,x _|_ p,q & LIN p,q,x ) thus ( a,x _|_ p,q & LIN p,q,x ) by A2, Def10, Th61; ::_thesis: verum end; now__::_thesis:_(_p_=_q_implies_ex_x_being_Element_of_POS_st_ (_a,x__|__p,q_&_LIN_p,q,x_)_) assume A3: p = q ; ::_thesis: ex x being Element of POS st ( a,x _|_ p,q & LIN p,q,x ) take x = a; ::_thesis: ( a,x _|_ p,q & LIN p,q,x ) p,q // p,a by A3, Th58; hence ( a,x _|_ p,q & LIN p,q,x ) by Def10, Th58; ::_thesis: verum end; hence ex x being Element of POS st ( a,x _|_ p,q & LIN p,q,x ) by A1; ::_thesis: verum end; 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 ) proof let POS be OrtAfPl; ::_thesis: 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 ) let K be Subset of POS; ::_thesis: 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 ) let a be Element of POS; ::_thesis: ( K is being_line implies ex x being Element of POS st ( a,x _|_ K & x in K ) ) assume K is being_line ; ::_thesis: ex x being Element of POS st ( a,x _|_ K & x in K ) then consider p, q being Element of POS such that A1: p <> q and A2: K = Line (p,q) by Def12; consider x being Element of POS such that A3: a,x _|_ p,q and A4: LIN p,q,x by Th69; take x ; ::_thesis: ( a,x _|_ K & x in K ) thus a,x _|_ K by A1, A2, A3, Def13; ::_thesis: x in K thus x in K by A2, A4, Def11; ::_thesis: verum end;