:: AFVECT01 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let A be non empty set ;
let C be Relation of [:A,A:];
cluster AffinStruct(# A,C #) -> non empty ;
coherence
not AffinStruct(# A,C #) is empty by STRUCT_0:def 1;
end;

Lm1: for AFV being WeakAffVect
for a, b, c being Element of AFV st a,b '||' b,c & a <> c holds
a,b // b,c
proof end;

Lm2: for AFV being WeakAffVect
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 ) )
proof end;

Lm3: for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b '||' c,d holds
b,a '||' c,d
proof end;

Lm4: for AFV being WeakAffVect
for a, b being Element of AFV holds a,b '||' b,a
proof end;

Lm5: for AFV being WeakAffVect
for a, b, p being Element of AFV st a,b '||' p,p holds
a = b
proof end;

Lm6: for AFV being WeakAffVect
for a, b, c, d, p, q being Element of AFV st a,b '||' p,q & c,d '||' p,q holds
a,b '||' c,d
proof end;

Lm7: for AFV being WeakAffVect
for a, c being Element of AFV ex b being Element of AFV st a,b '||' b,c
proof end;

Lm8: for AFV being WeakAffVect
for a, a', b, b', p being Element of AFV st a <> a' & b <> b' & p,a '||' p,a' & p,b '||' p,b' holds
a,b '||' a',b'
proof end;

Lm9: for AFV being WeakAffVect
for a, b being Element of AFV holds
( a = b or ex c being Element of AFV st
( ( a <> c & a,b '||' b,c ) or ex p, p' being Element of AFV st
( p <> p' & a,b '||' p,p' & a,p '||' p,b & a,p' '||' p',b ) ) )
proof end;

Lm10: for AFV being WeakAffVect
for a, b, b', p, p', c being Element of AFV st a,b '||' b,c & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' holds
a,b' '||' b',c
proof end;

Lm11: for AFV being WeakAffVect
for a, b, b', c being Element of AFV st a <> c & b <> b' & a,b '||' b,c & a,b' '||' b',c holds
ex p, p' being Element of AFV st
( p <> p' & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' )
proof end;

