:: TRANSLAC semantic presentation

definition

let c₁ be AffinSpace;
attr a₁ is Fanoian means :Def1: :: TRANSLAC:def 1
for b₁, b₂, b₃, b₄ being Element of a₁ st b₁,b₂ // b₃,b₄ & b₁,b₃ // b₂,b₄ & b₁,b₄ // b₂,b₃ holds
LIN b₁,b₂,b₃;

end;

:: deftheorem Def1 defines Fanoian TRANSLAC:def 1 :

notation

let c₁ be AffinSpace;
synonym c₁ satisfies_Fano for Fanoian c₁;

end;

Lemma2: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st LIN b₂,b₃,b₄ & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ & not LIN b₂,b₃,b₅ holds
ex b₆ being Element of b₁ st
( LIN b₅,b₂,b₆ & b₅ <> b₆ & b₂ <> b₆ )

proof end;

Lemma3: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st LIN b₂,b₃,b₄ & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ & not LIN b₂,b₃,b₅ & LIN b₂,b₃,b₆ holds
ex b₇ being Element of b₁ st
( LIN b₅,b₆,b₇ & b₅ <> b₇ & b₆ <> b₇ )

proof end;

Lemma4: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st LIN b₂,b₃,b₄ & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ & not LIN b₂,b₃,b₅ & b₅ <> b₆ & b₅,b₆ // b₂,b₃ holds
ex b₇ being Element of b₁ st
( LIN b₅,b₆,b₇ & b₅ <> b₇ & b₆ <> b₇ )

proof end;

theorem Th1: :: TRANSLAC:1

canceled;

theorem Th2: :: TRANSLAC:2

for b₁ being AffinSpace st ex b₂, b₃, b₄ being Element of b₁ st
( LIN b₂,b₃,b₄ & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ ) holds
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st
( LIN b₂,b₃,b₄ & b₂ <> b₄ & b₃ <> b₄ )

proof end;

theorem Th3: :: TRANSLAC:3

canceled;

theorem Th4: :: TRANSLAC:4

for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st b₁ satisfies_Fano & b₂,b₃ // b₄,b₅ & b₂,b₄ // b₃,b₅ & not LIN b₂,b₃,b₄ holds
ex b₆ being Element of b₁ st
( LIN b₃,b₄,b₆ & LIN b₂,b₅,b₆ )

proof end;

Lemma7: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₃ // b₄,b₅ & b₄ <> b₅ holds
( not LIN b₄,b₅,b₂ & not LIN b₃,b₂,b₅ & not LIN b₅,b₄,b₃ )

proof end;

Lemma8: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₃ // b₄,b₅ & b₂,b₄ // b₃,b₅ holds
( not LIN b₄,b₅,b₂ & not LIN b₃,b₂,b₅ & not LIN b₅,b₄,b₃ )

proof end;

theorem Th5: :: TRANSLAC:5

for b₁ being AffinPlane
for b₂, b₃, b₄ being Element of b₁
for b₅ being Permutation of the carrier of b₁ st b₅ is_Tr & not LIN b₂,b₅ . b₂,b₃ & b₂,b₅ . b₂ // b₃,b₄ & b₂,b₃ // b₅ . b₂,b₄ holds
b₄ = b₅ . b₃

proof end;

theorem Th6: :: TRANSLAC:6

