:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, NAT_1, FINSEQ_3, RELAT_1, ARYTM_1, ORDINAL4, RFINSEQ, SUBSET_1, TARSKI, XBOOLE_0, XXREAL_0, ARYTM_3, CARD_1, FUNCT_1, PARTFUN1, PRALG_1, PBOOLE, RLVECT_2, FUNCT_4, STRUCT_0, PENCIL_1, CARD_3, INTEGRA1, ZFMISC_1, PRE_TOPC, FUNCT_2, CAT_1, RCOMP_1, RELAT_2, PENCIL_2, WAYBEL18; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, XXREAL_0, RFINSEQ, CARD_1, FINSEQ_1, CARD_3, PRE_TOPC, PBOOLE, PZFMISC1, TOPS_2, T_0TOPSP, PRALG_1, FUNCT_7, WAYBEL18, PENCIL_1; constructors RFINSEQ, NAT_D, PZFMISC1, TOPS_2, T_0TOPSP, POLYNOM1, PENCIL_1, REAL_1, RELSET_1, PBOOLE, FUNCT_7; registrations SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, BORSUK_2, PENCIL_1, ORDINAL1, FINSEQ_1, RELSET_1, PRE_POLY, WAYBEL18; requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM; begin :: Preliminaries on finite sequences 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); end; theorem :: PENCIL_2:1 for D being set,p being FinSequence of D,i,j being Element of NAT holds rng Del(p,i,j) c= rng p; theorem :: PENCIL_2:2 for D being set,p being FinSequence of D,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; theorem :: PENCIL_2:3 for D being set,p being FinSequence of D,i,j being Element of NAT st i in dom p & j in dom p holds len Del(p,i,j) = 0 implies i=1 & j=len p; theorem :: PENCIL_2:4 for D being set,p being FinSequence of D,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; theorem :: PENCIL_2:5 for p,q being FinSequence, k being Element of NAT holds len p + 1 <= k implies (p^q).k=q.(k-len p); theorem :: PENCIL_2:6 for D being set,p being FinSequence of D,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); scheme :: PENCIL_2:sch 1 FinSeqOneToOne{X,Y,D()->set,f()-> FinSequence of D(),P[set,set]}: ex g being one-to-one FinSequence of D() st X() = g.1 & Y()=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 X() = f().1 & Y()=f().len f() and for i being Element of NAT, d1,d2 being set st 1 <= i & i < len f() & d1 =f().i & d2 = f().(i+1) holds P[d1,d2]; begin :: Segre cosets theorem :: 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; definition let I be non empty set; let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I; mode Segre-Coset of A -> Subset of Segre_Product A means :: PENCIL_2:def 2 ex L being Segre-like non trivial-yielding ManySortedSubset of Carrier A st it = product L & L.indx(L) = [#](A.indx(L)); end; theorem :: PENCIL_2:8 for I being non empty set for A being non-Trivial-yielding TopStruct-yielding ManySortedSet of I for B1,B2 being Segre-Coset of A st 2 c= card(B1 /\ B2) holds B1 = B2; 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 strong) & for i being Element of NAT st 1 <= i & i < len f holds 2 c= card((f.i) /\ (f.(i+1))); end; theorem :: PENCIL_2:9 for S being TopStruct for X,Y being Subset of S st X,Y are_joinable 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 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:10 for S being TopStruct for X being Subset of S st X is closed_under_lines strong holds X,X are_joinable; theorem :: 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 X is non trivial closed_under_lines strong & Y is non trivial closed_under_lines strong & X,Y are_joinable for X1,Y1 being Segre-like non trivial-yielding 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; begin :: Collineations of Segre product 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; definition let S,T be TopStruct; let f be Function of S,T; attr f is isomorphic means :: PENCIL_2:def 4 f is bijective open & f" is bijective open; end; registration let S be non empty TopStruct; cluster isomorphic for Function of S,S; 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; redefine func f.:l -> Block of S; end; definition let S be non empty non void TopStruct; let f be Collineation of S; let l be Block of S; redefine func f"l -> Block of S; end; theorem :: PENCIL_2:13 for S being non empty TopStruct for f being Collineation of S holds f" is Collineation of S; theorem :: PENCIL_2:14 for S being non empty TopStruct for f being Collineation of S for X being Subset of S st X is non trivial holds f.:X is non trivial; theorem :: PENCIL_2:15 for S being non empty TopStruct for f being Collineation of S for X being Subset of S st X is non trivial holds f"X is non trivial; theorem :: 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 ; 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; theorem :: 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; 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; theorem :: 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 X is non trivial & Y is non trivial & X,Y are_joinable holds f.:X,f.:Y are_joinable; 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 X is non trivial & Y is non trivial & X,Y are_joinable holds f"X,f"Y are_joinable; theorem :: 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 for W being Subset of Segre_Product A st W is non trivial strong closed_under_lines holds union {Y where Y is Subset of Segre_Product A : Y is non trivial strong closed_under_lines & W,Y are_joinable} is Segre-Coset of A; theorem :: 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 for B being set holds B is Segre-Coset of A iff ex W being Subset of Segre_Product A st W is non trivial strong closed_under_lines & B = union {Y where Y is Subset of Segre_Product A : Y is non trivial strong closed_under_lines & W,Y are_joinable }; theorem :: 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 for B being Segre-Coset of A for f being Collineation of Segre_Product A holds f.:B is Segre-Coset of A; 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 for B being Segre-Coset of A for f being Collineation of Segre_Product A holds f"B is Segre-Coset of A;