:: On the Characterization of Collineations of the Segre Product of Strongly Connected Partial Linear Spaces
::
:: Copyright (c) 2004-2021 Association of Mizar Users

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
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 () 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 () . 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 () 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 ()
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 ()
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 {P} . i is 1 -element
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 ()
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 () 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
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
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 :: PENCIL_3:def 2
for x being Point of () st x in B1 holds
ex y being Point of () st
( y in B2 & x,y are_collinear );
end;

:: deftheorem 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 () st x in B1 holds
ex y being Point of () st
( y in B2 & 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 ()
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 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 () 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 () 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 ()
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 () 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 ();
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 ;
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 ()
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 ();
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 . ( . (indx b1))) means :Def4: :: PENCIL_3:def 4
( it is isomorphic & ( for a being ManySortedSet of I st a is Point of () & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ( . (indx b1)) = it . (a . (indx b1)) ) );
existence
ex b1 being Function of (A . (indx b1)),(A . ( . (indx b1))) st
( b1 is isomorphic & ( for a being ManySortedSet of I st a is Point of () & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ( . (indx b1)) = b1 . (a . (indx b1)) ) )
proof end;
uniqueness
for b1, b2 being Function of (A . (indx b1)),(A . ( . (indx b1))) st b1 is isomorphic & ( for a being ManySortedSet of I st a is Point of () & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ( . (indx b1)) = b1 . (a . (indx b1)) ) & b2 is isomorphic & ( for a being ManySortedSet of I st a is Point of () & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ( . (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 ()
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 . ( . (indx b1))) holds
( b5 = canonical_embedding (f,b1) iff ( b5 is isomorphic & ( for a being ManySortedSet of I st a is Point of () & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ( . (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 ()
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 ()
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 ();
let i be Element of I;
func canonical_embedding (f,i) -> Function of (A . i),(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 = i holds
it = canonical_embedding (f,b);
existence
ex b1 being Function of (A . i),(A . ()) 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 . ()) 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 ()
for i being Element of I
for b5 being Function of (A . i),(A . ()) 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
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 () 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 ()
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;