:: PENCIL_3 semantic presentation

theorem Th1: :: PENCIL_3:1

for b₁ being non empty non void TopStruct
for b₂ being Collineation of b₁
for b₃, b₄ being Point of b₁ st b₃,b₄ are_collinear holds
b₂ . b₃,b₂ . b₄ are_collinear

proof end;

theorem Th2: :: PENCIL_3:2

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being 1-sorted-yielding non-Trivial-yielding ManySortedSet of b₁ holds not b₃ . b₂ is trivial

proof end;

theorem Th3: :: PENCIL_3:3

for b₁ being non void identifying_close_blocks TopStruct st b₁ is strongly_connected holds
b₁ is without_isolated_points

proof end;

theorem Th4: :: PENCIL_3:4

for b₁ being non empty non void identifying_close_blocks TopStruct st b₁ is strongly_connected holds
b₁ is connected

proof end;

theorem Th5: :: PENCIL_3:5

for b₁ being non void non degenerated TopStruct
for b₂ being Block of b₁ holds
not for b₃ being Point of b₁ holds b₃ in b₂

proof end;

theorem Th6: :: PENCIL_3:6

for b₁ being non empty set
for b₂ being non-Empty TopStruct-yielding ManySortedSet of b₁
for b₃ being Point of (Segre_Product b₂) holds b₃ is Element of Carrier b₂

proof end;

theorem Th7: :: PENCIL_3:7

