:: PENCIL_3 semantic presentation

for S being non empty non void TopStruct
for f being Collineation of S
for p, q being Point of S st p,q are_collinear holds
f . p,f . q are_collinear

proof end;

theorem Th2: :: PENCIL_3:2

for I being non empty set
for i being Element of I
for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial

proof end;

theorem Th3: :: PENCIL_3:3

for S being non void identifying_close_blocks TopStruct st S is strongly_connected holds
S is without_isolated_points

proof end;

theorem Th4: :: PENCIL_3:4

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

proof end;

theorem :: PENCIL_3:5

for S being non void non degenerated TopStruct
for L being Block of S holds
not for x being Point of S holds x in L

proof end;

theorem Th6: :: PENCIL_3:6

for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I
for p being Point of (Segre_Product A) holds p is Element of Carrier A

proof end;

theorem Th7: :: PENCIL_3:7

for I being non empty set
for A being 1-sorted-yielding ManySortedSet of I
for x being Element of I holds (Carrier A) . x = [#] (A . x)

proof end;

theorem Th8: :: PENCIL_3:8

for I being non empty set
for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A )

proof end;

theorem Th9: :: PENCIL_3:9

for I being non empty set
for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A & p in product L )

proof end;

theorem Th10: :: PENCIL_3:10

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

proof end;

theorem Th11: :: PENCIL_3:11

for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for L1, L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 holds
L1 = L2

proof end;

theorem Th12: :: PENCIL_3:12

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for B being Block of (A . (indx L)) holds product (L +* (indx L),B) is Block of (Segre_Product A)

proof end;

theorem Th13: :: PENCIL_3:13

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for i being Element of I
for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* i,{p} is non trivial-yielding Segre-like ManySortedSubset of Carrier A

proof end;

theorem Th14: :: PENCIL_3:14

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for i being Element of I
for S being Subset of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* i,S) is Subset of (Segre_Product A)

proof end;

theorem Th15: :: PENCIL_3:15

for I being non empty set
for P being ManySortedSet of I
for i being Element of I holds
( not {P} . i is empty & {P} . i is trivial )

proof end;

theorem Th16: :: PENCIL_3:16

for I being non empty set
for i being Element of I
for A being PLS-yielding ManySortedSet of I
for B being Block of (A . i)
for P being Element of Carrier A holds product ({P} +* i,B) is Block of (Segre_Product A)

proof end;

theorem Th17: :: PENCIL_3:17

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for p, q being Point of (Segre_Product A) st p <> q holds
( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )

proof end;

theorem Th18: :: PENCIL_3:18

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for x being Point of (A . (indx b)) ex p being ManySortedSet of I st
( p in product b & {(p +* (indx b),x)} = product (b +* (indx b),{x}) )

proof end;

definition

let I be non empty finite set ;
let b1, b2 be ManySortedSet of I;
func diff b1,b2 -> Nat equals :: PENCIL_3:def 1
Card { i where i is Element of I : b1 . i <> b2 . i } ;
correctness

proof end;

end;

:: deftheorem defines diff PENCIL_3:def 1 :

theorem Th19: :: PENCIL_3:19

for I being non empty finite set
for b1, b2 being ManySortedSet of I
for i being Element of I st b1 . i <> b2 . i holds
diff b1,b2 = (diff b1,(b2 +* i,(b1 . i))) + 1

proof end;

definition

let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
let B1, B2 be Segre-Coset of A;
pred B1 '||' B2 means :Def2: :: PENCIL_3:def 2
for x being Point of (Segre_Product A) st x in B1 holds
ex y being Point of (Segre_Product A) st
( y in B2 & x,y are_collinear );

end;

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

theorem Th20: :: PENCIL_3:20

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st B1 '||' B2 holds
for f being Collineation of (Segre_Product A)
for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2

proof end;

theorem Th21: :: PENCIL_3:21

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st B1 misses B2 holds
( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) )

proof end;

theorem Th22: :: PENCIL_3:22

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds
for i being Element of I
for p being Point of (A . i)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & b1 = b2 +* i,{p} & not p in b2 . i holds
ex D being FinSequence of bool the carrier of (Segre_Product A) st
( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds
D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )

proof end;

theorem Th23: :: PENCIL_3:23

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds
for B1, B2 being Segre-Coset of A st B1 misses B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st
( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds
D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )

proof end;

theorem Th24: :: PENCIL_3:24

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4

proof end;

theorem Th25: :: PENCIL_3:25

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A) ex s being Permutation of I st
for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )

proof end;

definition

let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume A1: for i being Element of I holds A . i is strongly_connected ;
let f be Collineation of (Segre_Product A);
func permutation_of_indices f -> Permutation of I means :Def3: :: PENCIL_3:def 3
for i, j being Element of I holds
( it . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j );
existence by A1, Th25;
uniqueness

proof end;

end;

:: deftheorem Def3 defines permutation_of_indices PENCIL_3:def 3 :

definition

let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume A1: for i being Element of I holds A . i is strongly_connected ;
let f be Collineation of (Segre_Product A);
let b1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A;
assume A2: product b1 is Segre-Coset of A ;
func canonical_embedding f,b1 -> Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) means :Def4: :: PENCIL_3:def 4
( it is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = it . (a . (indx b1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines canonical_embedding PENCIL_3:def 4 :

theorem Th26: :: PENCIL_3:26

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding f,b1 = canonical_embedding f,b2

proof end;

theorem Th27: :: PENCIL_3:27

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds
canonical_embedding f,b1 = canonical_embedding f,b2

proof end;

definition

let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume A1: for i being Element of I holds A . i is strongly_connected ;
let f be Collineation of (Segre_Product A);
let i be Element of I;
func canonical_embedding f,i -> Function of (A . i),(A . ((permutation_of_indices f) . i)) 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 = i holds
it = canonical_embedding f,b;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines canonical_embedding PENCIL_3:def 5 :

theorem :: PENCIL_3:28

for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A) ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st
for i being Element of I holds
( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) )

proof end;