for b₁ being AffinPlane holds
( b₁ satisfies_des iff for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not LIN b₂,b₃,b₄ & not LIN b₂,b₃,b₅ & b₂,b₃ // b₄,b₆ & b₂,b₃ // b₅,b₇ & b₂,b₄ // b₃,b₆ & b₂,b₅ // b₃,b₇ holds
b₄,b₅ // b₆,b₇ )

proof end;

theorem Th7: :: TRANSLAC:7

for b₁ being AffinPlane
for b₂ being Element of b₁ ex b₃ being Permutation of the carrier of b₁ st
( b₃ is_Tr & b₃ . b₂ = b₂ )

proof end;

Lemma12: for b₁ being AffinPlane
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ holds
ex b₅ being Element of b₁ st
( ( not LIN b₂,b₃,b₄ & b₂,b₃ // b₄,b₅ & b₂,b₄ // b₃,b₅ ) or ( LIN b₂,b₃,b₄ & ex b₆, b₇ being Element of b₁ st
( not LIN b₂,b₃,b₆ & b₂,b₃ // b₆,b₇ & b₂,b₆ // b₃,b₇ & b₆,b₇ // b₄,b₅ & b₆,b₄ // b₇,b₅ ) ) )

proof end;

Lemma13: for b₁ being AffinPlane
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ holds
ex b₅ being Element of b₁ st
( ( not LIN b₂,b₃,b₅ & b₂,b₃ // b₅,b₄ & b₂,b₅ // b₃,b₄ ) or ( LIN b₂,b₃,b₅ & ex b₆, b₇ being Element of b₁ st
( not LIN b₂,b₃,b₆ & b₂,b₃ // b₆,b₇ & b₂,b₆ // b₃,b₇ & b₆,b₇ // b₅,b₄ & b₆,b₅ // b₇,b₄ ) ) )

proof end;

Lemma14: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st b₁ satisfies_des & b₂ <> b₃ & LIN b₂,b₃,b₄ & b₂,b₃ // b₅,b₆ & b₂,b₃ // b₇,b₈ & b₂,b₅ // b₃,b₆ & b₂,b₇ // b₃,b₈ & b₅,b₆ // b₄,b₉ & b₇,b₈ // b₄,b₁₀ & b₅,b₄ // b₆,b₉ & b₇,b₄ // b₈,b₁₀ & not LIN b₂,b₃,b₅ & not LIN b₂,b₃,b₇ & not LIN b₅,b₆,b₇ holds
b₉ = b₁₀

proof end;

theorem Th8: :: TRANSLAC:8

for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st ( for b₆, b₇, b₈ being Element of b₁ st b₆ <> b₇ & LIN b₆,b₇,b₈ & not b₈ = b₆ holds
b₈ = b₇ ) & b₂,b₃ // b₄,b₅ & b₂,b₄ // b₃,b₅ & not LIN b₂,b₃,b₄ holds
b₂,b₅ // b₃,b₄

proof end;

Lemma16: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st b₁ satisfies_des & b₂ <> b₃ & LIN b₂,b₃,b₄ & b₂,b₃ // b₅,b₆ & b₂,b₃ // b₇,b₈ & b₂,b₅ // b₃,b₆ & b₂,b₇ // b₃,b₈ & b₅,b₆ // b₄,b₉ & b₇,b₈ // b₄,b₁₀ & b₅,b₄ // b₆,b₉ & b₇,b₄ // b₈,b₁₀ & not LIN b₂,b₃,b₅ & not LIN b₂,b₃,b₇ holds
b₉ = b₁₀

proof end;

Lemma17: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & LIN b₂,b₃,b₄ & b₂,b₃ // b₅,b₆ & b₂,b₅ // b₃,b₆ & b₅,b₆ // b₄,b₇ & not LIN b₂,b₃,b₅ holds
( b₅ <> b₆ & LIN b₂,b₃,b₇ )

proof end;

Lemma18: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st b₁ satisfies_des & b₂ <> b₃ & LIN b₂,b₃,b₄ & b₂,b₃ // b₅,b₆ & b₂,b₃ // b₇,b₈ & b₂,b₅ // b₃,b₆ & b₂,b₇ // b₃,b₈ & b₅,b₆ // b₄,b₉ & b₅,b₄ // b₆,b₉ & b₇,b₈ // b₁₀,b₉ & b₇,b₁₀ // b₈,b₉ & not LIN b₂,b₃,b₅ & not LIN b₂,b₃,b₇ holds
b₄ = b₁₀

proof end;

Lemma19: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁ st b₁ satisfies_des & b₂ <> b₃ holds
ex b₄ being Permutation of the carrier of b₁ st
( b₄ is_Tr & b₄ . b₂ = b₃ )

proof end;

theorem Th9: :: TRANSLAC:9

for b₁ being AffinPlane
for b₂, b₃ being Element of b₁ st b₁ satisfies_des holds
ex b₄ being Permutation of the carrier of b₁ st
( b₄ is_Tr & b₄ . b₂ = b₃ )

proof end;

theorem Th10: :: TRANSLAC:10

for b₁ being AffinPlane st ( for b₂, b₃ being Element of b₁ ex b₄ being Permutation of the carrier of b₁ st
( b₄ is_Tr & b₄ . b₂ = b₃ ) ) holds
b₁ satisfies_des

proof end;

theorem Th11: :: TRANSLAC:11

for b₁ being AffinPlane
for b₂ being Element of b₁
for b₃, b₄ being Permutation of the carrier of b₁ st b₃ is_Tr & b₄ is_Tr & not LIN b₂,b₃ . b₂,b₄ . b₂ holds
b₃ * b₄ = b₄ * b₃

proof end;

theorem Th12: :: TRANSLAC:12

for b₁ being AffinPlane
for b₂, b₃ being Permutation of the carrier of b₁ st b₁ satisfies_des & b₂ is_Tr & b₃ is_Tr holds
b₂ * b₃ = b₃ * b₂

proof end;

theorem Th13: :: TRANSLAC:13

for b₁ being AffinPlane
for b₂ being Element of b₁
for b₃, b₄ being Permutation of the carrier of b₁ st b₃ is_Tr & b₄ is_Tr & b₂,b₃ . b₂ // b₂,b₄ . b₂ holds
b₂,b₃ . b₂ // b₂,(b₃ * b₄) . b₂

proof end;

theorem Th14: :: TRANSLAC:14

for b₁ being AffinPlane
for b₂ being Permutation of the carrier of b₁ st b₁ satisfies_Fano & b₁ satisfies_des & b₂ is_Tr holds
ex b₃ being Permutation of the carrier of b₁ st
( b₃ is_Tr & b₃ * b₃ = b₂ )

proof end;

theorem Th15: :: TRANSLAC:15

for b₁ being AffinPlane
for b₂ being Permutation of the carrier of b₁ st b₁ satisfies_Fano & b₂ is_Tr & b₂ * b₂ = id the carrier of b₁ holds
b₂ = id the carrier of b₁

proof end;

theorem Th16: :: TRANSLAC:16

for b₁ being AffinPlane
for b₂, b₃, b₄ being Permutation of the carrier of b₁ st b₁ satisfies_des & b₁ satisfies_Fano & b₂ is_Tr & b₃ is_Tr & b₄ is_Tr & b₂ = b₃ * b₃ & b₂ = b₄ * b₄ holds
b₃ = b₄

proof end;