for b₁ being non empty set
for b₂ being 1-sorted-yielding ManySortedSet of b₁
for b₃ being Element of b₁ holds (Carrier b₂) . b₃ = [#] (b₂ . b₃)

proof end;

theorem Th8: :: PENCIL_3:8

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being TopStruct-yielding non-Trivial-yielding ManySortedSet of b₁ ex b₄ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₃ st
( indx b₄ = b₂ & product b₄ is Segre-Coset of b₃ )

proof end;

theorem Th9: :: PENCIL_3:9

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being TopStruct-yielding non-Trivial-yielding ManySortedSet of b₁
for b₄ being Point of (Segre_Product b₃) ex b₅ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₃ st
( indx b₅ = b₂ & product b₅ is Segre-Coset of b₃ & b₄ in product b₅ )

proof end;

theorem Th10: :: PENCIL_3:10

for b₁ being non empty set
for b₂ being TopStruct-yielding non-Trivial-yielding ManySortedSet of b₁
for b₃ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st product b₃ is Segre-Coset of b₂ holds
b₃ . (indx b₃) = [#] (b₂ . (indx b₃))

proof end;

theorem Th11: :: PENCIL_3:11

for b₁ being non empty set
for b₂ being TopStruct-yielding non-Trivial-yielding ManySortedSet of b₁
for b₃, b₄ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st product b₃ is Segre-Coset of b₂ & product b₄ is Segre-Coset of b₂ & indx b₃ = indx b₄ & product b₃ meets product b₄ holds
b₃ = b₄

proof end;

theorem Th12: :: PENCIL_3:12

for b₁ being non empty set
for b₂ being PLS-yielding ManySortedSet of b₁
for b₃ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂
for b₄ being Block of (b₂ . (indx b₃)) holds product (b₃ +* (indx b₃),b₄) is Block of (Segre_Product b₂)

proof end;

theorem Th13: :: PENCIL_3:13

for b₁ being non empty set
for b₂ being PLS-yielding ManySortedSet of b₁
for b₃ being Element of b₁
for b₄ being Point of (b₂ . b₃)
for b₅ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st b₃ <> indx b₅ holds
b₅ +* b₃,{b₄} is non trivial-yielding Segre-like ManySortedSubset of Carrier b₂

proof end;

theorem Th14: :: PENCIL_3:14

for b₁ being non empty set
for b₂ being PLS-yielding ManySortedSet of b₁
for b₃ being Element of b₁
for b₄ being Subset of (b₂ . b₃)
for b₅ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ holds product (b₅ +* b₃,b₄) is Subset of (Segre_Product b₂)

proof end;

theorem Th15: :: PENCIL_3:15

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃ being Element of b₁ holds
( not {b₂} . b₃ is empty & {b₂} . b₃ is trivial )

proof end;

theorem Th16: :: PENCIL_3:16

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being PLS-yielding ManySortedSet of b₁
for b₄ being Block of (b₃ . b₂)
for b₅ being Element of Carrier b₃ holds product ({b₅} +* b₂,b₄) is Block of (Segre_Product b₃)

proof end;

theorem Th17: :: PENCIL_3:17

for b₁ being non empty set
for b₂ being PLS-yielding ManySortedSet of b₁
for b₃, b₄ being Point of (Segre_Product b₂) st b₃ <> b₄ holds
( b₃,b₄ are_collinear iff for b₅, b₆ being ManySortedSet of b₁ st b₅ = b₃ & b₆ = b₄ holds
ex b₇ being Element of b₁ st
( ( for b₈, b₉ being Point of (b₂ . b₇) st b₈ = b₅ . b₇ & b₉ = b₆ . b₇ holds
( b₈ <> b₉ & b₈,b₉ are_collinear ) ) & ( for b₈ being Element of b₁ st b₈ <> b₇ holds
b₅ . b₈ = b₆ . b₈ ) ) )

proof end;

theorem Th18: :: PENCIL_3:18

for b₁ being non empty set
for b₂ being PLS-yielding ManySortedSet of b₁
for b₃ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂
for b₄ being Point of (b₂ . (indx b₃)) ex b₅ being ManySortedSet of b₁ st
( b₅ in product b₃ & {(b₅ +* (indx b₃),b₄)} = product (b₃ +* (indx b₃),{b₄}) )

proof end;

definition

let c₁ be non empty finite set ;
let c₂, c₃ be ManySortedSet of c₁;
func diff c₂,c₃ -> Nat equals :: PENCIL_3:def 1
Card { b₁ where B is Element of a₁ : a₂ . b₁ <> a₃ . b₁ } ;
correctness

proof end;

end;

:: deftheorem Def1 defines diff PENCIL_3:def 1 :

theorem Th19: :: PENCIL_3:19

for b₁ being non empty finite set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being Element of b₁ st b₂ . b₄ <> b₃ . b₄ holds
diff b₂,b₃ = (diff b₂,(b₃ +* b₄,(b₂ . b₄))) + 1

proof end;

definition

let c₁ be non empty set ;
let c₂ be PLS-yielding ManySortedSet of c₁;
let c₃, c₄ be Segre-Coset of c₂;
pred c₃ '||' c₄ means :Def2: :: PENCIL_3:def 2
for b₁ being Point of (Segre_Product a₂) st b₁ in a₃ holds
ex b₂ being Point of (Segre_Product a₂) st
( b₂ in a₄ & b₁,b₂ are_collinear );

end;

:: deftheorem Def2 defines '||' PENCIL_3:def 2 :

theorem Th20: :: PENCIL_3:20

for b₁ being non empty set
for b₂ being PLS-yielding ManySortedSet of b₁
for b₃, b₄ being Segre-Coset of b₂ st b₃ '||' b₄ holds
for b₅ being Collineation of (Segre_Product b₂)
for b₆, b₇ being Segre-Coset of b₂ st b₆ = b₅ .: b₃ & b₇ = b₅ .: b₄ holds
b₆ '||' b₇

proof end;

theorem Th21: :: PENCIL_3:21

for b₁ being non empty set
for b₂ being PLS-yielding ManySortedSet of b₁
for b₃, b₄ being Segre-Coset of b₂ st b₃ misses b₄ holds
( b₃ '||' b₄ iff for b₅, b₆ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st b₃ = product b₅ & b₄ = product b₆ holds
( indx b₅ = indx b₆ & ex b₇ being Element of b₁ st
( b₇ <> indx b₅ & ( for b₈ being Element of b₁ st b₈ <> b₇ holds
b₅ . b₈ = b₆ . b₈ ) & ( for b₈, b₉ being Point of (b₂ . b₇) st b₅ . b₇ = {b₈} & b₆ . b₇ = {b₉} holds
b₈,b₉ are_collinear ) ) ) )

proof end;

theorem Th22: :: PENCIL_3:22

for b₁ being non empty finite set
for b₂ being PLS-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is connected ) holds
for b₃ being Element of b₁
for b₄ being Point of (b₂ . b₃)
for b₅, b₆ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st product b₅ is Segre-Coset of b₂ & product b₆ is Segre-Coset of b₂ & b₅ = b₆ +* b₃,{b₄} & not b₄ in b₆ . b₃ holds
ex b₇ being FinSequence of bool the carrier of (Segre_Product b₂) st
( b₇ . 1 = product b₅ & b₇ . (len b₇) = product b₆ & ( for b₈ being Nat st b₈ in dom b₇ holds
b₇ . b₈ is Segre-Coset of b₂ ) & ( for b₈ being Nat st 1 <= b₈ & b₈ < len b₇ holds
for b₉, b₁₀ being Segre-Coset of b₂ st b₉ = b₇ . b₈ & b₁₀ = b₇ . (b₈ + 1) holds
( b₉ misses b₁₀ & b₉ '||' b₁₀ ) ) )

proof end;

theorem Th23: :: PENCIL_3:23

for b₁ being non empty finite set
for b₂ being PLS-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is connected ) holds
for b₃, b₄ being Segre-Coset of b₂ st b₃ misses b₄ holds
for b₅, b₆ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st b₃ = product b₅ & b₄ = product b₆ holds
( indx b₅ = indx b₆ iff ex b₇ being FinSequence of bool the carrier of (Segre_Product b₂) st
( b₇ . 1 = b₃ & b₇ . (len b₇) = b₄ & ( for b₈ being Nat st b₈ in dom b₇ holds
b₇ . b₈ is Segre-Coset of b₂ ) & ( for b₈ being Nat st 1 <= b₈ & b₈ < len b₇ holds
for b₉, b₁₀ being Segre-Coset of b₂ st b₉ = b₇ . b₈ & b₁₀ = b₇ . (b₈ + 1) holds
( b₉ misses b₁₀ & b₉ '||' b₁₀ ) ) ) )

