:: 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{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> FinSequence of F₃(), P₁[ set , set ] } :

ex g being one-to-one FinSequence of F₃() st
( F₁() = g . 1 & F₂() = g . (len g) & rng g c= rng F₄() & ( for j being Element of NAT st 1 <= j & j < len g holds
P₁[g . j,g . (j + 1)] ) )

provided

A1: ( F₁() = F₄() . 1 & F₂() = F₄() . (len F₄()) ) and
A2: for i being Element of NAT
for d1, d2 being set st 1 <= i & i < len F₄() & d1 = F₄() . i & d2 = F₄() . (i + 1) holds
P₁[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 b₁ being Subset of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b₁ = 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 b₃ being Subset of (Segre_Product A) holds
( b₃ is Segre-Coset of A iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b₃ = 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 b₁ being Function of S,S st b₁ 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;