:: PENCIL_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: PENCIL_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
coherence
Card { i where i is Element of I : b1 . i <> b2 . i } is Nat
;
proof end;
end;

:: deftheorem defines diff PENCIL_3:def 1 :
for I being non empty finite set
for b1, b2 being ManySortedSet of I holds diff b1,b2 = Card { i where i is Element of I : b1 . i <> b2 . i } ;

theorem Th19: :: PENCIL_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A holds
( B1 '||' B2 iff 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 ) );

theorem Th20: :: PENCIL_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Permutation of I st
for i, j being Element of I holds
( b1 . 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 )
by A1, Th25;
uniqueness
for b1, b2 being Permutation of I st ( for i, j being Element of I holds
( b1 . 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 ) ) & ( for i, j being Element of I holds
( b2 . 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 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines permutation_of_indices PENCIL_3:def 3 :
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 b4 being Permutation of I holds
( b4 = permutation_of_indices f iff for i, j being Element of I holds
( b4 . 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 ) );

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
ex b1 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st
( b1 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)) = b1 . (a . (indx b1)) ) )
proof end;
uniqueness
for b1, b2 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st b1 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)) = b1 . (a . (indx b1)) ) & b2 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)) = b2 . (a . (indx b1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines canonical_embedding PENCIL_3:def 4 :
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 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A holds
for b5 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) holds
( b5 = canonical_embedding f,b1 iff ( b5 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)) = b5 . (a . (indx b1)) ) ) );

theorem Th26: :: PENCIL_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Function of (A . i),(A . ((permutation_of_indices f) . i)) st
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b1 = canonical_embedding f,b
proof end;
uniqueness
for b1, b2 being Function of (A . i),(A . ((permutation_of_indices f) . i)) st ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b1 = canonical_embedding f,b ) & ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b2 = canonical_embedding f,b ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines canonical_embedding PENCIL_3:def 5 :
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 i being Element of I
for b5 being Function of (A . i),(A . ((permutation_of_indices f) . i)) holds
( b5 = canonical_embedding f,i iff for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b5 = canonical_embedding f,b );

theorem :: PENCIL_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;