proof end;

theorem Th24: :: PENCIL_3:24

for b₁ being non empty finite set
for b₂ being PLS-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is strongly_connected ) holds
for b₃ being Collineation of (Segre_Product b₂)
for b₄, b₅ being Segre-Coset of b₂
for b₆, b₇, b₈, b₉ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st b₄ = product b₆ & b₅ = product b₇ & b₃ .: b₄ = product b₈ & b₃ .: b₅ = product b₉ & indx b₆ = indx b₇ holds
indx b₈ = indx b₉

proof end;

theorem Th25: :: PENCIL_3:25

for b₁ being non empty finite set
for b₂ being PLS-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is strongly_connected ) holds
for b₃ being Collineation of (Segre_Product b₂) ex b₄ being Permutation of b₁ st
for b₅, b₆ being Element of b₁ holds
( b₄ . b₅ = b₆ iff for b₇ being Segre-Coset of b₂
for b₈, b₉ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st b₇ = product b₈ & b₃ .: b₇ = product b₉ & indx b₈ = b₅ holds
indx b₉ = b₆ )

proof end;

definition

let c₁ be non empty finite set ;
let c₂ be PLS-yielding ManySortedSet of c₁;
assume E26: for b₁ being Element of c₁ holds c₂ . b₁ is strongly_connected ;
let c₃ be Collineation of (Segre_Product c₂);
func permutation_of_indices c₃ -> Permutation of a₁ means :Def3: :: PENCIL_3:def 3
for b₁, b₂ being Element of a₁ holds
( a₄ . b₁ = b₂ iff for b₃ being Segre-Coset of a₂
for b₄, b₅ being non trivial-yielding Segre-like ManySortedSubset of Carrier a₂ st b₃ = product b₄ & a₃ .: b₃ = product b₅ & indx b₄ = b₁ holds
indx b₅ = b₂ );
existence by E26, Th25;
uniqueness

proof end;

