:: On the Characterization of Collineations of the Segre Product of Strongly Connected Partial Linear Spaces
:: by Adam Naumowicz
::
:: Received October 18, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: PENCIL_3:1
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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 )
proofend;

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 )
proofend;

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))
proofend;

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
proofend;

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)
proofend;

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
proofend;

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)
proofend;

theorem Th15: :: PENCIL_3:15
for I being non empty set
for P being ManySortedSet of I
for i being Element of I holds {P} . i is 1 -element
proofend;

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)
proofend;

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 &amp; q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i &amp; b = q1 . i holds
( a <> b &amp; a,b are_collinear ) ) &amp; ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )
proofend;

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 &amp; {(p +* ((indx b),x))} = product (b +* ((indx b),{x})) )
proofend;

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;
proofend;
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
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
proofend;

begin

definition
let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
let B1, B2 be Segre-Coset of A;
predB1 '||' 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 &amp; 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 &amp; x,y are_collinear ) );

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 &amp; C2 = f .: B2 holds
C1 '||' C2
proofend;

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 &amp; B2 = product b2 holds
( indx b1 = indx b2 &amp; ex r being Element of I st
( r <> indx b1 &amp; ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) &amp; ( for c1, c2 being Point of (A . r) st b1 . r = {c1} &amp; b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) )
proofend;

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 b2 is Segre-Coset of A &amp; b1 = b2 +* (i,{p}) &amp; not p in b2 . i holds
ex D being FinSequence of bool the carrier of (Segre_Product A) st
( D . 1 = product b1 &amp; D . (len D) = product b2 &amp; ( for i being Nat st i in dom D holds
D . i is Segre-Coset of A ) &amp; ( for i being Nat st 1 <= i &amp; i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i &amp; Di1 = D . (i + 1) holds
( Di misses Di1 &amp; Di '||' Di1 ) ) )
proofend;

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 &amp; 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 &amp; D . (len D) = B2 &amp; ( for i being Nat st i in dom D holds
D . i is Segre-Coset of A ) &amp; ( for i being Nat st 1 <= i &amp; i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i &amp; Di1 = D . (i + 1) holds
( Di misses Di1 &amp; Di '||' Di1 ) ) ) )
proofend;

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 &amp; B2 = product b2 &amp; f .: B1 = product b3 &amp; f .: B2 = product b4 &amp; indx b1 = indx b2 holds
indx b3 = indx b4
proofend;

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 &amp; f .: B1 = product b2 &amp; indx b1 = i holds
indx b2 = j )
proofend;

definition
let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume B1: 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 &amp; f .: B1 = product b2 &amp; 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 &amp; f .: B1 = product b2 &amp; indx b1 = i holds
indx b2 = j ) by B1, 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 &amp; f .: B1 = product b2 &amp; indx b1 = i holds
indx b2 = j ) ) &amp; ( 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 &amp; f .: B1 = product b2 &amp; indx b1 = i holds
indx b2 = j ) ) holds
b1 = b2
proofend;
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 &amp; f .: B1 = product b2 &amp; indx b1 = i holds
indx b2 = j ) );

begin

definition
let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume B1: 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 B2: 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 &amp; ( for a being ManySortedSet of I st a is Point of (Segre_Product A) &amp; 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 &amp; ( for a being ManySortedSet of I st a is Point of (Segre_Product A) &amp; 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)) ) )
proofend;
uniqueness
 for b1, b2 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st b1 is isomorphic &amp; ( for a being ManySortedSet of I st a is Point of (Segre_Product A) &amp; 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)) ) &amp; b2 is isomorphic &amp; ( for a being ManySortedSet of I st a is Point of (Segre_Product A) &amp; 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
proofend;
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 &amp; ( for a being ManySortedSet of I st a is Point of (Segre_Product A) &amp; 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
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 &amp; B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 &amp; product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)
proofend;

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 &amp; product b2 is Segre-Coset of A &amp; indx b1 = indx b2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)
proofend;

definition
let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume B1: 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 &amp; 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 &amp; indx b = i holds
b1 = canonical_embedding (f,b)
proofend;
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 &amp; indx b = i holds
b1 = canonical_embedding (f,b) ) &amp; ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A &amp; indx b = i holds
b2 = canonical_embedding (f,b) ) holds
b1 = b2
proofend;
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 &amp; indx b = i holds
b5 = canonical_embedding (f,b) );

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)) &amp; ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds
m is isomorphic ) &amp; ( 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) ) )
proofend;