:: by Adam Naumowicz

::

:: Received October 18, 2004

:: Copyright (c) 2004-2016 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

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

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

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

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

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

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)

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 )

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 )

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

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

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)

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

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)

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 {P} . i is 1 -element

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 (Segre_Product A)

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

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})) )

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;

coherence

card { i where i is Element of I : b1 . i <> b2 . i } is Nat;

end;
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 card { i where i is Element of I : b1 . i <> b2 . i } ;

coherence

card { i where i is Element of I : b1 . i <> b2 . i } is Nat;

proof 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 } ;

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

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;

end;
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 (Segre_Product A) st x in B1 holds

ex y being Point of (Segre_Product A) st

( y in B2 & x,y are_collinear );

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

:: 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 (Segre_Product A) st x in B1 holds

ex y being Point of (Segre_Product A) st

( y in B2 & x,y are_collinear ) );

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

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

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

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 (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 ) ) )

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 (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 ) ) ) )

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

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 )

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

ex b_{1} being Permutation of I st

for i, j being Element of I holds

( b_{1} . 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 b_{1}, b_{2} being Permutation of I st ( for i, j being Element of I holds

( b_{1} . 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

( b_{2} . 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

b_{1} = b_{2}

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

ex b

for i, j being Element of I holds

( b

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 b

( b

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

( b

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

b

proof 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 b_{4} being Permutation of I holds

( b_{4} = permutation_of_indices f iff for i, j being Element of I holds

( b_{4} . 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 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 b

( b

( b

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 ;

ex b_{1} being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st

( b_{1} 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)) = b_{1} . (a . (indx b1)) ) )

for b_{1}, b_{2} being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st b_{1} 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)) = b_{1} . (a . (indx b1)) ) & b_{2} 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)) = b_{2} . (a . (indx b1)) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) );

ex b

( b

for b being ManySortedSet of I st b = f . a holds

b . ((permutation_of_indices f) . (indx b1)) = b

proof end;

uniqueness for b

for b being ManySortedSet of I st b = f . a holds

b . ((permutation_of_indices f) . (indx b1)) = b

for b being ManySortedSet of I st b = f . a holds

b . ((permutation_of_indices f) . (indx b1)) = b

b

proof 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 b_{5} being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) holds

( b_{5} = canonical_embedding (f,b1) iff ( b_{5} 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)) = b_{5} . (a . (indx b1)) ) ) );

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 b

( b

for b being ManySortedSet of I st b = f . a holds

b . ((permutation_of_indices f) . (indx b1)) = b

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)

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)

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;

ex b_{1} 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

b_{1} = canonical_embedding (f,b)

for b_{1}, b_{2} 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

b_{1} = 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

b_{2} = canonical_embedding (f,b) ) holds

b_{1} = b_{2}

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

ex 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

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being Function of (A . i),(A . ((permutation_of_indices f) . i)) holds

( b_{5} = 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

b_{5} = canonical_embedding (f,b) );

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 b

( b

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)) & ( 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) ) )

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;