Lm12: for AFV being WeakAffVect
for a, b, c, p, p', q, q' being Element of AFV st a,b '||' p,p' & a,c '||' q,q' & a,p '||' p,b & a,q '||' q,c & a,p' '||' p',b & a,q' '||' q',c holds
ex r, r' being Element of AFV st
( b,c '||' r,r' & b,r '||' r,c & b,r' '||' r',c )
proof end;

consider AFV0 being WeakAffVect;

set X = the carrier of AFV0;

set XX = [:the carrier of AFV0,the carrier of AFV0:];

defpred S1[ set , set ] means ex a, b, c, d being Element of the carrier of AFV0 st
( $1 = [a,b] & $2 = [c,d] & a,b '||' c,d );

consider P being Relation of [:the carrier of AFV0,the carrier of AFV0:],[:the carrier of AFV0,the carrier of AFV0:] such that
Lm13: for x, y being set holds
( [x,y] in P iff ( x in [:the carrier of AFV0,the carrier of AFV0:] & y in [:the carrier of AFV0,the carrier of AFV0:] & S1[x,y] ) ) from RELSET_1:sch 1( [:the carrier of AFV0,the carrier of AFV0:] [:the carrier of AFV0,the carrier of AFV0:] );

Lm14: for a, b, c, d being Element of the carrier of AFV0 holds
( [[a,b],[c,d]] in P iff a,b '||' c,d )
proof end;

set WAS = AffinStruct(# the carrier of AFV0,P #);

Lm15: for a, b, c, d being Element of AFV0
for a', b', c', d' being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a = a' & b = b' & c = c' & d = d' holds
( a,b '||' c,d iff a',b' // c',d' )
proof end;

Lm16: now
thus ex a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a' <> b' by REALSET2:def 7; :: thesis: ( ( for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) holds a',b' // b',a' ) & ( for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a',b' // a',a' holds
a' = b' ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of AFV0,P #) ex b being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
thus for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) holds a',b' // b',a' :: thesis: ( ( for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a',b' // a',a' holds
a' = b' ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of AFV0,P #) ex b being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
proof
let a', b' be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: a',b' // b',a'
reconsider a = a', b = b' as Element of the carrier of AFV0 ;
a,b '||' b,a by Lm4;
hence a',b' // b',a' by Lm15; :: thesis: verum
end;
thus for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a',b' // a',a' holds
a' = b' :: thesis: ( ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of AFV0,P #) ex b being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
proof
let a', b' be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ( a',b' // a',a' implies a' = b' )
assume A1: a',b' // a',a' ; :: thesis: a' = b'
reconsider a = a', b = b' as Element of AFV0 ;
a,b '||' a,a by A1, Lm15;
hence a' = b' by Lm5; :: thesis: verum
end;
thus for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d :: thesis: ( ( for a, c being Element of AffinStruct(# the carrier of AFV0,P #) ex b being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
proof
let a, b, c, d, p, q be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ( a,b // p,q & c,d // p,q implies a,b // c,d )
assume A2: ( a,b // p,q & c,d // p,q ) ; :: thesis: a,b // c,d
reconsider a1 = a, b1 = b, c1 = c, d1 = d, p1 = p, q1 = q as Element of AFV0 ;
( a1,b1 '||' p1,q1 & c1,d1 '||' p1,q1 ) by A2, Lm15;
then a1,b1 '||' c1,d1 by Lm6;
hence a,b // c,d by Lm15; :: thesis: verum
end;
thus for a, c being Element of AffinStruct(# the carrier of AFV0,P #) ex b being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c :: thesis: ( ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
proof
let a, c be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ex b being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c
reconsider a1 = a, c1 = c as Element of AFV0 ;
consider b1 being Element of AFV0 such that
A3: a1,b1 '||' b1,c1 by Lm7;
reconsider b = b1 as Element of AffinStruct(# the carrier of AFV0,P #) ;
a,b // b,c by A3, Lm15;
hence ex b being Element of the carrier of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ; :: thesis: verum
end;
thus for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' :: thesis: ( ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
proof
let a, a', b, b', p be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ( a <> a' & b <> b' & p,a // p,a' & p,b // p,b' implies a,b // a',b' )
assume that
A4: ( a <> a' & b <> b' ) and
A5: ( p,a // p,a' & p,b // p,b' ) ; :: thesis: a,b // a',b'
reconsider a1 = a, a1' = a', b1 = b, b1' = b', p1 = p as Element of AFV0 ;
( p1,a1 '||' p1,a1' & p1,b1 '||' p1,b1' ) by A5, Lm15;
then a1,b1 '||' a1',b1' by A4, Lm8;
hence a,b // a',b' by Lm15; :: thesis: verum
end;
thus for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) :: thesis: ( ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
proof
let a, b be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) )
assume A6: not a = b ; :: thesis: ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) )
reconsider a1 = a, b1 = b as Element of AFV0 ;
A7: now
given c1 being Element of AFV0 such that A8: ( a1 <> c1 & a1,b1 '||' b1,c1 ) ; :: thesis: ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( a <> c & a,b // b,c )
reconsider c = c1 as Element of AffinStruct(# the carrier of AFV0,P #) ;
( a <> c & a,b // b,c ) by A8, Lm15;
hence ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( a <> c & a,b // b,c ) ; :: thesis: verum
end;
now
given p1, p1' being Element of AFV0 such that A9: ( p1 <> p1' & a1,b1 '||' p1,p1' & a1,p1 '||' p1,b1 & a1,p1' '||' p1',b1 ) ; :: thesis: ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b )
reconsider p = p1, p' = p1' as Element of AffinStruct(# the carrier of AFV0,P #) ;
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) by A9, Lm15;
hence ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ; :: thesis: verum
end;
hence ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) by A6, A7, Lm9; :: thesis: verum
end;
thus for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c :: thesis: ( ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
proof
let a, b, b', p, p', c be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ( a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' implies a,b' // b',c )
assume A10: ( a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ; :: thesis: a,b' // b',c
reconsider a1 = a, b1 = b, b1' = b', p1 = p, p1' = p', c1 = c as Element of AFV0 ;
( a1,b1 '||' b1,c1 & b1,b1' '||' p1,p1' & b1,p1 '||' p1,b1' & b1,p1' '||' p1',b1' ) by A10, Lm15;
then a1,b1' '||' b1',c1 by Lm10;
hence a,b' // b',c by Lm15; :: thesis: verum
end;
thus for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) :: thesis: for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c )
proof
let a, b, b', c be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ( a <> c & b <> b' & a,b // b,c & a,b' // b',c implies ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) )
assume that
A11: ( a <> c & b <> b' ) and
A12: ( a,b // b,c & a,b' // b',c ) ; :: thesis: ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' )
reconsider a1 = a, b1 = b, b1' = b', c1 = c as Element of the carrier of AFV0 ;
( a1,b1 '||' b1,c1 & a1,b1' '||' b1',c1 ) by A12, Lm15;
then consider p1, p1' being Element of AFV0 such that
A13: ( p1 <> p1' & b1,b1' '||' p1,p1' & b1,p1 '||' p1,b1' & b1,p1' '||' p1',b1' ) by A11, Lm11;
reconsider p = p1, p' = p1' as Element of AffinStruct(# the carrier of AFV0,P #) ;
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) by A13, Lm15;
hence ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ; :: thesis: verum
end;
thus for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) :: thesis: verum
proof
let a, b, c, p, p', q, q' be Element of AffinStruct(# the carrier of AFV0,P #); :: thesis: ( a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c implies ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) )
assume A14: ( a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c ) ; :: thesis: ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c )
reconsider a1 = a, b1 = b, c1 = c, p1 = p, p1' = p', q1 = q, q1' = q' as Element of the carrier of AFV0 ;
( a1,b1 '||' p1,p1' & a1,c1 '||' q1,q1' & a1,p1 '||' p1,b1 & a1,q1 '||' q1,c1 & a1,p1' '||' p1',b1 & a1,q1' '||' q1',c1 ) by A14, Lm15;
then consider r1, r1' being Element of AFV0 such that
A15: ( b1,c1 '||' r1,r1' & b1,r1 '||' r1,c1 & b1,r1' '||' r1',c1 ) by Lm12;
reconsider r = r1, r' = r1' as Element of AffinStruct(# the carrier of AFV0,P #) ;
( b,c // r,r' & b,r // r,c & b,r' // r',c ) by A15, Lm15;
hence ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ; :: thesis: verum
end;
end;

definition
let IT be non empty AffinStruct ;
canceled;
attr IT is WeakAffSegm-like means :Def2: :: AFVECT01:def 2
( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b being Element of IT st a,b // a,a holds
a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, a', b, b', p being Element of IT st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of IT holds
( a = b or ex c being Element of IT st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of IT st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of IT st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of IT st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of IT st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of IT st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of IT st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) );
end;

:: deftheorem AFVECT01:def 1 :
canceled;

:: deftheorem Def2 defines WeakAffSegm-like AFVECT01:def 2 :
for IT being non empty AffinStruct holds
( IT is WeakAffSegm-like iff ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b being Element of IT st a,b // a,a holds
a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, a', b, b', p being Element of IT st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of IT holds
( a = b or ex c being Element of IT st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of IT st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of IT st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of IT st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of IT st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of IT st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of IT st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) ) );

registration
cluster non empty non trivial strict WeakAffSegm-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & not b1 is trivial & b1 is WeakAffSegm-like )
proof end;
end;

definition
mode WeakAffSegm is non empty non trivial WeakAffSegm-like AffinStruct ;
end;

theorem Th1: :: AFVECT01:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b being Element of AFV holds a,b // a,b
proof end;

theorem Th2: :: AFVECT01:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b, c, d being Element of AFV st a,b // c,d holds
c,d // a,b
proof end;

theorem Th3: :: AFVECT01:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b, c, d being Element of AFV st a,b // c,d holds
a,b // d,c
proof end;

theorem Th4: :: AFVECT01:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // c,d
proof end;

theorem Th5: :: AFVECT01:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b being Element of AFV holds a,a // b,b
proof end;

theorem Th6: :: AFVECT01:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b, c being Element of AFV st a,b // c,c holds
a = b
proof end;

theorem Th7: :: AFVECT01:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b, p, p', c being Element of AFV st a,b // p,p' & a,b // b,c & a,p // p,b & a,p' // p',b holds
a = c
proof end;

theorem :: AFVECT01:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b', b'', b being Element of AFV st a,b' // a,b'' & a,b // a,b'' & not b = b' & not b = b'' holds
b' = b''
proof end;

definition
let AFV be WeakAffSegm;
let a, b be Element of AFV;
canceled;
pred MDist a,b means :Def4: :: AFVECT01:def 4
 ex p, p' being Element of AFV st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b );
end;

:: deftheorem AFVECT01:def 3 :
canceled;

:: deftheorem Def4 defines MDist AFVECT01:def 4 :
for AFV being WeakAffSegm
for a, b being Element of AFV holds
( MDist a,b iff ex p, p' being Element of AFV st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) );

definition
let AFV be WeakAffSegm;
let a, b, c be Element of AFV;
pred Mid a,b,c means :: AFVECT01:def 5
( ( a = b & b = c & a = c ) or ( a = c & MDist a,b ) or ( a <> c & a,b // b,c ) );
end;

:: deftheorem defines Mid AFVECT01:def 5 :
for AFV being WeakAffSegm
for a, b, c being Element of AFV holds
( Mid a,b,c iff ( ( a = b & b = c & a = c ) or ( a = c & MDist a,b ) or ( a <> c & a,b // b,c ) ) );

theorem :: AFVECT01:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFVECT01:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFVECT01:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b being Element of AFV st a <> b & not MDist a,b holds
ex c being Element of AFV st
( a <> c & a,b // b,c )
proof end;

theorem :: AFVECT01:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b, c being Element of AFV st MDist a,b & a,b // b,c holds
a = c
proof end;

theorem :: AFVECT01:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AFV being WeakAffSegm
for a, b being Element of AFV st MDist a,b holds
a <> b
proof end;