end;

:: deftheorem Def3 defines permutation_of_indices PENCIL_3:def 3 :

definition

let c₁ be non empty finite set ;
let c₂ be PLS-yielding ManySortedSet of c₁;
assume E27: for b₁ being Element of c₁ holds c₂ . b₁ is strongly_connected ;
let c₃ be Collineation of (Segre_Product c₂);
let c₄ be non trivial-yielding Segre-like ManySortedSubset of Carrier c₂;
assume E28: product c₄ is Segre-Coset of c₂ ;
func canonical_embedding c₃,c₄ -> Function of (a₂ . (indx a₄)),(a₂ . ((permutation_of_indices a₃) . (indx a₄))) means :Def4: :: PENCIL_3:def 4
( a₅ is isomorphic & ( for b₁ being ManySortedSet of a₁ st b₁ is Point of (Segre_Product a₂) & b₁ in product a₄ holds
for b₂ being ManySortedSet of a₁ st b₂ = a₃ . b₁ holds
b₂ . ((permutation_of_indices a₃) . (indx a₄)) = a₅ . (b₁ . (indx a₄)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines canonical_embedding PENCIL_3:def 4 :

theorem Th26: :: PENCIL_3:26

for b₁ being non empty finite set
for b₂ being PLS-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is strongly_connected ) holds
for b₃ being Collineation of (Segre_Product b₂)
for b₄, b₅ being Segre-Coset of b₂ st b₄ misses b₅ & b₄ '||' b₅ holds
for b₆, b₇ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st product b₆ = b₄ & product b₇ = b₅ holds
canonical_embedding b₃,b₆ = canonical_embedding b₃,b₇

proof end;

theorem Th27: :: PENCIL_3:27

for b₁ being non empty finite set
for b₂ being PLS-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is strongly_connected ) holds
for b₃ being Collineation of (Segre_Product b₂)
for b₄, b₅ being non trivial-yielding Segre-like ManySortedSubset of Carrier b₂ st product b₄ is Segre-Coset of b₂ & product b₅ is Segre-Coset of b₂ & indx b₄ = indx b₅ holds
canonical_embedding b₃,b₄ = canonical_embedding b₃,b₅

proof end;

definition

let c₁ be non empty finite set ;
let c₂ be PLS-yielding ManySortedSet of c₁;
assume E30: for b₁ being Element of c₁ holds c₂ . b₁ is strongly_connected ;
let c₃ be Collineation of (Segre_Product c₂);
let c₄ be Element of c₁;
func canonical_embedding c₃,c₄ -> Function of (a₂ . a₄),(a₂ . ((permutation_of_indices a₃) . a₄)) means :Def5: :: PENCIL_3:def 5
for b₁ being non trivial-yielding Segre-like ManySortedSubset of Carrier a₂ st product b₁ is Segre-Coset of a₂ & indx b₁ = a₄ holds
a₅ = canonical_embedding a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines canonical_embedding PENCIL_3:def 5 :

theorem Th28: :: PENCIL_3:28

for b₁ being non empty finite set
for b₂ being PLS-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is strongly_connected ) holds
for b₃ being Collineation of (Segre_Product b₂) ex b₄ being Permutation of b₁ex b₅ being Function-yielding ManySortedSet of b₁ st
for b₆ being Element of b₁ holds
( b₅ . b₆ is Function of (b₂ . b₆),(b₂ . (b₄ . b₆)) & ( for b₇ being Function of (b₂ . b₆),(b₂ . (b₄ . b₆)) st b₇ = b₅ . b₆ holds
b₇ is isomorphic ) & ( for b₇ being Point of (Segre_Product b₂)
for b₈ being ManySortedSet of b₁ st b₈ = b₇ holds
for b₉ being ManySortedSet of b₁ st b₉ = b₃ . b₇ holds
for b₁₀ being Function of (b₂ . b₆),(b₂ . (b₄ . b₆)) st b₁₀ = b₅ . b₆ holds
b₉ . (b₄ . b₆) = b₁₀ . (b₈ . b₆) ) )

proof end;