:: AFVECT0 semantic presentation

definition

let c₁ be non empty AffinStruct ;
attr a₁ is WeakAffVect-like means :E1: :: AFVECT0:def 1
( ( for b₁, b₂, b₃ being Element of a₁ holds
( b₁,b₂ // b₃,b₃ implies b₁ = b₂ ) ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ holds
( ( b₁,b₂ // b₅,b₆ & b₃,b₄ // b₅,b₆ ) implies ( b₁,b₂ // b₃,b₄ ) ) ) & ( for b₁, b₂, b₃ being Element of a₁ holds
ex b₄ being Element of a₁ st b₁,b₂ // b₃,b₄ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ holds
( ( b₁,b₂ // b₄,b₅ & b₁,b₃ // b₄,b₆ ) implies ( b₂,b₃ // b₅,b₆ ) ) ) & ( for b₁, b₂ being Element of a₁ holds
ex b₃ being Element of a₁ st b₁,b₃ // b₃,b₂ ) & ( for b₁, b₂, b₃, b₄ being Element of a₁ holds
( b₁,b₂ // b₃,b₄ implies b₁,b₃ // b₂,b₄ ) ) );

end;

:: deftheorem E1 defines WeakAffVect-like AFVECT0:def 1 :

registration

cluster non empty non trivial strict WeakAffVect-like AffinStruct ;
existence

consider c₁ being strict AffVect;
reconsider c₂ = c₁ as non empty AffinStruct ;
( ( for b₁, b₂, b₃ being Element of c₂ holds
( b₁,b₂ // b₃,b₃ implies b₁ = b₂ ) ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of c₂ holds
( ( b₁,b₂ // b₅,b₆ & b₃,b₄ // b₅,b₆ ) implies ( b₁,b₂ // b₃,b₄ ) ) ) & ( for b₁, b₂, b₃ being Element of c₂ holds
ex b₄ being Element of c₂ st b₁,b₂ // b₃,b₄ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of c₂ holds
( ( b₁,b₂ // b₄,b₅ & b₁,b₃ // b₄,b₆ ) implies ( b₂,b₃ // b₅,b₆ ) ) ) & ( for b₁, b₂ being Element of c₂ holds
ex b₃ being Element of c₂ st b₁,b₃ // b₃,b₂ ) & ( for b₁, b₂, b₃, b₄ being Element of c₂ holds
( b₁,b₂ // b₃,b₄ implies b₁,b₃ // b₂,b₄ ) ) ) by TDGROUP:21;
then c₂ is WeakAffVect-like by E1;
hence ex b₁ being non empty AffinStruct st
( b₁ is strict & not b₁ is trivial & b₁ is WeakAffVect-like ) ;

end;

end;

definition

mode WeakAffVect is non empty non trivial WeakAffVect-like AffinStruct ;

end;

registration

cluster non empty AffVect-like -> non empty WeakAffVect-like AffinStruct ;
coherence

let c₁ be non empty AffinStruct ;
assume E2: c₁ is AffVect-like ;
c₁ is WeakAffVect-like

( ( for b₁, b₂, b₃ being Element of c₁ holds
( b₁,b₂ // b₃,b₃ implies b₁ = b₂ ) ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of c₁ holds
( ( b₁,b₂ // b₅,b₆ & b₃,b₄ // b₅,b₆ ) implies ( b₁,b₂ // b₃,b₄ ) ) ) & ( for b₁, b₂, b₃ being Element of c₁ holds
ex b₄ being Element of c₁ st b₁,b₂ // b₃,b₄ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of c₁ holds
( ( b₁,b₂ // b₄,b₅ & b₁,b₃ // b₄,b₆ ) implies ( b₂,b₃ // b₅,b₆ ) ) ) & ( for b₁, b₂ being Element of c₁ holds
ex b₃ being Element of c₁ st b₁,b₃ // b₃,b₂ ) & ( for b₁, b₂, b₃, b₄ being Element of c₁ holds
( b₁,b₂ // b₃,b₄ implies b₁,b₃ // b₂,b₄ ) ) ) by E2, TDGROUP:def 8;
hence c₁ is WeakAffVect-like by E1;

end;

hence c₁ is WeakAffVect-like ;

end;

end;

theorem :: AFVECT0:1

canceled;

theorem E2: :: AFVECT0:2

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds b₂,b₃ // b₂,b₃

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
ex b₁ being Element of c₁ st c₂,c₃ // c₃,b₁ by E1;
hence c₂,c₃ // c₂,c₃ by E1;

end;

theorem :: AFVECT0:3

for b₁ being WeakAffVect
for b₂ being Element of b₁ holds b₂,b₂ // b₂,b₂ by E2;

theorem E3: :: AFVECT0:4

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( b₂,b₃ // b₄,b₅ implies b₄,b₅ // b₂,b₃ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
assume E4: c₂,c₃ // c₄,c₅ ;
c₄,c₅ // c₄,c₅ by E2;
hence c₄,c₅ // c₂,c₃ by E4, E1;

end;

theorem E4: :: AFVECT0:5

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( b₂,b₃ // b₂,b₄ implies b₃ = b₄ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
assume c₂,c₃ // c₂,c₄ ;
then c₂,c₂ // c₃,c₄ by E1;
then c₃,c₄ // c₂,c₂ by E3;
hence c₃ = c₄ by E1;

end;

theorem E5: :: AFVECT0:6

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( ( b₂,b₃ // b₄,b₅ & b₂,b₃ // b₄,b₆ ) implies ( b₅ = b₆ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆ be Element of c₁;
assume ( c₂,c₃ // c₄,c₅ & c₂,c₃ // c₄,c₆ ) ;
then ( c₄,c₅ // c₂,c₃ & c₄,c₆ // c₂,c₃ ) by E3;
then c₄,c₅ // c₄,c₆ by E1;
hence c₅ = c₆ by E4;

end;

theorem E6: :: AFVECT0:7

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds b₂,b₂ // b₃,b₃

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
consider c₄ being Element of c₁ such that
E7: c₂,c₂ // c₃,c₄ by E1;
c₃,c₄ // c₂,c₂ by E7, E3;
hence c₂,c₂ // c₃,c₃ by E7, E1;

end;

theorem E7: :: AFVECT0:8

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( b₂,b₃ // b₄,b₅ implies b₃,b₂ // b₅,b₄ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
assume E8: c₂,c₃ // c₄,c₅ ;
c₂,c₂ // c₄,c₄ by E6;
hence c₃,c₂ // c₅,c₄ by E8, E1;

end;

theorem :: AFVECT0:9

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( ( b₂,b₃ // b₄,b₅ & b₂,b₄ // b₆,b₅ ) implies ( b₃ = b₆ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆ be Element of c₁;
assume E8: ( c₂,c₃ // c₄,c₅ & c₂,c₄ // c₆,c₅ ) ;
then c₂,c₄ // c₃,c₅ by E1;
then c₃,c₅ // c₂,c₄ by E3;
then E9: c₅,c₃ // c₄,c₂ by E7;
c₆,c₅ // c₂,c₄ by E8, E3;
then c₅,c₆ // c₄,c₂ by E7;
then c₅,c₃ // c₅,c₆ by E9, E1;
hence c₃ = c₆ by E4;

end;

theorem :: AFVECT0:10

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ holds
( ( b₂,b₃ // b₄,b₅ & b₆,b₇ // b₂,b₃ & b₆,b₈ // b₄,b₅ ) implies ( b₇ = b₈ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆, c₇, c₈ be Element of c₁;
assume E8: ( c₂,c₃ // c₄,c₅ & c₆,c₇ // c₂,c₃ & c₆,c₈ // c₄,c₅ ) ;
then c₄,c₅ // c₂,c₃ by E3;
then c₆,c₇ // c₄,c₅ by E8, E1;
then c₆,c₇ // c₆,c₈ by E8, E1;
hence c₇ = c₈ by E4;

end;

theorem :: AFVECT0:11

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ holds
( ( b₂,b₃ // b₄,b₅ & b₆,b₇ // b₃,b₂ & b₆,b₈ // b₅,b₄ ) implies ( b₇ = b₈ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆, c₇, c₈ be Element of c₁;
assume E8: ( c₂,c₃ // c₄,c₅ & c₆,c₇ // c₃,c₂ & c₆,c₈ // c₅,c₄ ) ;
then c₄,c₅ // c₂,c₃ by E3;
then c₅,c₄ // c₃,c₂ by E7;
then c₆,c₇ // c₅,c₄ by E8, E1;
then c₆,c₇ // c₆,c₈ by E8, E1;
hence c₇ = c₈ by E4;

end;

theorem :: AFVECT0:12

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ holds
( ( b₂,b₃ // b₄,b₅ & b₆,b₇ // b₈,b₉ & b₃,b₁₀ // b₆,b₇ & b₅,b₁₁ // b₈,b₉ ) implies ( b₂,b₁₀ // b₄,b₁₁ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆, c₇, c₈, c₉, c₁₀, c₁₁ be Element of c₁;
assume E8: ( c₂,c₃ // c₄,c₅ & c₆,c₇ // c₈,c₉ & c₃,c₁₀ // c₆,c₇ & c₅,c₁₁ // c₈,c₉ ) ;
then c₅,c₁₁ // c₆,c₇ by E1;
then E9: c₃,c₁₀ // c₅,c₁₁ by E8, E1;
c₃,c₂ // c₅,c₄ by E8, E7;
hence c₂,c₁₀ // c₄,c₁₁ by E9, E1;

end;

theorem E8: :: AFVECT0:13

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ holds
( ( b₂,b₃ // b₄,b₅ & b₂,b₆ // b₇,b₅ ) implies ( b₃,b₆ // b₇,b₄ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆, c₇ be Element of c₁;
assume E9: ( c₂,c₃ // c₄,c₅ & c₂,c₆ // c₇,c₅ ) ;
consider c₈ being Element of c₁ such that
E10: c₇,c₅ // c₄,c₈ by E1;
E11: c₇,c₄ // c₅,c₈ by E10, E1;
c₄,c₈ // c₇,c₅ by E10, E3;
then c₂,c₆ // c₄,c₈ by E9, E1;
then c₃,c₆ // c₅,c₈ by E9, E1;
hence c₃,c₆ // c₇,c₄ by E11, E1;

end;

definition

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
pred MDist c₂,c₃ means :E9: :: AFVECT0:def 2
( a₂,a₃ // a₃,a₂ & a₂ <> a₃ );
irreflexivity ;
symmetry by E3;

end;

:: deftheorem E9 defines MDist AFVECT0:def 2 :

theorem :: AFVECT0:14

canceled;

theorem :: AFVECT0:15

canceled;

theorem :: AFVECT0:16

for b₁ being WeakAffVect holds
ex b₂, b₃ being Element of b₁ st
( b₂ <> b₃ & not MDist b₂,b₃ )

let c₁ be WeakAffVect;
consider c₂, c₃ being Element of c₁ such that
E10: c₂ <> c₃ by REALSET2:def 7;

now

consider c₄ being Element of c₁ such that
E11: c₂,c₄ // c₄,c₃ by E1;

E12: now

assume E13: c₂ = c₄ ;
then c₄,c₃ // c₂,c₂ by E11, E3;
hence ex b₁, b₂ being Element of c₁ st
( b₁ <> b₂ & not MDist b₁,b₂ ) by E10, E13, E1;

end;

now

assume E13: c₂ <> c₄ ;

now

assume E14: MDist c₂,c₄ ;
c₄,c₃ // c₂,c₄ by E11, E3;
then E15: c₃,c₄ // c₄,c₂ by E7;
c₂,c₄ // c₄,c₂ by E14, E9;
then c₂,c₄ // c₃,c₄ by E15, E1;
then c₄,c₂ // c₄,c₃ by E7;
hence ex b₁, b₂ being Element of c₁ st
( b₁ <> b₂ & not MDist b₁,b₂ ) by E10, E4;

end;

hence ex b₁, b₂ being Element of c₁ st
( b₁ <> b₂ & not MDist b₁,b₂ ) by E13;

end;

hence ex b₁, b₂ being Element of c₁ st
( b₁ <> b₂ & not MDist b₁,b₂ ) by E12;

end;

hence ex b₁, b₂ being Element of c₁ st
( b₁ <> b₂ & not MDist b₁,b₂ ) ;

end;

theorem :: AFVECT0:17

canceled;

theorem :: AFVECT0:18

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
not ( MDist b₂,b₃ & MDist b₂,b₄ & not b₃ = b₄ & not MDist b₃,b₄ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
assume E10: ( MDist c₂,c₃ & MDist c₂,c₄ ) ;
consider c₅ being Element of c₁ such that
E11: c₄,c₂ // c₃,c₅ by E1;
E12: c₃,c₅ // c₄,c₂ by E11, E3;
E13: ( c₂,c₃ // c₃,c₂ & c₂,c₄ // c₄,c₂ ) by E10, E9;
then E14: c₂,c₄ // c₃,c₅ by E12, E1;
E15: c₄,c₃ // c₂,c₅ by E11, E1;
c₃,c₄ // c₂,c₅ by E13, E14, E1;
then c₃,c₄ // c₄,c₃ by E15, E1;
hence not ( not c₃ = c₄ & not MDist c₃,c₄ ) by E9;

end;

theorem :: AFVECT0:19

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( ( MDist b₂,b₃ & b₂,b₃ // b₄,b₅ ) implies ( MDist b₄,b₅ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
assume E10: ( MDist c₂,c₃ & c₂,c₃ // c₄,c₅ ) ;
then E11: ( c₂ <> c₃ & c₂,c₃ // c₃,c₂ ) by E9;
E12: c₄,c₅ // c₂,c₃ by E10, E3;
then c₅,c₄ // c₃,c₂ by E7;
then c₅,c₄ // c₂,c₃ by E11, E1;
then c₄,c₅ // c₅,c₄ by E12, E1;
then ( c₄ <> c₅ implies MDist c₄,c₅ ) by E9;
hence MDist c₄,c₅ by E10, E1;

end;

definition

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
pred Mid c₂,c₃,c₄ means :E10: :: AFVECT0:def 3
a₂,a₃ // a₃,a₄;

end;

:: deftheorem E10 defines Mid AFVECT0:def 3 :

theorem :: AFVECT0:20

canceled;

theorem E11: :: AFVECT0:21

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( Mid b₂,b₃,b₄ implies Mid b₄,b₃,b₂ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
assume Mid c₂,c₃,c₄ ;
then c₂,c₃ // c₃,c₄ by E10;
then c₃,c₂ // c₄,c₃ by E7;
then c₄,c₃ // c₃,c₂ by E3;
hence Mid c₄,c₃,c₂ by E10;

end;

theorem :: AFVECT0:22

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
( Mid b₂,b₃,b₃ iff b₂ = b₃ )

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;

E12: now

assume Mid c₂,c₃,c₃ ;
then c₂,c₃ // c₃,c₃ by E10;
hence c₂ = c₃ by E1;

end;

now

assume c₂ = c₃ ;
then c₂,c₃ // c₃,c₃ by E6;
hence Mid c₂,c₃,c₃ by E10;

end;

hence ( Mid c₂,c₃,c₃ iff c₂ = c₃ ) by E12;

end;

theorem E12: :: AFVECT0:23

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
( Mid b₂,b₃,b₂ iff ( b₂ = b₃ or MDist b₂,b₃ ) )

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;

E13: now

assume Mid c₂,c₃,c₂ ;
then c₂,c₃ // c₃,c₂ by E10;
hence ( c₂ = c₃ or MDist c₂,c₃ ) by E9;

end;

E14: now

assume c₂ = c₃ ;
then c₂,c₃ // c₃,c₂ by E6;
hence Mid c₂,c₃,c₂ by E10;

end;

now

assume MDist c₂,c₃ ;
then c₂,c₃ // c₃,c₂ by E9;
hence Mid c₂,c₃,c₂ by E10;

end;

hence ( Mid c₂,c₃,c₂ iff ( c₂ = c₃ or MDist c₂,c₃ ) ) by E13, E14;

end;

theorem E13: :: AFVECT0:24

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
ex b₄ being Element of b₁ st Mid b₂,b₄,b₃

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
consider c₄ being Element of c₁ such that
E14: c₂,c₄ // c₄,c₃ by E1;
Mid c₂,c₄,c₃ by E14, E10;
hence ex b₁ being Element of c₁ st Mid c₂,b₁,c₃ ;

end;

theorem E14: :: AFVECT0:25

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
not ( Mid b₂,b₃,b₄ & Mid b₂,b₅,b₄ & not b₃ = b₅ & not MDist b₃,b₅ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
assume ( Mid c₂,c₃,c₄ & Mid c₂,c₅,c₄ ) ;
then E15: ( c₂,c₃ // c₃,c₄ & c₂,c₅ // c₅,c₄ ) by E10;
consider c₆ being Element of c₁ such that
E16: c₅,c₄ // c₃,c₆ by E1;
E17: c₃,c₆ // c₅,c₄ by E16, E3;
then c₂,c₅ // c₃,c₆ by E15, E1;
then E18: c₃,c₅ // c₄,c₆ by E15, E1;
c₃,c₅ // c₆,c₄ by E17, E1;
then c₅,c₃ // c₄,c₆ by E7;
then c₃,c₅ // c₅,c₃ by E18, E1;
hence not ( not c₃ = c₅ & not MDist c₃,c₅ ) by E9;

end;

theorem E15: :: AFVECT0:26

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
ex b₄ being Element of b₁ st Mid b₂,b₃,b₄

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
consider c₄ being Element of c₁ such that
E16: c₂,c₃ // c₃,c₄ by E1;
Mid c₂,c₃,c₄ by E16, E10;
hence ex b₁ being Element of c₁ st Mid c₂,c₃,b₁ ;

end;

theorem E16: :: AFVECT0:27

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( ( Mid b₂,b₃,b₄ & Mid b₂,b₃,b₅ ) implies ( b₄ = b₅ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
assume ( Mid c₂,c₃,c₄ & Mid c₂,c₃,c₅ ) ;
then ( c₂,c₃ // c₃,c₄ & c₂,c₃ // c₃,c₅ ) by E10;
then ( c₃,c₄ // c₂,c₃ & c₃,c₅ // c₂,c₃ ) by E3;
then c₃,c₄ // c₃,c₅ by E1;
hence c₄ = c₅ by E4;

end;

theorem E17: :: AFVECT0:28

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( ( Mid b₂,b₃,b₄ & MDist b₃,b₅ ) implies ( Mid b₂,b₅,b₄ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
assume ( Mid c₂,c₃,c₄ & MDist c₃,c₅ ) ;
then E18: ( c₂,c₃ // c₃,c₄ & c₃,c₅ // c₅,c₃ ) by E9, E10;
consider c₆ being Element of c₁ such that
E19: c₅,c₃ // c₄,c₆ by E1;
c₄,c₆ // c₅,c₃ by E19, E3;
then E20: c₃,c₅ // c₄,c₆ by E18, E1;
c₃,c₂ // c₄,c₃ by E18, E7;
then E21: c₂,c₅ // c₃,c₆ by E20, E1;
c₅,c₄ // c₃,c₆ by E19, E1;
then c₂,c₅ // c₅,c₄ by E21, E1;
hence Mid c₂,c₅,c₄ by E10;

end;

theorem E18: :: AFVECT0:29

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( ( Mid b₂,b₃,b₄ & Mid b₂,b₅,b₆ & MDist b₃,b₅ ) implies ( b₄ = b₆ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆ be Element of c₁;
assume E19: ( Mid c₂,c₃,c₄ & Mid c₂,c₅,c₆ & MDist c₃,c₅ ) ;
then Mid c₂,c₅,c₄ by E17;
hence c₄ = c₆ by E19, E16;

end;

theorem E19: :: AFVECT0:30

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( ( Mid b₂,b₃,b₄ & Mid b₅,b₃,b₆ ) implies ( b₂,b₅ // b₆,b₄ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆ be Element of c₁;
assume E20: ( Mid c₂,c₃,c₄ & Mid c₅,c₃,c₆ ) ;
consider c₇ being Element of c₁ such that
E21: c₆,c₃ // c₄,c₇ by E1;
E22: c₄,c₇ // c₆,c₃ by E21, E3;
c₅,c₃ // c₃,c₆ by E20, E10;
then c₃,c₅ // c₆,c₃ by E7;
then E23: c₃,c₅ // c₄,c₇ by E22, E1;
c₂,c₃ // c₃,c₄ by E20, E10;
then c₃,c₂ // c₄,c₃ by E7;
then E24: c₂,c₅ // c₃,c₇ by E23, E1;
c₆,c₄ // c₃,c₇ by E21, E1;
hence c₂,c₅ // c₆,c₄ by E24, E1;

end;

theorem :: AFVECT0:31

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ holds
( ( Mid b₂,b₃,b₄ & Mid b₅,b₆,b₇ & MDist b₃,b₆ ) implies ( b₂,b₅ // b₇,b₄ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆, c₇ be Element of c₁;
assume E20: ( Mid c₂,c₃,c₄ & Mid c₅,c₆,c₇ & MDist c₃,c₆ ) ;
then Mid c₂,c₆,c₄ by E17;
hence c₂,c₅ // c₇,c₄ by E20, E19;

end;

definition

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
func PSym c₂,c₃ -> Element of a₁ means :E20: :: AFVECT0:def 4
Mid a₃,a₂,a₄;
correctness by E15, E16;

end;

:: deftheorem E20 defines PSym AFVECT0:def 4 :

theorem :: AFVECT0:32

canceled;

theorem :: AFVECT0:33

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( PSym b₂,b₃ = b₄ iff b₃,b₂ // b₂,b₄ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;

E21: now

assume PSym c₂,c₃ = c₄ ;
then Mid c₃,c₂,c₄ by E20;
hence c₃,c₂ // c₂,c₄ by E10;

end;

now

assume c₃,c₂ // c₂,c₄ ;
then Mid c₃,c₂,c₄ by E10;
hence PSym c₂,c₃ = c₄ by E20;

end;

hence ( PSym c₂,c₃ = c₄ iff c₃,c₂ // c₂,c₄ ) by E21;

end;

theorem :: AFVECT0:34

canceled;

theorem E21: :: AFVECT0:35

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
( PSym b₂,b₃ = b₃ iff ( b₃ = b₂ or MDist b₃,b₂ ) )

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;

E22: now

assume PSym c₂,c₃ = c₃ ;
then Mid c₃,c₂,c₃ by E20;
hence ( c₃ = c₂ or MDist c₃,c₂ ) by E12;

end;

now

assume ( c₃ = c₂ or MDist c₃,c₂ ) ;
then Mid c₃,c₂,c₃ by E12;
hence PSym c₂,c₃ = c₃ by E20;

end;

hence ( PSym c₂,c₃ = c₃ iff ( c₃ = c₂ or MDist c₃,c₂ ) ) by E22;

end;

theorem E22: :: AFVECT0:36

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds PSym b₂,(PSym b₂,b₃) = b₃

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
Mid c₃,c₂, PSym c₂,c₃ by E20;
then Mid PSym c₂,c₃,c₂,c₃ by E11;
hence PSym c₂,(PSym c₂,c₃) = c₃ by E20;

end;

theorem E23: :: AFVECT0:37

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( PSym b₂,b₃ = PSym b₂,b₄ implies b₃ = b₄ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
assume E24: PSym c₂,c₃ = PSym c₂,c₄ ;
( PSym c₂,(PSym c₂,c₃) = c₃ & PSym c₂,(PSym c₂,c₄) = c₄ ) by E22;
hence c₃ = c₄ by E24;

end;

theorem :: AFVECT0:38

for b₁ being WeakAffVect
for b₂, b₃ being Element of b₁ holds
ex b₄ being Element of b₁ st PSym b₂,b₄ = b₃

let c₁ be WeakAffVect;
let c₂, c₃ be Element of c₁;
PSym c₂,(PSym c₂,c₃) = c₃ by E22;
hence ex b₁ being Element of c₁ st PSym c₂,b₁ = c₃ ;

end;

theorem E24: :: AFVECT0:39

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds b₂,b₃ // PSym b₄,b₃, PSym b₄,b₂

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
( Mid c₂,c₄, PSym c₄,c₂ & Mid c₃,c₄, PSym c₄,c₃ ) by E20;
hence c₂,c₃ // PSym c₄,c₃, PSym c₄,c₂ by E19;

end;

theorem E25: :: AFVECT0:40

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( b₂,b₃ // b₄,b₅ iff PSym b₆,b₂, PSym b₆,b₃ // PSym b₆,b₄, PSym b₆,b₅ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅, c₆ be Element of c₁;

E26: now

assume E27: c₂,c₃ // c₄,c₅ ;
E28: ( c₂,c₃ // PSym c₆,c₃, PSym c₆,c₂ & c₄,c₅ // PSym c₆,c₅, PSym c₆,c₄ ) by E24;
then PSym c₆,c₅, PSym c₆,c₄ // c₄,c₅ by E3;
then E29: PSym c₆,c₅, PSym c₆,c₄ // c₂,c₃ by E27, E1;
PSym c₆,c₃, PSym c₆,c₂ // c₂,c₃ by E28, E3;
then PSym c₆,c₃, PSym c₆,c₂ // PSym c₆,c₅, PSym c₆,c₄ by E29, E1;
hence PSym c₆,c₂, PSym c₆,c₃ // PSym c₆,c₄, PSym c₆,c₅ by E7;

end;

now

assume E27: PSym c₆,c₂, PSym c₆,c₃ // PSym c₆,c₄, PSym c₆,c₅ ;
E28: ( c₂,c₃ // PSym c₆,c₃, PSym c₆,c₂ & c₄,c₅ // PSym c₆,c₅, PSym c₆,c₄ ) by E24;
c₅,c₄ // PSym c₆,c₄, PSym c₆,c₅ by E24;
then c₅,c₄ // PSym c₆,c₂, PSym c₆,c₃ by E27, E1;
then c₄,c₅ // PSym c₆,c₃, PSym c₆,c₂ by E7;
hence c₂,c₃ // c₄,c₅ by E28, E1;

end;

hence ( c₂,c₃ // c₄,c₅ iff PSym c₆,c₂, PSym c₆,c₃ // PSym c₆,c₄, PSym c₆,c₅ ) by E26;

end;

theorem :: AFVECT0:41

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( MDist b₂,b₃ iff MDist PSym b₄,b₂, PSym b₄,b₃ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;

E26: now

assume MDist c₂,c₃ ;
then ( c₂,c₃ // c₃,c₂ & c₂ <> c₃ ) by E9;
then ( PSym c₄,c₂, PSym c₄,c₃ // PSym c₄,c₃, PSym c₄,c₂ & PSym c₄,c₂ <> PSym c₄,c₃ ) by E23, E25;
hence MDist PSym c₄,c₂, PSym c₄,c₃ by E9;

end;

now

assume MDist PSym c₄,c₂, PSym c₄,c₃ ;
then ( PSym c₄,c₂, PSym c₄,c₃ // PSym c₄,c₃, PSym c₄,c₂ & PSym c₄,c₂ <> PSym c₄,c₃ ) by E9;
then ( c₂,c₃ // c₃,c₂ & c₂ <> c₃ ) by E25;
hence MDist c₂,c₃ by E9;

end;

hence ( MDist c₂,c₃ iff MDist PSym c₄,c₂, PSym c₄,c₃ ) by E26;

end;

theorem E26: :: AFVECT0:42

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( Mid b₂,b₃,b₄ iff Mid PSym b₅,b₂, PSym b₅,b₃, PSym b₅,b₄ )

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;

E27: now

assume Mid c₂,c₃,c₄ ;
then c₂,c₃ // c₃,c₄ by E10;
then PSym c₅,c₂, PSym c₅,c₃ // PSym c₅,c₃, PSym c₅,c₄ by E25;
hence Mid PSym c₅,c₂, PSym c₅,c₃, PSym c₅,c₄ by E10;

end;

now

assume Mid PSym c₅,c₂, PSym c₅,c₃, PSym c₅,c₄ ;
then PSym c₅,c₂, PSym c₅,c₃ // PSym c₅,c₃, PSym c₅,c₄ by E10;
then c₂,c₃ // c₃,c₄ by E25;
hence Mid c₂,c₃,c₄ by E10;

end;

hence ( Mid c₂,c₃,c₄ iff Mid PSym c₅,c₂, PSym c₅,c₃, PSym c₅,c₄ ) by E27;

end;

theorem E27: :: AFVECT0:43

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( PSym b₂,b₃ = PSym b₄,b₃ iff ( b₂ = b₄ or MDist b₂,b₄ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;

E28: now

assume E29: PSym c₂,c₃ = PSym c₄,c₃ ;
( Mid c₃,c₂, PSym c₂,c₃ & Mid c₃,c₄, PSym c₄,c₃ ) by E20;
hence ( c₂ = c₄ or MDist c₂,c₄ ) by E29, E14;

end;

now

assume E29: MDist c₂,c₄ ;
( Mid c₃,c₂, PSym c₂,c₃ & Mid c₃,c₄, PSym c₄,c₃ ) by E20;
hence PSym c₂,c₃ = PSym c₄,c₃ by E29, E18;

end;

hence ( PSym c₂,c₃ = PSym c₄,c₃ iff ( c₂ = c₄ or MDist c₂,c₄ ) ) by E28;

end;

theorem E28: :: AFVECT0:44

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds PSym b₂,(PSym b₃,(PSym b₂,b₄)) = PSym (PSym b₂,b₃),b₄

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;
Mid PSym c₂,c₄,c₃, PSym c₃,(PSym c₂,c₄) by E20;
then Mid PSym c₂,(PSym c₂,c₄), PSym c₂,c₃, PSym c₂,(PSym c₃,(PSym c₂,c₄)) by E26;
then PSym c₂,(PSym c₃,(PSym c₂,c₄)) = PSym (PSym c₂,c₃),(PSym c₂,(PSym c₂,c₄)) by E20;
hence PSym c₂,(PSym c₃,(PSym c₂,c₄)) = PSym (PSym c₂,c₃),c₄ by E22;

end;

theorem :: AFVECT0:45

for b₁ being WeakAffVect
for b₂, b₃, b₄ being Element of b₁ holds
( PSym b₂,(PSym b₃,b₄) = PSym b₃,(PSym b₂,b₄) iff not ( not b₂ = b₃ & not MDist b₂,b₃ & not MDist b₃, PSym b₂,b₃ ) )

let c₁ be WeakAffVect;
let c₂, c₃, c₄ be Element of c₁;

E29: now

assume PSym c₂,(PSym c₃,c₄) = PSym c₃,(PSym c₂,c₄) ;
then PSym c₂,(PSym c₃,(PSym c₂,c₄)) = PSym c₃,c₄ by E22;
then PSym (PSym c₂,c₃),c₄ = PSym c₃,c₄ by E28;
then ( c₃ = PSym c₂,c₃ or MDist c₃, PSym c₂,c₃ ) by E27;
then E30: ( Mid c₃,c₂,c₃ or MDist c₃, PSym c₂,c₃ ) by E20;
hence not ( not c₂ = c₃ & not MDist c₃,c₂ & not MDist c₃, PSym c₂,c₃ ) by E12;
thus not ( not c₂ = c₃ & not MDist c₂,c₃ & not MDist c₃, PSym c₂,c₃ ) by E30, E12;

end;

now

assume not ( not c₂ = c₃ & not MDist c₂,c₃ & not MDist c₃, PSym c₂,c₃ ) ;
then ( Mid c₃,c₂,c₃ or MDist c₃, PSym c₂,c₃ ) by E12;
then PSym (PSym c₂,c₃),c₄ = PSym c₃,c₄ by E20, E27;
then PSym c₂,(PSym c₃,(PSym c₂,c₄)) = PSym c₃,c₄ by E28;
hence PSym c₂,(PSym c₃,c₄) = PSym c₃,(PSym c₂,c₄) by E22;

end;

hence ( PSym c₂,(PSym c₃,c₄) = PSym c₃,(PSym c₂,c₄) iff not ( not c₂ = c₃ & not MDist c₂,c₃ & not MDist c₃, PSym c₂,c₃ ) ) by E29;

end;

theorem E29: :: AFVECT0:46

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds PSym b₂,(PSym b₃,(PSym b₄,b₅)) = PSym b₄,(PSym b₃,(PSym b₂,b₅))

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
PSym c₃,(PSym c₄,c₂),c₂ // PSym c₃,c₂, PSym c₃,(PSym c₃,(PSym c₄,c₂)) by E24;
then E30: PSym c₃,(PSym c₄,c₂),c₂ // PSym c₃,c₂, PSym c₄,c₂ by E22;
PSym c₃,c₂, PSym c₄,c₂ // PSym c₄,(PSym c₄,c₂), PSym c₄,(PSym c₃,c₂) by E24;
then PSym c₃,c₂, PSym c₄,c₂ // c₂, PSym c₄,(PSym c₃,c₂) by E22;
then c₂, PSym c₄,(PSym c₃,c₂) // PSym c₃,c₂, PSym c₄,c₂ by E3;
then PSym c₃,(PSym c₄,c₂),c₂ // c₂, PSym c₄,(PSym c₃,c₂) by E30, E1;
then Mid PSym c₃,(PSym c₄,c₂),c₂, PSym c₄,(PSym c₃,c₂) by E10;
then PSym c₂,(PSym c₃,(PSym c₄,c₂)) = PSym c₄,(PSym c₃,c₂) by E20;
then E31: PSym c₂,(PSym c₃,(PSym c₄,c₂)) = PSym c₄,(PSym c₃,(PSym c₂,c₂)) by E21;
E32: c₂,c₅ // PSym c₄,c₅, PSym c₄,c₂ by E24;
PSym c₄,c₅, PSym c₄,c₂ // PSym c₃,(PSym c₄,c₂), PSym c₃,(PSym c₄,c₅) by E24;
then PSym c₃,(PSym c₄,c₂), PSym c₃,(PSym c₄,c₅) // PSym c₄,c₅, PSym c₄,c₂ by E3;
then E33: c₂,c₅ // PSym c₃,(PSym c₄,c₂), PSym c₃,(PSym c₄,c₅) by E32, E1;
PSym c₃,(PSym c₄,c₂), PSym c₃,(PSym c₄,c₅) // PSym c₂,(PSym c₃,(PSym c₄,c₅)), PSym c₂,(PSym c₃,(PSym c₄,c₂)) by E24;
then PSym c₂,(PSym c₃,(PSym c₄,c₅)), PSym c₂,(PSym c₃,(PSym c₄,c₂)) // PSym c₃,(PSym c₄,c₂), PSym c₃,(PSym c₄,c₅) by E3;
then E34: PSym c₂,(PSym c₃,(PSym c₄,c₅)), PSym c₂,(PSym c₃,(PSym c₄,c₂)) // c₂,c₅ by E33, E1;
E35: c₂,c₅ // PSym c₂,c₅, PSym c₂,c₂ by E24;
PSym c₂,c₅, PSym c₂,c₂ // PSym c₃,(PSym c₂,c₂), PSym c₃,(PSym c₂,c₅) by E24;
then PSym c₃,(PSym c₂,c₂), PSym c₃,(PSym c₂,c₅) // PSym c₂,c₅, PSym c₂,c₂ by E3;
then E36: c₂,c₅ // PSym c₃,(PSym c₂,c₂), PSym c₃,(PSym c₂,c₅) by E35, E1;
PSym c₃,(PSym c₂,c₂), PSym c₃,(PSym c₂,c₅) // PSym c₄,(PSym c₃,(PSym c₂,c₅)), PSym c₄,(PSym c₃,(PSym c₂,c₂)) by E24;
then PSym c₄,(PSym c₃,(PSym c₂,c₅)), PSym c₄,(PSym c₃,(PSym c₂,c₂)) // PSym c₃,(PSym c₂,c₂), PSym c₃,(PSym c₂,c₅) by E3;
then PSym c₄,(PSym c₃,(PSym c₂,c₅)), PSym c₄,(PSym c₃,(PSym c₂,c₂)) // c₂,c₅ by E36, E1;
then PSym c₂,(PSym c₃,(PSym c₄,c₅)), PSym c₂,(PSym c₃,(PSym c₄,c₂)) // PSym c₄,(PSym c₃,(PSym c₂,c₅)), PSym c₂,(PSym c₃,(PSym c₄,c₂)) by E31, E34, E1;
then PSym c₂,(PSym c₃,(PSym c₄,c₂)), PSym c₂,(PSym c₃,(PSym c₄,c₅)) // PSym c₂,(PSym c₃,(PSym c₄,c₂)), PSym c₄,(PSym c₃,(PSym c₂,c₅)) by E7;
hence PSym c₂,(PSym c₃,(PSym c₄,c₅)) = PSym c₄,(PSym c₃,(PSym c₂,c₅)) by E4;

end;

theorem :: AFVECT0:47

for b₁ being WeakAffVect
for b₂, b₃, b₄, b₅ being Element of b₁ holds
ex b₆ being Element of b₁ st PSym b₂,(PSym b₃,(PSym b₄,b₅)) = PSym b₆,b₅

let c₁ be WeakAffVect;
let c₂, c₃, c₄, c₅ be Element of c₁;
consider c₆ being Element of c₁ such that
E30: Mid c₂,c₆,c₄ by E13;
E31: c₄ = PSym c₆,c₂ by E30, E20;
consider c₇ being Element of c₁ such that
E32: