let AFV be WeakAffVect; :: thesis: for a, b being Element of AFV holds
( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
let a, b be Element of AFV; :: thesis: ( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
A1: now :: thesis: ( ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) implies a,b // b,a )
given p, q being Element of AFV such that A2: a,b '||' p,q and
A3: a,p '||' p,b and
A4: a,q '||' q,b ; :: thesis: a,b // b,a
now :: thesis: ( a <> b implies a,b // b,a )
A5: now :: thesis: ( MDist p,q implies a,b // b,a )
assume A6: MDist p,q ; :: thesis: a,b // b,a
( a,b // p,q or a,b // q,p ) by A2, DIRAF:def 4;
then MDist a,b by A6, AFVECT0:3, AFVECT0:15;
hence a,b // b,a by AFVECT0:def 2; :: thesis: verum
end;
assume A7: a <> b ; :: thesis: a,b // b,a
then a,q // q,b by A4, Lm1;
then A8: Mid a,q,b by AFVECT0:def 3;
a,p // p,b by A3, A7, Lm1;
then Mid a,p,b by AFVECT0:def 3;
hence a,b // b,a by A8, A9, A5, AFVECT0:20; :: thesis: verum
end;
hence a,b // b,a by AFVECT0:2; :: thesis: verum
end;
now :: thesis: ( a,b // b,a implies ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
assume A10: a,b // b,a ; :: thesis: ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
A11: now :: thesis: ( a <> b implies ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
assume a <> b ; :: thesis: ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
then A12: MDist a,b by A10, AFVECT0:def 2;
consider p being Element of AFV such that
A13: Mid a,p,b by AFVECT0:19;
A14: a,p // p,b by A13, AFVECT0:def 3;
consider q being Element of AFV such that
A15: a,b // p,q by AFVECT0:def 1;
take p = p; :: thesis: ex q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
take q = q; :: thesis: ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
Mid a,q,b by A13, A15, A12, AFVECT0:15, AFVECT0:23;
then a,q // q,b by AFVECT0:def 3;
hence ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A15, A14, DIRAF:def 4; :: thesis: verum
end;
now :: thesis: ( a = b implies ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
assume A16: a = b ; :: thesis: ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
take p = a; :: thesis: ex q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
take q = a; :: thesis: ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
a,b // p,q by A16, AFVECT0:2;
hence ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A16, DIRAF:def 4; :: thesis: verum
end;
hence ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A11; :: thesis: verum
end;
hence ( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) ) by A1; :: thesis: verum