:: On Cosets in Segre's Product of Partial Linear Spaces :: by Adam Naumowicz :: :: Received August 14, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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)) proofend; 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) proofend; 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] proofend; begin 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 proofend; 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)) ) proofend; 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 proofend; definition let S be TopStruct ; let X, Y be Subset of S; predX,Y are_joinable means :Def3: :: 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 Def3 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))) ) ) proofend; 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 proofend; 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 set st i <> indx X1 holds X1 . i = Y1 . i ) ) proofend; begin 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 proofend; definition let S, T be TopStruct ; let f be Function of S,T; attrf 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 proofend; 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 funcf .: l -> Block of S; coherence f .: l is Block of S proofend; end; definition let S be non empty non void TopStruct ; let f be Collineation of S; let l be Block of S; :: original:" redefine funcf " l -> Block of S; coherence f " l is Block of S proofend; end; theorem Th13: :: PENCIL_2:13 for S being non empty TopStruct for f being Collineation of S holds f " is Collineation of S proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) } ) ) proofend; 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 proofend; 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 proofend;