:: AFVECT01 semantic presentation
E1:
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( ( b2,b3 '||' b3,b4 ) implies ( not b2 <> b4 or b2,b3 // b3,b4 ) )
E2:
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
( b2,b3 // b3,b2 iff ex b4, b5 being Element of b1 st
( b2,b3 '||' b4,b5 & b2,b4 '||' b4,b3 & b2,b5 '||' b5,b3 ) )
proof
let c
1 be
WeakAffVect;
let c
2, c
3 be
Element of c
1;
E3:
now
assume E4:
c
2,c
3 // c
3,c
2
;
E5:
now
assume E6:
c
2 = c
3
;
take c
4 = c
2;
take c
5 = c
2;
( c
2,c
3 // c
4,c
5 & c
2,c
4 // c
4,c
3 & c
2,c
5 // c
5,c
3 )
by E6, AFVECT0:3;
hence
( c
2,c
3 '||' c
4,c
5 & c
2,c
4 '||' c
4,c
3 & c
2,c
5 '||' c
5,c
3 )
by DIRAF:def 4;
end;
now
assume E6:
c
2 <> c
3
;
consider c
4 being
Element of c
1 such that E7:
Mid c
2,c
4,c
3
by AFVECT0:24;
consider c
5 being
Element of c
1 such that E8:
c
2,c
3 // c
4,c
5
by AFVECT0:def 1;
MDist c
2,c
3
by E4, E6, AFVECT0:def 2;
then
MDist c
4,c
5
by E8, AFVECT0:19;
then E9:
Mid c
2,c
5,c
3
by E7, AFVECT0:28;
E10:
c
2,c
4 // c
4,c
3
by E7, AFVECT0:def 3;
E11:
c
2,c
5 // c
5,c
3
by E9, AFVECT0:def 3;
take c
6 = c
4;
take c
7 = c
5;
thus
( c
2,c
3 '||' c
6,c
7 & c
2,c
6 '||' c
6,c
3 & c
2,c
7 '||' c
7,c
3 )
by E8, E10, E11, DIRAF:def 4;
end;
hence
ex b
1, b
2 being
Element of c
1 st
( c
2,c
3 '||' b
1,b
2 & c
2,b
1 '||' b
1,c
3 & c
2,b
2 '||' b
2,c
3 )
by E5;
end;
now
given c
4, c
5 being
Element of c
1 such that E4:
( c
2,c
3 '||' c
4,c
5 & c
2,c
4 '||' c
4,c
3 & c
2,c
5 '||' c
5,c
3 )
;
now
assume E5:
c
2 <> c
3
;
then
( c
2,c
4 // c
4,c
3 & c
2,c
5 // c
5,c
3 )
by E4, E1;
then E6:
(
Mid c
2,c
4,c
3 &
Mid c
2,c
5,c
3 )
by AFVECT0:def 3;
now
assume E8:
MDist c
4,c
5
;
( c
2,c
3 // c
4,c
5 or c
2,c
3 // c
5,c
4 )
by E4, DIRAF:def 4;
then
( c
4,c
5 // c
2,c
3 or c
5,c
4 // c
2,c
3 )
by AFVECT0:4;
then
MDist c
2,c
3
by E8, AFVECT0:19;
hence
c
2,c
3 // c
3,c
2
by AFVECT0:def 2;
end;
hence
c
2,c
3 // c
3,c
2
by E6, E7, AFVECT0:25;
end;
hence
c
2,c
3 // c
3,c
2
by AFVECT0:3;
end;
hence
( c
2,c
3 // c
3,c
2 iff ex b
1, b
2 being
Element of c
1 st
( c
2,c
3 '||' b
1,b
2 & c
2,b
1 '||' b
1,c
3 & c
2,b
2 '||' b
2,c
3 ) )
by E3;
end;
E3:
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 '||' b4,b5 implies b3,b2 '||' b4,b5 )
proof
let c
1 be
WeakAffVect;
let c
2, c
3, c
4, c
5 be
Element of c
1;
assume
c
2,c
3 '||' c
4,c
5
;
then
( c
2,c
3 // c
4,c
5 or c
2,c
3 // c
5,c
4 )
by DIRAF:def 4;
then
( c
3,c
2 // c
5,c
4 or c
3,c
2 // c
4,c
5 )
by AFVECT0:8;
hence
c
3,c
2 '||' c
4,c
5
by DIRAF:def 4;
end;
E4:
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds b2,b3 '||' b3,b2
E5:
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( b2,b3 '||' b4,b4 implies b2 = b3 )
E6:
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( ( b2,b3 '||' b6,b7 & b4,b5 '||' b6,b7 ) implies ( b2,b3 '||' b4,b5 ) )
proof
let c
1 be
WeakAffVect;
let c
2, c
3, c
4, c
5, c
6, c
7 be
Element of c
1;
assume
( c
2,c
3 '||' c
6,c
7 & c
4,c
5 '||' c
6,c
7 )
;
then
not ( not ( c
2,c
3 // c
6,c
7 & c
4,c
5 // c
6,c
7 ) & not ( c
2,c
3 // c
6,c
7 & c
4,c
5 // c
7,c
6 ) & not ( c
2,c
3 // c
7,c
6 & c
4,c
5 // c
6,c
7 ) & not ( c
2,c
3 // c
7,c
6 & c
4,c
5 // c
7,c
6 ) )
by DIRAF:def 4;
then
not ( not c
2,c
3 // c
4,c
5 & not ( c
2,c
3 // c
6,c
7 & c
5,c
4 // c
6,c
7 ) & not ( c
2,c
3 // c
7,c
6 & c
5,c
4 // c
7,c
6 ) )
by AFVECT0:8, AFVECT0:def 1;
then
( c
2,c
3 // c
4,c
5 or c
2,c
3 // c
5,c
4 )
by AFVECT0:def 1;
hence
c
2,c
3 '||' c
4,c
5
by DIRAF:def 4;
end;
E7:
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b2,b4 '||' b4,b3
E8:
for b1 being WeakAffVect
for b2, b3, b4, b5, b6 being Element of b1 holds
( ( b6,b2 '||' b6,b3 & b6,b4 '||' b6,b5 ) implies ( not b2 <> b3 or not b4 <> b5 or b2,b4 '||' b3,b5 ) )
proof
let c
1 be
WeakAffVect;
let c
2, c
3, c
4, c
5, c
6 be
Element of c
1;
assume
( c
2 <> c
3 & c
4 <> c
5 & c
6,c
2 '||' c
6,c
3 & c
6,c
4 '||' c
6,c
5 )
;
then
( c
2 <> c
3 & c
4 <> c
5 & c
2,c
6 '||' c
6,c
3 & c
4,c
6 '||' c
6,c
5 )
by E3;
then
( c
2,c
6 // c
6,c
3 & c
4,c
6 // c
6,c
5 )
by E1;
then
(
Mid c
2,c
6,c
3 &
Mid c
4,c
6,c
5 )
by AFVECT0:def 3;
then
c
2,c
4 // c
5,c
3
by AFVECT0:30;
hence
c
2,c
4 '||' c
3,c
5
by DIRAF:def 4;
end;
E9:
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
not ( not b2 = b3 & ( for b4 being Element of b1 holds
( not ( b2 <> b4 & b2,b3 '||' b3,b4 ) & ( for b5, b6 being Element of b1 holds
not ( b5 <> b6 & b2,b3 '||' b5,b6 & b2,b5 '||' b5,b3 & b2,b6 '||' b6,b3 ) ) ) ) )
proof
let c
1 be
WeakAffVect;
let c
2, c
3 be
Element of c
1;
consider c
4 being
Element of c
1 such that E10:
c
2,c
3 // c
3,c
4
by AFVECT0:def 1;
E11:
now
assume
c
2 = c
4
;
then consider c
5, c
6 being
Element of c
1 such that E12:
( c
2,c
3 '||' c
5,c
6 & c
2,c
5 '||' c
5,c
3 & c
2,c
6 '||' c
6,c
3 )
by E10, E2;
( c
5 = c
6 implies c
2 = c
3 )
by E12, E5;
hence
not ( not c
2 = c
3 & ( for b
1, b
2 being
Element of c
1 holds
not ( b
1 <> b
2 & c
2,c
3 '||' b
1,b
2 & c
2,b
1 '||' b
1,c
3 & c
2,b
2 '||' b
2,c
3 ) ) )
by E12;
end;
hence
not ( not c
2 = c
3 & ( for b
1 being
Element of c
1 holds
( not ( c
2 <> b
1 & c
2,c
3 '||' c
3,b
1 ) & ( for b
2, b
3 being
Element of c
1 holds
not ( b
2 <> b
3 & c
2,c
3 '||' b
2,b
3 & c
2,b
2 '||' b
2,c
3 & c
2,b
3 '||' b
3,c
3 ) ) ) ) )
by E11;
end;
E10:
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( ( b2,b3 '||' b3,b7 & b3,b4 '||' b5,b6 & b3,b5 '||' b5,b4 & b3,b6 '||' b6,b4 ) implies ( b2,b4 '||' b4,b7 ) )
proof
let c
1 be
WeakAffVect;
let c
2, c
3, c
4, c
5, c
6, c
7 be
Element of c
1;
assume E11:
( c
2,c
3 '||' c
3,c
7 & c
3,c
4 '||' c
5,c
6 & c
3,c
5 '||' c
5,c
4 & c
3,c
6 '||' c
6,c
4 )
;
then E12:
( c
2,c
3 '||' c
3,c
7 & c
3,c
4 // c
4,c
3 )
by E2;
E13:
now
assume E14:
c
2,c
3 // c
3,c
7
;
then E15:
Mid c
2,c
3,c
7
by AFVECT0:def 3;
( c
3 = c
4 implies c
2,c
4 '||' c
4,c
7 )
by E14, DIRAF:def 4;
hence
c
2,c
4 '||' c
4,c
7
by E12, E16, AFVECT0:def 2;
end;
hence
c
2,c
4 '||' c
4,c
7
by E11, E13, DIRAF:def 4;
end;
E11:
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
not ( b2 <> b5 & b3 <> b4 & b2,b3 '||' b3,b5 & b2,b4 '||' b4,b5 & ( for b6, b7 being Element of b1 holds
not ( b6 <> b7 & b3,b4 '||' b6,b7 & b3,b6 '||' b6,b4 & b3,b7 '||' b7,b4 ) ) )
proof
let c
1 be
WeakAffVect;
let c
2, c
3, c
4, c
5 be
Element of c
1;
assume E12:
( c
2 <> c
5 & c
3 <> c
4 & c
2,c
3 '||' c
3,c
5 & c
2,c
4 '||' c
4,c
5 )
;
then
( c
3 <> c
4 & c
2,c
3 // c
3,c
5 & c
2,c
4 // c
4,c
5 )
by E1;
then
( c
3 <> c
4 &
Mid c
2,c
3,c
5 &
Mid c
2,c
4,c
5 )
by AFVECT0:def 3;
then
( c
3 <> c
4 &
MDist c
3,c
4 )
by AFVECT0:25;
then
c
3,c
4 // c
4,c
3
by AFVECT0:def 2;
then consider c
6, c
7 being
Element of c
1 such that E13:
( c
3,c
4 '||' c
6,c
7 & c
3,c
6 '||' c
6,c
4 & c
3,c
7 '||' c
7,c
4 )
by E2;
not ( c
6 <> c
7 & ( for b
1, b
2 being
Element of c
1 holds
not ( b
1 <> b
2 & c
3,c
4 '||' b
1,b
2 & c
3,b
1 '||' b
1,c
4 & c
3,b
2 '||' b
2,c
4 ) ) )
by E13;
hence
ex b
1, b
2 being
Element of c
1 st
( b
1 <> b
2 & c
3,c
4 '||' b
1,b
2 & c
3,b
1 '||' b
1,c
4 & c
3,b
2 '||' b
2,c
4 )
by E12, E13, E5;
end;
E12:
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7, b8 being Element of b1 holds
not ( b2,b3 '||' b5,b6 & b2,b4 '||' b7,b8 & b2,b5 '||' b5,b3 & b2,b7 '||' b7,b4 & b2,b6 '||' b6,b3 & b2,b8 '||' b8,b4 & ( for b9, b10 being Element of b1 holds
not ( b3,b4 '||' b9,b10 & b3,b9 '||' b9,b4 & b3,b10 '||' b10,b4 ) ) )
proof
let c
1 be
WeakAffVect;
let c
2, c
3, c
4, c
5, c
6, c
7, c
8 be
Element of c
1;
assume
( c
2,c
3 '||' c
5,c
6 & c
2,c
4 '||' c
7,c
8 & c
2,c
5 '||' c
5,c
3 & c
2,c
7 '||' c
7,c
4 & c
2,c
6 '||' c
6,c
3 & c
2,c
8 '||' c
8,c
4 )
;
then
( c
2,c
3 // c
3,c
2 & c
2,c
4 // c
4,c
2 )
by E2;
then
c
3,c
4 // c
4,c
3
by AFVECT0:13;
hence
ex b
1, b
2 being
Element of c
1 st
( c
3,c
4 '||' b
1,b
2 & c
3,b
1 '||' b
1,c
4 & c
3,b
2 '||' b
2,c
4 )
by E2;
end;
consider c1 being WeakAffVect;
set c2 = the carrier of c1;
set c3 = [:the carrier of c1,the carrier of c1:];
defpred S1[ set , set ] means ex b1, b2, b3, b4 being Element of the carrier of c1 st
( a1 = [b1,b2] & a2 = [b3,b4] & b1,b2 '||' b3,b4 );
consider c4 being Relation of [:the carrier of c1,the carrier of c1:],[:the carrier of c1,the carrier of c1:] such that
E13:
for b1, b2 being set holds
( [b1,b2] in c4 iff ( b1 in [:the carrier of c1,the carrier of c1:] & b2 in [:the carrier of c1,the carrier of c1:] & S1[b1,b2] ) )
from RELSET_1:sch 1();
E14:
for b1, b2, b3, b4 being Element of the carrier of c1 holds
( [[b1,b2],[b3,b4]] in c4 iff b1,b2 '||' b3,b4 )
proof
let c
5, c
6, c
7, c
8 be
Element of the
carrier of c
1;
E15:
(
[[c5,c6],[c7,c8]] in c
4 implies c
5,c
6 '||' c
7,c
8 )
proof
assume
[[c5,c6],[c7,c8]] in c
4
;
then consider c
9, c
10, c
11, c
12 being
Element of the
carrier of c
1 such that E16:
(
[c5,c6] = [c9,c10] &
[c7,c8] = [c11,c12] )
and E17:
c
9,c
10 '||' c
11,c
12
by E13;
( c
5 = c
9 & c
6 = c
10 & c
7 = c
11 & c
8 = c
12 )
by E16, ZFMISC_1:33;
hence
c
5,c
6 '||' c
7,c
8
by E17;
end;
(
[c5,c6] in [:the carrier of c1,the carrier of c1:] &
[c7,c8] in [:the carrier of c1,the carrier of c1:] )
by ZFMISC_1:def 2;
hence
(
[[c5,c6],[c7,c8]] in c
4 iff c
5,c
6 '||' c
7,c
8 )
by E15, E13;
end;
set c5 = AffinStruct(# the carrier of c1,c4 #);
E15:
for b1, b2, b3, b4 being Element of c1
for b5, b6, b7, b8 being Element of the carrier of AffinStruct(# the carrier of c1,c4 #) holds
( ( b1 = b5 & b2 = b6 & b3 = b7 & b4 = b8 ) implies ( ( b1,b2 '||' b3,b4 iff b5,b6 // b7,b8 ) ) )
proof
let c
6, c
7, c
8, c
9 be
Element of c
1;
let c
10, c
11, c
12, c
13 be
Element of the
carrier of
AffinStruct(# the
carrier of c
1,c
4 #);
assume E16:
( c
6 = c
10 & c
7 = c
11 & c
8 = c
12 & c
9 = c
13 )
;
hence
( c
6,c
7 '||' c
8,c
9 iff c
10,c
11 // c
12,c
13 )
by E17;
end;
E16:
now
thus
not for b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds not b
1 <> b
2
by REALSET2:def 7;
thus
for b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds b
1,b
2 // b
2,b
1
thus
for b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
( b
1,b
2 // b
1,b
1 implies b
1 = b
2 )
thus
for b
1, b
2, b
3, b
4, b
5, b
6 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
( ( b
1,b
2 // b
5,b
6 & b
3,b
4 // b
5,b
6 ) implies ( b
1,b
2 // b
3,b
4 ) )
proof
let c
6, c
7, c
8, c
9, c
10, c
11 be
Element of
AffinStruct(# the
carrier of c
1,c
4 #);
assume E17:
( c
6,c
7 // c
10,c
11 & c
8,c
9 // c
10,c
11 )
;
reconsider c
12 = c
6, c
13 = c
7, c
14 = c
8, c
15 = c
9, c
16 = c
10, c
17 = c
11 as
Element of c
1 ;
( c
12,c
13 '||' c
16,c
17 & c
14,c
15 '||' c
16,c
17 )
by E17, E15;
then
c
12,c
13 '||' c
14,c
15
by E6;
hence
c
6,c
7 // c
8,c
9
by E15;
end;
thus
for b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
ex b
3 being
Element of the
carrier of
AffinStruct(# the
carrier of c
1,c
4 #) st b
1,b
3 // b
3,b
2
proof
let c
6, c
7 be
Element of
AffinStruct(# the
carrier of c
1,c
4 #);
reconsider c
8 = c
6, c
9 = c
7 as
Element of c
1 ;
consider c
10 being
Element of c
1 such that E17:
c
8,c
10 '||' c
10,c
9
by E7;
reconsider c
11 = c
10 as
Element of
AffinStruct(# the
carrier of c
1,c
4 #) ;
c
6,c
11 // c
11,c
7
by E17, E15;
hence
ex b
1 being
Element of the
carrier of
AffinStruct(# the
carrier of c
1,c
4 #) st c
6,b
1 // b
1,c
7
;
end;
thus
for b
1, b
2, b
3, b
4, b
5 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
( ( b
5,b
1 // b
5,b
2 & b
5,b
3 // b
5,b
4 ) implies ( not b
1 <> b
2 or not b
3 <> b
4 or b
1,b
3 // b
2,b
4 ) )
proof
let c
6, c
7, c
8, c
9, c
10 be
Element of
AffinStruct(# the
carrier of c
1,c
4 #);
assume that E17:
( c
6 <> c
7 & c
8 <> c
9 )
and E18:
( c
10,c
6 // c
10,c
7 & c
10,c
8 // c
10,c
9 )
;
reconsider c
11 = c
6, c
12 = c
7, c
13 = c
8, c
14 = c
9, c
15 = c
10 as
Element of c
1 ;
( c
15,c
11 '||' c
15,c
12 & c
15,c
13 '||' c
15,c
14 )
by E18, E15;
then
c
11,c
13 '||' c
12,c
14
by E17, E8;
hence
c
6,c
8 // c
7,c
9
by E15;
end;
thus
for b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
not ( not b
1 = b
2 & ( for b
3 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
( not ( b
1 <> b
3 & b
1,b
2 // b
2,b
3 ) & ( for b
4, b
5 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
not ( b
4 <> b
5 & b
1,b
2 // b
4,b
5 & b
1,b
4 // b
4,b
2 & b
1,b
5 // b
5,b
2 ) ) ) ) )
proof
let c
6, c
7 be
Element of
AffinStruct(# the
carrier of c
1,c
4 #);
assume E17:
not c
6 = c
7
;
reconsider c
8 = c
6, c
9 = c
7 as
Element of c
1 ;
now
given c
10, c
11 being
Element of c
1 such that E19:
( c
10 <> c
11 & c
8,c
9 '||' c
10,c
11 & c
8,c
10 '||' c
10,c
9 & c
8,c
11 '||' c
11,c
9 )
;
reconsider c
12 = c
10, c
13 = c
11 as
Element of
AffinStruct(# the
carrier of c
1,c
4 #) ;
( c
12 <> c
13 & c
6,c
7 // c
12,c
13 & c
6,c
12 // c
12,c
7 & c
6,c
13 // c
13,c
7 )
by E19, E15;
hence
ex b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) st
( b
1 <> b
2 & c
6,c
7 // b
1,b
2 & c
6,b
1 // b
1,c
7 & c
6,b
2 // b
2,c
7 )
;
end;
hence
not for b
1 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
( not ( c
6 <> b
1 & c
6,c
7 // c
7,b
1 ) & ( for b
2, b
3 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
not ( b
2 <> b
3 & c
6,c
7 // b
2,b
3 & c
6,b
2 // b
2,c
7 & c
6,b
3 // b
3,c
7 ) ) )
by E17, E18, E9;
end;
thus
for b
1, b
2, b
3, b
4, b
5, b
6 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
( ( b
1,b
2 // b
2,b
6 & b
2,b
3 // b
4,b
5 & b
2,b
4 // b
4,b
3 & b
2,b
5 // b
5,b
3 ) implies ( b
1,b
3 // b
3,b
6 ) )
proof
let c
6, c
7, c
8, c
9, c
10, c
11 be
Element of
AffinStruct(# the
carrier of c
1,c
4 #);
assume E17:
( c
6,c
7 // c
7,c
11 & c
7,c
8 // c
9,c
10 & c
7,c
9 // c
9,c
8 & c
7,c
10 // c
10,c
8 )
;
reconsider c
12 = c
6, c
13 = c
7, c
14 = c
8, c
15 = c
9, c
16 = c
10, c
17 = c
11 as
Element of c
1 ;
( c
12,c
13 '||' c
13,c
17 & c
13,c
14 '||' c
15,c
16 & c
13,c
15 '||' c
15,c
14 & c
13,c
16 '||' c
16,c
14 )
by E17, E15;
then
c
12,c
14 '||' c
14,c
17
by E10;
hence
c
6,c
8 // c
8,c
11
by E15;
end;
thus
for b
1, b
2, b
3, b
4 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
not ( b
1 <> b
4 & b
2 <> b
3 & b
1,b
2 // b
2,b
4 & b
1,b
3 // b
3,b
4 & ( for b
5, b
6 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
not ( b
5 <> b
6 & b
2,b
3 // b
5,b
6 & b
2,b
5 // b
5,b
3 & b
2,b
6 // b
6,b
3 ) ) )
proof
let c
6, c
7, c
8, c
9 be
Element of
AffinStruct(# the
carrier of c
1,c
4 #);
assume that E17:
( c
6 <> c
9 & c
7 <> c
8 )
and E18:
( c
6,c
7 // c
7,c
9 & c
6,c
8 // c
8,c
9 )
;
reconsider c
10 = c
6, c
11 = c
7, c
12 = c
8, c
13 = c
9 as
Element of the
carrier of c
1 ;
( c
10,c
11 '||' c
11,c
13 & c
10,c
12 '||' c
12,c
13 )
by E18, E15;
then consider c
14, c
15 being
Element of c
1 such that E19:
( c
14 <> c
15 & c
11,c
12 '||' c
14,c
15 & c
11,c
14 '||' c
14,c
12 & c
11,c
15 '||' c
15,c
12 )
by E17, E11;
reconsider c
16 = c
14, c
17 = c
15 as
Element of
AffinStruct(# the
carrier of c
1,c
4 #) ;
( c
16 <> c
17 & c
7,c
8 // c
16,c
17 & c
7,c
16 // c
16,c
8 & c
7,c
17 // c
17,c
8 )
by E19, E15;
hence
ex b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) st
( b
1 <> b
2 & c
7,c
8 // b
1,b
2 & c
7,b
1 // b
1,c
8 & c
7,b
2 // b
2,c
8 )
;
end;
thus
for b
1, b
2, b
3, b
4, b
5, b
6, b
7 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
not ( b
1,b
2 // b
4,b
5 & b
1,b
3 // b
6,b
7 & b
1,b
4 // b
4,b
2 & b
1,b
6 // b
6,b
3 & b
1,b
5 // b
5,b
2 & b
1,b
7 // b
7,b
3 & ( for b
8, b
9 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) holds
not ( b
2,b
3 // b
8,b
9 & b
2,b
8 // b
8,b
3 & b
2,b
9 // b
9,b
3 ) ) )
proof
let c
6, c
7, c
8, c
9, c
10, c
11, c
12 be
Element of
AffinStruct(# the
carrier of c
1,c
4 #);
assume E17:
( c
6,c
7 // c
9,c
10 & c
6,c
8 // c
11,c
12 & c
6,c
9 // c
9,c
7 & c
6,c
11 // c
11,c
8 & c
6,c
10 // c
10,c
7 & c
6,c
12 // c
12,c
8 )
;
reconsider c
13 = c
6, c
14 = c
7, c
15 = c
8, c
16 = c
9, c
17 = c
10, c
18 = c
11, c
19 = c
12 as
Element of the
carrier of c
1 ;
( c
13,c
14 '||' c
16,c
17 & c
13,c
15 '||' c
18,c
19 & c
13,c
16 '||' c
16,c
14 & c
13,c
18 '||' c
18,c
15 & c
13,c
17 '||' c
17,c
14 & c
13,c
19 '||' c
19,c
15 )
by E17, E15;
then consider c
20, c
21 being
Element of c
1 such that E18:
( c
14,c
15 '||' c
20,c
21 & c
14,c
20 '||' c
20,c
15 & c
14,c
21 '||' c
21,c
15 )
by E12;
reconsider c
22 = c
20, c
23 = c
21 as
Element of
AffinStruct(# the
carrier of c
1,c
4 #) ;
( c
7,c
8 // c
22,c
23 & c
7,c
22 // c
22,c
8 & c
7,c
23 // c
23,c
8 )
by E18, E15;
hence
ex b
1, b
2 being
Element of
AffinStruct(# the
carrier of c
1,c
4 #) st
( c
7,c
8 // b
1,b
2 & c
7,b
1 // b
1,c
8 & c
7,b
2 // b
2,c
8 )
;
end;
end;
definition
let c
6 be non
empty AffinStruct ;
canceled;attr a
1 is
WeakAffSegm-like means :
E17:
:: AFVECT01:def 2
( ( for b
1, b
2 being
Element of a
1 holds b
1,b
2 // b
2,b
1 ) & ( for b
1, b
2 being
Element of a
1 holds
( b
1,b
2 // b
1,b
1 implies b
1 = b
2 ) ) & ( for b
1, b
2, b
3, b
4, b
5, b
6 being
Element of a
1 holds
( ( b
1,b
2 // b
5,b
6 & b
3,b
4 // b
5,b
6 ) implies ( b
1,b
2 // b
3,b
4 ) ) ) & ( for b
1, b
2 being
Element of a
1 holds
ex b
3 being
Element of a
1 st b
1,b
3 // b
3,b
2 ) & ( for b
1, b
2, b
3, b
4, b
5 being
Element of a
1 holds
( ( b
5,b
1 // b
5,b
2 & b
5,b
3 // b
5,b
4 ) implies ( not b
1 <> b
2 or not b
3 <> b
4 or b
1,b
3 // b
2,b
4 ) ) ) & ( for b
1, b
2 being
Element of a
1 holds
not ( not b
1 = b
2 & ( for b
3 being
Element of a
1 holds
( not ( b
1 <> b
3 & b
1,b
2 // b
2,b
3 ) & ( for b
4, b
5 being
Element of a
1 holds
not ( b
4 <> b
5 & b
1,b
2 // b
4,b
5 & b
1,b
4 // b
4,b
2 & b
1,b
5 // b
5,b
2 ) ) ) ) ) ) & ( for b
1, b
2, b
3, b
4, b
5, b
6 being
Element of a
1 holds
( ( b
1,b
2 // b
2,b
6 & b
2,b
3 // b
4,b
5 & b
2,b
4 // b
4,b
3 & b
2,b
5 // b
5,b
3 ) implies ( b
1,b
3 // b
3,b
6 ) ) ) & ( for b
1, b
2, b
3, b
4 being
Element of a
1 holds
not ( b
1 <> b
4 & b
2 <> b
3 & b
1,b
2 // b
2,b
4 & b
1,b
3 // b
3,b
4 & ( for b
5, b
6 being
Element of a
1 holds
not ( b
5 <> b
6 & b
2,b
3 // b
5,b
6 & b
2,b
5 // b
5,b
3 & b
2,b
6 // b
6,b
3 ) ) ) ) & ( for b
1, b
2, b
3, b
4, b
5, b
6, b
7 being
Element of a
1 holds
not ( b
1,b
2 // b
4,b
5 & b
1,b
3 // b
6,b
7 & b
1,b
4 // b
4,b
2 & b
1,b
6 // b
6,b
3 & b
1,b
5 // b
5,b
2 & b
1,b
7 // b
7,b
3 & ( for b
8, b
9 being
Element of a
1 holds
not ( b
2,b
3 // b
8,b
9 & b
2,b
8 // b
8,b
3 & b
2,b
9 // b
9,b
3 ) ) ) ) );
end;
:: deftheorem AFVECT01:def 1 :
canceled;
:: deftheorem E17 defines WeakAffSegm-like AFVECT01:def 2 :
for b
1 being non
empty AffinStruct holds
( b
1 is
WeakAffSegm-like iff ( ( for b
2, b
3 being
Element of b
1 holds b
2,b
3 // b
3,b
2 ) & ( for b
2, b
3 being
Element of b
1 holds
( b
2,b
3 // b
2,b
2 implies b
2 = b
3 ) ) & ( for b
2, b
3, b
4, b
5, b
6, b
7 being
Element of b
1 holds
( ( b
2,b
3 // b
6,b
7 & b
4,b
5 // b
6,b
7 ) implies ( b
2,b
3 // b
4,b
5 ) ) ) & ( for b
2, b
3 being
Element of b
1 holds
ex b
4 being
Element of b
1 st b
2,b
4 // b
4,b
3 ) & ( for b
2, b
3, b
4, b
5, b
6 being
Element of b
1 holds
( ( b
6,b
2 // b
6,b
3 & b
6,b
4 // b
6,b
5 ) implies ( not b
2 <> b
3 or not b
4 <> b
5 or b
2,b
4 // b
3,b
5 ) ) ) & ( for b
2, b
3 being
Element of b
1 holds
not ( not b
2 = b
3 & ( for b
4 being
Element of b
1 holds
( not ( b
2 <> b
4 & b
2,b
3 // b
3,b
4 ) & ( for b
5, b
6 being
Element of b
1 holds
not ( b
5 <> b
6 & b
2,b
3 // b
5,b
6 & b
2,b
5 // b
5,b
3 & b
2,b
6 // b
6,b
3 ) ) ) ) ) ) & ( for b
2, b
3, b
4, b
5, b
6, b
7 being
Element of b
1 holds
( ( b
2,b
3 // b
3,b
7 & b
3,b
4 // b
5,b
6 & b
3,b
5 // b
5,b
4 & b
3,b
6 // b
6,b
4 ) implies ( b
2,b
4 // b
4,b
7 ) ) ) & ( for b
2, b
3, b
4, b
5 being
Element of b
1 holds
not ( b
2 <> b
5 & b
3 <> b
4 & b
2,b
3 // b
3,b
5 & b
2,b
4 // b
4,b
5 & ( for b
6, b
7 being
Element of b
1 holds
not ( b
6 <> b
7 & b
3,b
4 // b
6,b
7 & b
3,b
6 // b
6,b
4 & b
3,b
7 // b
7,b
4 ) ) ) ) & ( for b
2, b
3, b
4, b
5, b
6, b
7, b
8 being
Element of b
1 holds
not ( b
2,b
3 // b
5,b
6 & b
2,b
4 // b
7,b
8 & b
2,b
5 // b
5,b
3 & b
2,b
7 // b
7,b
4 & b
2,b
6 // b
6,b
3 & b
2,b
8 // b
8,b
4 & ( for b
9, b
10 being
Element of b
1 holds
not ( b
3,b
4 // b
9,b
10 & b
3,b
9 // b
9,b
4 & b
3,b
10 // b
10,b
4 ) ) ) ) ) );
theorem E18: :: AFVECT01:1
theorem E19: :: AFVECT01:2
for b
1 being
WeakAffSegmfor b
2, b
3, b
4, b
5 being
Element of b
1 holds
( b
2,b
3 // b
4,b
5 implies b
4,b
5 // b
2,b
3 )
proof
let c
6 be
WeakAffSegm;
let c
7, c
8, c
9, c
10 be
Element of c
6;
assume E20:
c
7,c
8 // c
9,c
10
;
c
9,c
10 // c
9,c
10
by E18;
hence
c
9,c
10 // c
7,c
8
by E20, E17;
end;
theorem E20: :: AFVECT01:3
for b
1 being
WeakAffSegmfor b
2, b
3, b
4, b
5 being
Element of b
1 holds
( b
2,b
3 // b
4,b
5 implies b
2,b
3 // b
5,b
4 )
proof
let c
6 be
WeakAffSegm;
let c
7, c
8, c
9, c
10 be
Element of c
6;
assume E21:
c
7,c
8 // c
9,c
10
;
c
10,c
9 // c
9,c
10
by E17;
hence
c
7,c
8 // c
10,c
9
by E21, E17;
end;
theorem E21: :: AFVECT01:4
for b
1 being
WeakAffSegmfor b
2, b
3, b
4, b
5 being
Element of b
1 holds
( b
2,b
3 // b
4,b
5 implies b
3,b
2 // b
4,b
5 )
proof
let c
6 be
WeakAffSegm;
let c
7, c
8, c
9, c
10 be
Element of c
6;
assume
c
7,c
8 // c
9,c
10
;
then
c
9,c
10 // c
7,c
8
by E19;
then
c
9,c
10 // c
8,c
7
by E20;
hence
c
8,c
7 // c
9,c
10
by E19;
end;
theorem E22: :: AFVECT01:5
proof
let c
6 be
WeakAffSegm;
let c
7, c
8 be
Element of c
6;
now
assume E23:
c
7 <> c
8
;
consider c
9 being
Element of c
6 such that E24:
c
7,c
9 // c
9,c
8
by E17;
c
9,c
7 // c
9,c
8
by E24, E21;
hence
c
7,c
7 // c
8,c
8
by E23, E17;
end;
hence
c
7,c
7 // c
8,c
8
by E17;
end;
theorem E23: :: AFVECT01:6
proof
let c
6 be
WeakAffSegm;
let c
7, c
8, c
9 be
Element of c
6;
assume E24:
c
7,c
8 // c
9,c
9
;
c
7,c
7 // c
9,c
9
by E22;
then
c
7,c
8 // c
7,c
7
by E24, E17;
hence
c
7 = c
8
by E17;
end;
theorem E24: :: AFVECT01:7
for b
1 being
WeakAffSegmfor b
2, b
3, b
4, b
5, b
6 being
Element of b
1 holds
( ( b
2,b
3 // b
4,b
5 & b
2,b
3 // b
3,b
6 & b
2,b
4 // b
4,b
3 & b
2,b
5 // b
5,b
3 ) implies ( b
2 = b
6 ) )
proof
let c
6 be
WeakAffSegm;
let c
7, c
8, c
9, c
10, c
11 be
Element of c
6;
assume that E25:
c
7,c
8 // c
9,c
10
and E26:
c
7,c
8 // c
8,c
11
and E27:
c
7,c
9 // c
9,c
8
and E28:
c
7,c
10 // c
10,c
8
;
E29:
c
8,c
7 // c
9,c
10
by E25, E21;
c
9,c
8 // c
7,c
9
by E27, E19;
then
c
9,c
8 // c
9,c
7
by E20;
then E30:
c
8,c
9 // c
9,c
7
by E21;
c
10,c
8 // c
7,c
10
by E28, E19;
then
c
10,c
8 // c
10,c
7
by E20;
then
c
8,c
10 // c
10,c
7
by E21;
then
c
7,c
7 // c
7,c
11
by E26, E29, E30, E17;
then
c
7,c
11 // c
7,c
7
by E19;
hence
c
7 = c
11
by E17;
end;
theorem :: AFVECT01:8
for b
1 being
WeakAffSegmfor b
2, b
3, b
4, b
5 being
Element of b
1 holds
not ( b
2,b
3 // b
2,b
4 & b
2,b
5 // b
2,b
4 & not b
5 = b
3 & not b
5 = b
4 & not b
3 = b
4 )
proof
let c
6 be
WeakAffSegm;
let c
7, c
8, c
9, c
10 be
Element of c
6;
assume that E25:
c
7,c
8 // c
7,c
9
and E26:
c
7,c
10 // c
7,c
9
;
now
assume that E27:
c
8 <> c
9
and E28:
c
10 <> c
9
;
c
8,c
10 // c
9,c
9
by E25, E26, E27, E28, E17;
hence
not ( not c
10 = c
8 & not c
10 = c
9 & not c
8 = c
9 )
by E23;
end;
hence
not ( not c
10 = c
8 & not c
10 = c
9 & not c
8 = c
9 )
;
end;
:: deftheorem AFVECT01:def 3 :
canceled;
:: deftheorem E25 defines MDist AFVECT01:def 4 :
:: deftheorem defines Mid AFVECT01:def 5 :
for b
1 being
WeakAffSegmfor b
2, b
3, b
4 being
Element of b
1 holds
(
Mid b
2,b
3,b
4 iff not ( not ( b
2 = b
3 & b
3 = b
4 & b
2 = b
4 ) & not ( b
2 = b
4 &
MDist b
2,b
3 ) & not ( b
2 <> b
4 & b
2,b
3 // b
3,b
4 ) ) );
theorem :: AFVECT01:9
canceled;
theorem :: AFVECT01:10
canceled;
theorem :: AFVECT01:11
proof
let c
6 be
WeakAffSegm;
let c
7, c
8 be
Element of c
6;
assume that E26:
c
7 <> c
8
and E27:
not
MDist c
7,c
8
;
not ( not c
7 = c
8 & ( for b
1 being
Element of c
6 holds
( not ( c
7 <> b
1 & c
7,c
8 // c
8,b
1 ) & ( for b
2, b
3 being
Element of c
6 holds
not ( b
2 <> b
3 & c
7,c
8 // b
2,b
3 & c
7,b
2 // b
2,c
8 & c
7,b
3 // b
3,c
8 ) ) ) ) )
by E17;
hence
ex b
1 being
Element of c
6 st
( c
7 <> b
1 & c
7,c
8 // c
8,b
1 )
by E26, E27, E25;
end;
theorem :: AFVECT01:12
proof
let c
6 be
WeakAffSegm;
let c
7, c
8, c
9 be
Element of c
6;
assume that E26:
MDist c
7,c
8
and E27:
c
7,c
8 // c
8,c
9
;
consider c
10, c
11 being
Element of c
6 such that
c
10 <> c
11
and E28:
c
7,c
8 // c
10,c
11
and E29:
c
7,c
10 // c
10,c
8
and E30:
c
7,c
11 // c
11,c
8
by E26, E25;
thus
c
7 = c
9
by E27, E28, E29, E30, E24;
end;
theorem :: AFVECT01:13
proof
let c
6 be
WeakAffSegm;
let c
7, c
8 be
Element of c
6;
assume
MDist c
7,c
8
;
then consider c
9, c
10 being
Element of c
6 such that E26:
c
9 <> c
10
and E27:
c
7,c
8 // c
9,c
10
and
c
7,c
9 // c
9,c
8
and
c
7,c
10 // c
10,c
8
by E25;
now
assume
c
7 = c
8
;
then
c
9,c
10 // c
7,c
7
by E27, E19;
hence
not verum
by E26, E23;
end;
hence
c
7 <> c
8
;
end;