:: On Cosets in Segre's Product of Partial Linear Spaces
:: by Adam Naumowicz
::
:: Received August 14, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users


definition
let D be set ;
let p be FinSequence of D;
let i, j be Nat;
func Del (p,i,j) -> FinSequence of D equals :: PENCIL_2:def 1
(p | (i -' 1)) ^ (p /^ j);
coherence
(p | (i -' 1)) ^ (p /^ j) is FinSequence of D ;
end;

:: deftheorem defines Del PENCIL_2:def 1 :
for D being set
for p being FinSequence of D
for i, j being Nat holds Del (p,i,j) = (p | (i -' 1)) ^ (p /^ j);

theorem Th1: :: PENCIL_2:1
for D being set
for p being FinSequence of D
for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p
proof end;

theorem Th2: :: PENCIL_2:2
for D being set
for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p holds
len (Del (p,i,j)) = (((len p) - j) + i) - 1
proof end;

theorem Th3: :: PENCIL_2:3
for D being set
for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds
( i = 1 & j = len p )
proof end;

theorem Th4: :: PENCIL_2:4
for D being set
for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds
(Del (p,i,j)) . k = p . k
proof end;

theorem Th5: :: PENCIL_2:5
for p, q being FinSequence
for k being Element of NAT st (len p) + 1 <= k holds
(p ^ q) . k = q . (k - (len p))
proof end;

theorem Th6: :: PENCIL_2:6
for D being set
for p being FinSequence of D
for i, j, k being Element of NAT st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del (p,i,j)) . k = p . (((j -' i) + k) + 1)
proof end;

scheme :: PENCIL_2:sch 1
FinSeqOneToOne{ F1() -> set , F2() -> set , F3() -> set , F4() -> FinSequence of F3(), P1[ set , set ] } :
ex g being one-to-one FinSequence of F3() st
( F1() = g . 1 & F2() = g . (len g) & rng g c= rng F4() & ( for j being Element of NAT st 1 <= j & j < len g holds
P1[g . j,g . (j + 1)] ) )
provided
A1: ( F1() = F4() . 1 & F2() = F4() . (len F4()) ) and
A2: for i being Element of NAT
for d1, d2 being set st 1 <= i & i < len F4() & d1 = F4() . i & d2 = F4() . (i + 1) holds
P1[d1,d2]
proof end;

theorem Th7: :: PENCIL_2:7
for I being non empty set
for A being 1-sorted-yielding ManySortedSet of I
for L being ManySortedSubset of Carrier A
for i being Element of I
for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A
proof end;

definition
let I be non empty set ;
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I;
mode Segre-Coset of A -> Subset of (Segre_Product A) means :Def2: :: PENCIL_2:def 2
 ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( it = product L & L . (indx L) = [#] (A . (indx L)) );
existence
ex b1 being Subset of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b1 = product L & L . (indx L) = [#] (A . (indx L)) )
proof end;
end;

:: deftheorem Def2 defines Segre-Coset PENCIL_2:def 2 :
for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for b3 being Subset of (Segre_Product A) holds
( b3 is Segre-Coset of A iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b3 = product L & L . (indx L) = [#] (A . (indx L)) ) );

theorem Th8: :: PENCIL_2:8
for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds
B1 = B2
proof end;

definition
let S be TopStruct ;
let X, Y be Subset of S;
pred X,Y are_joinable means :: PENCIL_2:def 3
 ex f being FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) );
end;

:: deftheorem defines are_joinable PENCIL_2:def 3 :
for S being TopStruct
for X, Y being Subset of S holds
( X,Y are_joinable iff ex f being FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) ) );

theorem :: PENCIL_2:9
for S being TopStruct
for X, Y being Subset of S st X,Y are_joinable holds
ex f being one-to-one FinSequence of bool the carrier of S st
( X = f . 1 & Y = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )
proof end;

theorem Th10: :: PENCIL_2:10
for S being TopStruct
for X being Subset of S st X is closed_under_lines & X is strong holds
X,X are_joinable
proof end;

theorem Th11: :: PENCIL_2:11
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds
for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds
( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds
X1 . i = Y1 . i ) )
proof end;

theorem :: PENCIL_2:12
for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T st f is bijective holds
f " is bijective
proof end;

definition
let S, T be TopStruct ;
let f be Function of S,T;
attr f is isomorphic means :Def4: :: PENCIL_2:def 4
( f is bijective & f is open & f " is bijective & f " is open );
end;

:: deftheorem Def4 defines isomorphic PENCIL_2:def 4 :
for S, T being TopStruct
for f being Function of S,T holds
( f is isomorphic iff ( f is bijective & f is open & f " is bijective & f " is open ) );

registration
let S be non empty TopStruct ;
cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty total quasi_total isomorphic for Element of bool [: the carrier of S, the carrier of S:];
existence
ex b1 being Function of S,S st b1 is isomorphic
proof end;
end;

definition
let S be non empty TopStruct ;
mode Collineation of S is isomorphic Function of S,S;
end;

definition
let S be non empty non void TopStruct ;
let f be Collineation of S;
let l be Block of S;
:: original: .:
redefine func f .: l -> Block of S;
coherence
f .: l is Block of S
proof end;
end;

definition
let S be non empty non void TopStruct ;
let f be Collineation of S;
let l be Block of S;
:: original: "
redefine func f " l -> Block of S;
coherence
f " l is Block of S
proof end;
end;

theorem Th13: :: PENCIL_2:13
for S being non empty TopStruct
for f being Collineation of S holds f " is Collineation of S
proof end;

theorem Th14: :: PENCIL_2:14
for S being non empty TopStruct
for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f .: X is trivial
proof end;

theorem :: PENCIL_2:15
for S being non empty TopStruct
for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f " X is trivial
proof end;

theorem Th16: :: PENCIL_2:16
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is strong holds
f .: X is strong
proof end;

theorem :: PENCIL_2:17
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is strong holds
f " X is strong
proof end;

theorem Th18: :: PENCIL_2:18
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f .: X is closed_under_lines
proof end;

theorem :: PENCIL_2:19
for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f " X is closed_under_lines
proof end;

theorem Th20: :: PENCIL_2:20
for S being non empty non void TopStruct
for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f .: X,f .: Y are_joinable
proof end;

theorem :: PENCIL_2:21
for S being non empty non void TopStruct
for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f " X,f " Y are_joinable
proof end;

theorem Th22: :: PENCIL_2:22
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A
proof end;

theorem Th23: :: PENCIL_2:23
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being set holds
( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )
proof end;

theorem Th24: :: PENCIL_2:24
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A
proof end;

theorem :: PENCIL_2:25
for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f " B is Segre-Coset of A
proof end;