let V be RealLinearSpace; :: thesis: for u, u1, v, v1, x, y being VECTOR of V st Gen x,y holds
( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) )
let u, u1, v, v1, x, y be VECTOR of V; :: thesis: ( Gen x,y implies ( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) ) )
assume A1: Gen x,y ; :: thesis: ( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) )
A2: now :: thesis: ( u = v implies u,v,u1,v1 are_Ort_wrt x,y )
assume u = v ; :: thesis: u,v,u1,v1 are_Ort_wrt x,y
then v - u = 0. V by RLVECT_1:15;
then v - u,v1 - u1 are_Ort_wrt x,y by A1, ANALMETR:5;
hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3; :: thesis: verum
end;
now :: thesis: ( u <> v implies ( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) ) )
assume A3: u <> v ; :: thesis: ( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) )
set u2 = Orte (x,y,u);
set v2 = Orte (x,y,v);
A4: v - u <> 0. V by A3, RLVECT_1:21;
u,v, Orte (x,y,u), Orte (x,y,v) are_Ort_wrt x,y by A1, Th24;
then A5: v - u,(Orte (x,y,v)) - (Orte (x,y,u)) are_Ort_wrt x,y by ANALMETR:def 3;
A6: now :: thesis: ( not u,v,u1,v1 are_Ort_wrt x,y or u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y )
assume u,v,u1,v1 are_Ort_wrt x,y ; :: thesis: ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y )
then v - u,v1 - u1 are_Ort_wrt x,y by ANALMETR:def 3;
then ex a, b being Real st
( a * ((Orte (x,y,v)) - (Orte (x,y,u))) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A1, A4, A5, ANALMETR:9;
then ( Orte (x,y,u), Orte (x,y,v) // u1,v1 or Orte (x,y,u), Orte (x,y,v) // v1,u1 ) by ANALMETR:14;
hence ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) ; :: thesis: verum
end;
now :: thesis: ( ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) implies u,v,u1,v1 are_Ort_wrt x,y )
assume ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) ; :: thesis: u,v,u1,v1 are_Ort_wrt x,y
then ( Orte (x,y,u), Orte (x,y,v) // u1,v1 or Orte (x,y,u), Orte (x,y,v) // v1,u1 ) ;
then consider a, b being Real such that
A7: a * ((Orte (x,y,v)) - (Orte (x,y,u))) = b * (v1 - u1) and
A8: ( a <> 0 or b <> 0 ) by ANALMETR:14;
A9: now :: thesis: ( b = 0 implies u,v,u1,v1 are_Ort_wrt x,y )
assume A10: b = 0 ; :: thesis: u,v,u1,v1 are_Ort_wrt x,y
then 0. V = a * ((Orte (x,y,v)) - (Orte (x,y,u))) by A7, RLVECT_1:10;
then (Orte (x,y,v)) - (Orte (x,y,u)) = 0. V by A8, A10, RLVECT_1:11;
then Orte (x,y,v) = Orte (x,y,u) by RLVECT_1:21;
then u = v by A1, Th13;
then v - u = 0. V by RLVECT_1:15;
then v - u,v1 - u1 are_Ort_wrt x,y by A1, ANALMETR:5;
hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3; :: thesis: verum
end;
now :: thesis: ( b <> 0 implies u,v,u1,v1 are_Ort_wrt x,y )
assume A11: b <> 0 ; :: thesis: u,v,u1,v1 are_Ort_wrt x,y
((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) = (b ") * (b * (v1 - u1)) by A7, RLVECT_1:def 7;
then ((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) = ((b ") * b) * (v1 - u1) by RLVECT_1:def 7;
then ((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) = 1 * (v1 - u1) by A11, XCMPLX_0:def 7;
then v1 - u1 = ((b ") * a) * ((Orte (x,y,v)) - (Orte (x,y,u))) by RLVECT_1:def 8;
then v - u,v1 - u1 are_Ort_wrt x,y by A5, ANALMETR:7;
hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3; :: thesis: verum
end;
hence u,v,u1,v1 are_Ort_wrt x,y by A9; :: thesis: verum
end;
hence ( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) ) by A6; :: thesis: verum
end;
hence ( u,v,u1,v1 are_Ort_wrt x,y iff ( u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y ) ) by A2, Th20; :: thesis: verum