:: AFVECT01 semantic presentation

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();

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 STRUCT_0:def 10; :: 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',