:: On Cosets in Segre's Product of Partial Linear Spaces
:: by Adam Naumowicz
::
:: Received August 14, 2001
:: Copyright (c) 2001-2026 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;
definitions TARSKI, PBOOLE, PENCIL_1, XBOOLE_0;
equalities PENCIL_1, XBOOLE_0, STRUCT_0;
expansions TARSKI, PBOOLE, PENCIL_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, PBOOLE, CARD_3, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1,
FUNCT_7, YELLOW_6, PZFMISC1, PUA2MSS1, PRE_TOPC, FINSEQ_3, FUNCT_2,
TOPGRP_1, TOPS_2, T_0TOPSP, RELAT_1, PENCIL_1, RFINSEQ, FINSEQ_4,
FINSEQ_5, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, XREAL_0,
NAT_D;
schemes FINSEQ_1, NAT_1, INT_1;
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
(p|(i -' 1))^(p/^j);
coherence;
end;
theorem Th1:
for D being set,p being FinSequence of D,i,j being Element of NAT
holds rng Del(p,i,j) c= rng p
proof
let D be set,p be FinSequence of D,i,j be Element of NAT;
A1: rng (p/^j) c= rng p
proof
per cases;
suppose
A2: D is empty;
then A3: j>len p implies thesis;
j<=len p implies thesis by A2;
hence thesis by A3;
end;
suppose
D is non empty;
then reconsider E=D as non empty set;
reconsider r=p as FinSequence of E;
rng (r/^j) c= rng r by FINSEQ_5:33;
hence thesis;
end;
end;
rng (p|(i -' 1)) = rng (p|Seg(i -' 1)) by FINSEQ_1:def 16;
then
A4: rng (p|(i -' 1)) c= rng p by RELAT_1:70;
rng ((p|(i -' 1))^(p/^j)) = (rng (p|(i -' 1))) \/ rng (p/^j) by FINSEQ_1:31;
hence thesis by A4,A1,XBOOLE_1:8;
end;
theorem Th2:
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
proof
let D be set;
let p be FinSequence of D;
let i,j be Element of NAT;
assume that
A1: i in dom p and
A2: j in dom p;
A3: i <= len p by A1,FINSEQ_3:25;
1 <= i by A1,FINSEQ_3:25;
then
A4: i - 1 >= 1-1 by XREAL_1:9;
A5: i -' 1 <= i by NAT_D:35;
A6: j <= len p by A2,FINSEQ_3:25;
thus len Del(p,i,j) = len (p|(i -' 1)) + len (p/^j) by FINSEQ_1:22
.= i -' 1 + len (p/^j) by A3,A5,FINSEQ_1:59,XXREAL_0:2
.= i -' 1 + (len p - j) by A6,RFINSEQ:def 1
.= (i - 1) + (len p - j) by A4,XREAL_0:def 2
.=len p - j + i - 1;
end;
theorem Th3:
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
proof
let D be set;
let p be FinSequence of D;
let i,j be Element of NAT;
assume that
A1: i in dom p and
A2: j in dom p and
A3: len Del(p,i,j) = 0;
A4: 1 <= i by A1,FINSEQ_3:25;
j <= len p by A2,FINSEQ_3:25;
then
A5: len p - j >= 0 by XREAL_1:48;
A6: len p - j + i - 1 = 0 by A1,A2,A3,Th2;
then len p - j = 1 - i;
then 1 >= i by A5,XREAL_1:49;
hence i=1 by A4,XXREAL_0:1;
hence thesis by A6;
end;
theorem Th4:
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
proof
let D be set;
let p be FinSequence of D;
let i,j,k be Element of NAT;
assume that
A1: i in dom p and
A2: 1 <= k and
A3: k <= i-1;
A4: i <= len p by A1,FINSEQ_3:25;
A5: k <= i -' 1 by A3,XREAL_0:def 2;
A6: i -' 1 <= i by NAT_D:35;
then len (p|(i -' 1)) = i -' 1 by A4,FINSEQ_1:59,XXREAL_0:2;
then
A7: k in dom (p|(i -' 1)) by A2,A5,FINSEQ_3:25;
i -' 1 <= len p by A4,A6,XXREAL_0:2;
then k <= len p by A5,XXREAL_0:2;
then
A8: k in dom p by A2,FINSEQ_3:25;
thus Del(p,i,j).k = (p|(i -' 1)).k by A7,FINSEQ_1:def 7
.= (p|(i -' 1))/.k by A7,PARTFUN1:def 6
.= p/.k by A7,FINSEQ_4:70
.= p.k by A8,PARTFUN1:def 6;
end;
theorem Th5:
for p,q being FinSequence, k being Element of NAT holds len p + 1
<= k implies (p^q).k=q.(k-len p)
proof
let p,q be FinSequence;
let k be Element of NAT;
assume
A1: len p + 1 <= k;
per cases;
suppose
k <= len p + len q;
hence thesis by A1,FINSEQ_1:23;
end;
suppose
A2: not k <= len p + len q;
then k-len p > len q by XREAL_1:20;
then
A3: not k-len p in dom q by FINSEQ_3:25;
not k <= len (p^q) by A2,FINSEQ_1:22;
then not k in dom (p^q) by FINSEQ_3:25;
hence (p^q).k= {} by FUNCT_1:def 2
.= q.(k-len p) by A3,FUNCT_1:def 2;
end;
end;
theorem Th6:
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)
proof
let D be set;
let p be FinSequence of D;
let i,j,k be Element of NAT;
assume that
A1: i in dom p and
A2: j in dom p and
A3: i <= j and
A4: i <= k and
A5: k <= len p - j + i - 1;
A6: i -' 1 <= i by NAT_D:35;
i -' 1 <= i by NAT_D:35;
then k >= i -' 1 by A4,XXREAL_0:2;
then k - (i -' 1) >= (i -' 1) - (i -' 1) by XREAL_1:9;
then
A7: k - (i -' 1) = k -' (i -' 1) by XREAL_0:def 2;
A8: 1 <=i by A1,FINSEQ_3:25;
then
A9: i -' 1 + 1 <= k by A4,XREAL_1:235;
i-1 >= 1-1 by A8,XREAL_1:9;
then
A10: i -' 1 = i-1 by XREAL_0:def 2;
j-i >= i-i by A3,XREAL_1:9;
then
A11: j -' i = j-i by XREAL_0:def 2;
A12: j <= len p by A2,FINSEQ_3:25;
then
A13: len (p/^j) = len p - j by RFINSEQ:def 1;
k <= len p - j + (i - 1) by A5;
then
A14: k - (i -' 1) <= len p - j by A10,XREAL_1:20;
1 <= k - (i -' 1) by A9,XREAL_1:19;
then
A15: k - (i -' 1) in dom (p/^j) by A7,A13,A14,FINSEQ_3:25;
i <= len p by A1,FINSEQ_3:25;
then len (p|(i -' 1)) = i -' 1 by A6,FINSEQ_1:59,XXREAL_0:2;
hence Del(p,i,j).k = (p/^j).(k - (i -' 1)) by A9,Th5
.= p.(j + (k + (1 - i))) by A12,A10,A15,RFINSEQ:def 1
.= p.(j -'i + k + 1) by A11;
end;
scheme
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
A1: X() = f().1 & Y()=f().len f() and
A2: 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]
proof
defpred Q[Nat] means ex f being FinSequence of D() st len f = $1 & X() = f.1
& Y() = f.(len f) & rng f c= rng f() & for i being Element of NAT st 1 <= i & i
< len f holds P[f.i,f.(i+1)];
for i being Element of NAT st 1 <= i & i < len f() holds P[f().i,f().(i+
1)] by A2;
then
A3: ex k being Nat st Q[k] by A1;
consider k being Nat such that
A4: Q[k] & for n being Nat st Q[n] holds k <= n from NAT_1:sch 5(A3);
consider g being FinSequence of D() such that
A5: len g = k and
A6: X() = g.1 and
A7: Y() = g.(len g) and
A8: rng g c= rng f() and
A9: for i being Element of NAT st 1 <= i & i < len g holds P[g.i,g.(i+1
) ] by A4;
now
assume not g is one-to-one;
then consider x,y being object such that
A10: x in dom g and
A11: y in dom g and
A12: g.x = g.y and
A13: x <> y by FUNCT_1:def 4;
reconsider x,y as Element of NAT by A10,A11;
per cases by A13,XXREAL_0:1;
suppose
A14: x < y;
set d = Del(g,x+1,y);
A15: 1 <= y by A11,FINSEQ_3:25;
A16: x+1 >= 1 by NAT_1:11;
A17: y <= len g by A11,FINSEQ_3:25;
then
A18: x < len g by A14,XXREAL_0:2;
then x+1 <= len g by NAT_1:13;
then
A19: x+1 in dom g by A16,FINSEQ_3:25;
A20: x+1 <= y by A14,NAT_1:13;
then
A21: y - (x+1) >= 0 by XREAL_1:48;
A22: rng d c= rng f() & for i being Element of NAT st 1 <= i & i < len d
holds P[d.i,d.(i+1)]
proof
rng d c= rng g by Th1;
hence rng d c= rng f() by A8;
let i be Element of NAT;
assume that
A23: 1 <= i and
A24: i < len d;
per cases by XXREAL_0:1;
suppose
A25: i < x;
then i+1 <= (x+1)-1 by NAT_1:13;
then
A26: d.(i+1) = g.(i+1) by A19,Th4,NAT_1:11;
i <= (x+1)-1 by A25;
then
A27: d.i = g.i by A19,A23,Th4;
i < len g by A18,A25,XXREAL_0:2;
hence thesis by A9,A23,A27,A26;
end;
suppose
A28: i = x;
now
assume y=len g;
then x < len g - len g + (x+1) - 1 by A11,A19,A24,A28,Th2;
hence contradiction;
end;
then
A29: y < len g by A17,XXREAL_0:1;
then
A30: 0 < len g - y by XREAL_1:50;
then 0 < len g -' y by XREAL_0:def 2;
then 0+1 <= len g -' y by NAT_1:13;
then 1-1 <= (len g -' y) - 1 by XREAL_1:9;
then 0 <= (len g - y) - 1 by A30,XREAL_0:def 2;
then (i+1) + 0 <= (i+1) + ((len g - y) - 1) by XREAL_1:7;
then (i+1) + 0 <= (i+1) + (len g - y) - 1;
then
A31: d.(i+1) = g.(y -'(x+1) + (i+1) + 1) by A11,A20,A19,A28,Th6
.= g.(y+1) by A20,A28,XREAL_1:235;
i <= (x+1)-1 by A28;
then d.i = g.y by A12,A19,A23,A28,Th4;
hence thesis by A9,A15,A29,A31;
end;
suppose
i > x;
then
A32: x+1 <= i by NAT_1:13;
A33: len g - y >= 0 by A17,XREAL_1:48;
i < len g - y + (x+1) - 1 by A11,A19,A24,Th2;
then
A34: i < len g -' y + (x+1) - 1 by A33,XREAL_0:def 2;
then i+1 <= len g -' y + x by NAT_1:13;
then i+1 <= len g - y + x + 1 - 1 by A33,XREAL_0:def 2;
then
A35: i+1 <= len g - y + (x+1) - 1;
i < len g -' y + x + 1 - 1 by A34;
then i < len g - y + x by A33,XREAL_0:def 2;
then i - x < len g - y + x - x by XREAL_1:9;
then i - x + y < len g - y + y by XREAL_1:8;
then y - x - 1 + i + 1 < len g;
then
A36: y -'(x+1) + i + 1 < len g by A21,XREAL_0:def 2;
i <= i+1 by NAT_1:11;
then x+1 <= i+1 by A32,XXREAL_0:2;
then
A37: d.(i+1) = g.(y -'(x+1) + (i+1) + 1) by A11,A20,A19,A35,Th6
.= g.(y -'(x+1) + i + 1 + 1);
i <= len g - y + (x+1) - 1 by A11,A19,A24,Th2;
then d.i = g.(y -'(x+1) + i + 1) by A11,A20,A19,A32,Th6;
hence thesis by A9,A37,A36,NAT_1:11;
end;
end;
A38: Y() = d.(len d)
proof
per cases;
suppose
A39: len d <= x;
now
assume len d = 0;
then x+1 = 0+1 by A11,A19,Th3;
hence contradiction by A10,FINSEQ_3:24;
end;
then
A40: 0+1 <= len d by NAT_1:13;
len d <= (x+1)-1 by A39;
then
A41: d.len d = g.len d by A19,A40,Th4;
len g - y + (x+1) - 1 <= x by A11,A19,A39,Th2;
then len g - y + x + 1 - 1 <= x;
then len g - y <= 0 by XREAL_1:29;
then len g <= y by XREAL_1:50;
then
A42: len g = y by A17,XXREAL_0:1;
then x <= len g - y + (x+1) - 1;
hence thesis by A7,A11,A12,A19,A42,A41,Th2;
end;
suppose
len d > x;
then
A43: x+1 <= len d by NAT_1:13;
len d = len g - y + (x+1) - 1 by A11,A19,Th2;
hence d.len d = g.(y -'(x+1) + (len g - y + (x+1) - 1) + 1) by A11
,A20,A19,A43,Th6
.= g.(y - (x+1) + ((x+1) + ((len g - y) - 1)) + 1) by A20,
XREAL_1:233
.= Y() by A7;
end;
end;
1 <= (x+1)-1 by A10,FINSEQ_3:25;
then
A44: X() = d.1 by A6,A19,Th4;
0 < --(y - x) by A14,XREAL_1:50;
then -(y - x) < 0;
then len g + - (y - x) < len g + 0 by XREAL_1:8;
then len g - y + (x+1) - 1 < len g;
then len d < len g by A11,A19,Th2;
hence contradiction by A4,A5,A44,A38,A22;
end;
suppose
A45: y < x;
set d = Del(g,y+1,x);
A46: 1 <= x by A10,FINSEQ_3:25;
A47: y+1 >= 1 by NAT_1:11;
A48: x <= len g by A10,FINSEQ_3:25;
then
A49: y < len g by A45,XXREAL_0:2;
then y+1 <= len g by NAT_1:13;
then
A50: y+1 in dom g by A47,FINSEQ_3:25;
A51: y+1 <= x by A45,NAT_1:13;
then
A52: x - (y+1) >= 0 by XREAL_1:48;
A53: rng d c= rng f() & for i being Element of NAT st 1 <= i & i < len
d holds P[d.i,d.(i+1)]
proof
rng d c= rng g by Th1;
hence rng d c= rng f() by A8;
let i be Element of NAT;
assume that
A54: 1 <= i and
A55: i < len d;
per cases by XXREAL_0:1;
suppose
A56: i < y;
then i+1 <= (y+1)-1 by NAT_1:13;
then
A57: d.(i+1) = g.(i+1) by A50,Th4,NAT_1:11;
i <= (y+1)-1 by A56;
then
A58: d.i = g.i by A50,A54,Th4;
i < len g by A49,A56,XXREAL_0:2;
hence thesis by A9,A54,A58,A57;
end;
suppose
A59: i = y;
now
assume x=len g;
then y < len g - len g + (y+1) - 1 by A10,A50,A55,A59,Th2;
hence contradiction;
end;
then
A60: x < len g by A48,XXREAL_0:1;
then
A61: 0 < len g - x by XREAL_1:50;
then 0 < len g -' x by XREAL_0:def 2;
then 0+1 <= len g -' x by NAT_1:13;
then 1-1 <= (len g -' x) - 1 by XREAL_1:9;
then 0 <= (len g - x) - 1 by A61,XREAL_0:def 2;
then (i+1) + 0 <= (i+1) + ((len g - x) - 1) by XREAL_1:7;
then (i+1) + 0 <= (i+1) + (len g - x) - 1;
then
A62: d.(i+1) = g.(x -'(y+1) + (i+1) + 1) by A10,A51,A50,A59,Th6
.= g.(x+1) by A51,A59,XREAL_1:235;
i <= (y+1)-1 by A59;
then d.i = g.x by A12,A50,A54,A59,Th4;
hence thesis by A9,A46,A60,A62;
end;
suppose
i > y;
then
A63: y+1 <= i by NAT_1:13;
A64: len g - x >= 0 by A48,XREAL_1:48;
i < len g - x + (y+1) - 1 by A10,A50,A55,Th2;
then
A65: i < len g -' x + (y+1) - 1 by A64,XREAL_0:def 2;
then i+1 <= len g -' x + y by NAT_1:13;
then i+1 <= len g - x + y + 1 - 1 by A64,XREAL_0:def 2;
then
A66: i+1 <= len g - x + (y+1) - 1;
i < len g -' x + y + 1 - 1 by A65;
then i < len g - x + y by A64,XREAL_0:def 2;
then i - y < len g - x + y - y by XREAL_1:9;
then i - y + x < len g - x + x by XREAL_1:8;
then x - y - 1 + i + 1 < len g;
then
A67: x -'(y+1) + i + 1 < len g by A52,XREAL_0:def 2;
i <= i+1 by NAT_1:11;
then y+1 <= i+1 by A63,XXREAL_0:2;
then
A68: d.(i+1) = g.(x -'(y+1) + (i+1) + 1) by A10,A51,A50,A66,Th6
.= g.(x -'(y+1) + i + 1 + 1);
i <= len g - x + (y+1) - 1 by A10,A50,A55,Th2;
then d.i = g.(x -'(y+1) + i + 1) by A10,A51,A50,A63,Th6;
hence thesis by A9,A68,A67,NAT_1:11;
end;
end;
A69: Y() = d.(len d)
proof
per cases;
suppose
A70: len d <= y;
now
assume len d = 0;
then y+1 = 0+1 by A10,A50,Th3;
hence contradiction by A11,FINSEQ_3:24;
end;
then
A71: 0+1 <= len d by NAT_1:13;
len d <= (y+1)-1 by A70;
then
A72: d.len d = g.len d by A50,A71,Th4;
len g - x + (y+1) - 1 <= y by A10,A50,A70,Th2;
then len g - x + y + 1 - 1 <= y;
then len g - x <= 0 by XREAL_1:29;
then len g <= x by XREAL_1:50;
then
A73: len g = x by A48,XXREAL_0:1;
then y <= len g - x + (y+1) - 1;
hence thesis by A7,A10,A12,A50,A73,A72,Th2;
end;
suppose
len d > y;
then
A74: y+1 <= len d by NAT_1:13;
len d = len g - x + (y+1) - 1 by A10,A50,Th2;
hence d.len d = g.(x -'(y+1) + (len g - x + (y+1) - 1) + 1) by A10
,A51,A50,A74,Th6
.= g.(x - (y+1) + ((y+1) + ((len g - x) - 1)) + 1) by A51,
XREAL_1:233
.= Y() by A7;
end;
end;
1 <= (y+1)-1 by A11,FINSEQ_3:25;
then
A75: X() = d.1 by A6,A50,Th4;
0 < --(x - y) by A45,XREAL_1:50;
then -(x - y) < 0;
then len g + - (x - y) < len g + 0 by XREAL_1:8;
then len g - x + (y+1) - 1 < len g;
then len d < len g by A10,A50,Th2;
hence contradiction by A4,A5,A75,A69,A53;
end;
end;
hence thesis by A6,A7,A8,A9;
end;
begin :: Segre cosets
theorem Th7:
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
let I be non empty set;
let A be 1-sorted-yielding ManySortedSet of I;
let L be ManySortedSubset of Carrier A;
let i be Element of I;
let S be Subset of A.i;
A1: L c= Carrier A by PBOOLE:def 18;
A2: dom L = I by PARTFUN1:def 2;
L+*(i,S) c= Carrier A
proof
let a be object;
assume a in I;
then reconsider b=a as Element of I;
per cases;
suppose
A3: a = i;
then L+*(i,S).b = S by A2,FUNCT_7:31;
then L+*(i,S).b c= the carrier of A.b by A3;
hence thesis by YELLOW_6:2;
end;
suppose
a <> i;
then L+*(i,S).a = L.b by FUNCT_7:32;
hence thesis by A1;
end;
end;
hence thesis by PBOOLE:def 18;
end;
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
:Def2:
ex L being
Segre-like non trivial-yielding ManySortedSubset of Carrier A st it = product L
& L.indx(L) = [#](A.indx(L));
existence
proof
set L = the Segre-like non trivial-yielding ManySortedSubset of Carrier A;
reconsider C=L+*(indx(L),[#](A.indx(L))) as ManySortedSubset of Carrier A
by Th7;
A1: dom Carrier A = I by PARTFUN1:def 2;
dom A = I by PARTFUN1:def 2;
then A.indx(L) in rng A by FUNCT_1:3;
then
A2: A.indx(L) is non trivial by PENCIL_1:def 17;
then reconsider C as Segre-like non trivial-yielding ManySortedSubset of
Carrier A by PENCIL_1:27;
C c= Carrier A by PBOOLE:def 18;
then
A3: for a being object st a in I holds C.a c= (Carrier A).a;
dom C = I by PARTFUN1:def 2;
then reconsider P = product C as Subset of Segre_Product A by A1,A3,
CARD_3:27;
take P;
dom L = I by PARTFUN1:def 2;
then
A4: C.indx(L) = [#](A.indx(L)) by FUNCT_7:31;
then indx(C) = indx(L) by A2,PENCIL_1:def 21;
hence thesis by A4;
end;
end;
theorem Th8:
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
proof
let I be non empty set;
let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I;
let B1,B2 be Segre-Coset of A;
consider L1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A1: B1 = product L1 and
A2: L1.indx(L1) = [#](A.indx(L1)) by Def2;
consider L2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A3: B2 = product L2 and
A4: L2.indx(L2) = [#](A.indx(L2)) by Def2;
assume
A5: 2 c= card(B1 /\ B2);
then
A6: indx L1 = indx L2 by A1,A3,PENCIL_1:26;
A7: now
let i be object;
assume i in I;
per cases;
suppose
i <> indx L1;
hence L1.i = L2.i by A5,A1,A3,PENCIL_1:26;
end;
suppose
i = indx(L1);
hence L1.i = L2.i by A2,A4,A6;
end;
end;
A8: dom L2 = I by PARTFUN1:def 2;
dom L1 = I by PARTFUN1:def 2;
hence thesis by A1,A3,A8,A7,FUNCT_1:2;
end;
definition
let S be TopStruct;
let X,Y be Subset of S;
pred X,Y are_joinable means
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
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))))
proof
defpred P[set,set] means 2 c= card($1 /\ $2);
let S be TopStruct;
let X,Y be Subset of S;
assume X,Y are_joinable;
then consider f being FinSequence of bool the carrier of S such that
A1: X = f.1 & Y = f.(len f) and
A2: for W being Subset of S st W in rng f holds W is closed_under_lines
strong and
A3: for i being Element of NAT st 1 <= i & i < len f holds 2 c= card((f.
i) /\ (f.(i+1)));
A4: 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] by A3;
consider g being one-to-one FinSequence of bool the carrier of S such that
A5: X = g.1 & Y = g.(len g) and
A6: rng g c= rng f and
A7: for i being Element of NAT st 1 <= i & i < len g holds P[g.i,g.(i+1)
] from FinSeqOneToOne(A1,A4);
take g;
thus thesis by A2,A5,A6,A7;
end;
theorem Th10:
for S being TopStruct for X being Subset of S st X is
closed_under_lines strong holds X,X are_joinable
proof
let S be TopStruct;
let X be Subset of S;
assume
A1: X is closed_under_lines strong;
reconsider f = <*X*> as FinSequence of bool the carrier of S;
take f;
thus X = f.1;
len f = 1 by FINSEQ_1:40;
hence X = f.(len f);
thus for W being Subset of S st W in rng f holds W is closed_under_lines
strong
proof
let W be Subset of S;
assume W in rng f;
then W in {X} by FINSEQ_1:38;
hence thesis by A1,TARSKI:def 1;
end;
let i be Element of NAT;
assume that
A2: 1 <= i and
A3: i < len f;
thus thesis by A2,A3,FINSEQ_1:40;
end;
theorem Th11:
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
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let X,Y be Subset of Segre_Product A;
assume that
A1: X is non trivial closed_under_lines strong and
A2: Y is non trivial closed_under_lines strong and
A3: X,Y are_joinable;
set B=bool the carrier of Segre_Product A;
consider f being FinSequence of B such that
A4: X = f.1 and
A5: Y = f.(len f) and
A6: for W being Subset of Segre_Product A st W in rng f holds W is
closed_under_lines strong and
A7: for i being Element of NAT st 1 <= i & i < len f holds 2 c= card((f
. i) /\ (f.(i+1))) by A3;
len f in dom f by A2,A5,FUNCT_1:def 2;
then
A8: 1 <= len f by FINSEQ_3:25;
consider B0 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A9: X = product B0 and
for C being Subset of A.indx(B0) st C=B0.indx(B0) holds C is strong
closed_under_lines by A1,PENCIL_1:29;
let X1,Y1 be Segre-like non trivial-yielding ManySortedSubset of Carrier A
such that
A10: X = product X1 and
A11: Y = product Y1;
defpred P[Element of NAT] means for H being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st f.$1 = product H holds indx(X1) = indx(H) &
for i being object st i <> indx(X1) holds X1.i = H.i;
A12: B0=X1 by A10,A9,PUA2MSS1:2;
A13: for j being Element of NAT st 1 <= j & j < len f holds P[j] implies P[j
+1]
proof
let j be Element of NAT;
assume that
A14: 1 <= j and
A15: j < len f;
j in dom f by A14,A15,FINSEQ_3:25;
then
A16: f.j in rng f by FUNCT_1:3;
A17: 1 <= j+1 by NAT_1:11;
j+1 <= len f by A15,NAT_1:13;
then j+1 in dom f by A17,FINSEQ_3:25;
then f.(j+1) in rng f by FUNCT_1:3;
then reconsider
fj = f.j, fj1 = f.(j+1) as Subset of Segre_Product A by A16;
A18: card (fj /\ fj1) c= card fj by CARD_1:11,XBOOLE_1:17;
A19: 2 c= card (fj /\ fj1) by A7,A14,A15;
then 2 c= card fj by A18;
then fj is non trivial closed_under_lines strong by A6,A16,PENCIL_1:4;
then consider B1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A20: fj = product B1 and
for C being Subset of A.indx(B1) st C=B1.indx(B1) holds C is strong
closed_under_lines by PENCIL_1:29;
assume
A21: P[j];
then
A22: indx(B0) = indx(B1) by A12,A20;
now
let H be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
assume
A23: f.(j+1) = product H;
hence indx(X1) = indx(H) by A12,A20,A22,A19,PENCIL_1:26;
thus for i being object st i <> indx(X1) holds X1.i = H.i
proof
let i be object;
assume
A24: i <> indx(X1);
then
A25: i <> indx(B1) by A21,A20;
thus X1.i = B1.i by A21,A20,A24
.= H.i by A20,A19,A23,A25,PENCIL_1:26;
end;
end;
hence thesis;
end;
A26: P[1] by A10,A4,PUA2MSS1:2;
for i being Element of NAT st 1 <= i & i <= len f holds P[i] from
INT_1:sch 7(A26,A13);
hence thesis by A11,A5,A8;
end;
begin :: Collineations of Segre product
theorem
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
let S be 1-sorted;
let T be non empty 1-sorted;
let f be Function of S,T;
assume
A1: f is bijective;
then
A2: rng f = [#]T by FUNCT_2:def 3;
then rng (f") = [#]S by A1,TOPS_2:49;
then
A3: f" is onto by FUNCT_2:def 3;
f" is one-to-one by A1,A2,TOPS_2:50;
hence thesis by A3;
end;
definition
let S,T be TopStruct;
let f be Function of S,T;
attr f is isomorphic means
:Def4:
f is bijective open & f" is bijective open;
end;
registration
let S be non empty TopStruct;
cluster isomorphic for Function of S,S;
existence
proof
take f = id S;
f" = id S by TOPGRP_1:2;
hence f is isomorphic;
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;
redefine func f.:l -> Block of S; :: redefines .: (FUNCT_1, redefinition) → .: (RELAT_1, definition)
coherence
proof
l in the topology of S;
then reconsider L=l as Subset of S;
A1: L is open by PRE_TOPC:def 2;
f is open by Def4;
then f.:L is open by A1,T_0TOPSP:def 2;
hence thesis by PRE_TOPC:def 2;
end;
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; :: redefines " (FUNCT_1, redefinition) → " (RELAT_1, definition)
coherence
proof
l in the topology of S;
then reconsider L=l as Subset of S;
A1: L is open by PRE_TOPC:def 2;
A2: f is bijective by Def4;
f" = (f qua Function)" by A2,TOPS_2:def 4;
then
A3: (f").:L = f"L by A2,FUNCT_1:85;
f" is open by Def4;
then (f").:L is open by A1,T_0TOPSP:def 2;
hence thesis by A3,PRE_TOPC:def 2;
end;
end;
theorem Th13:
for S being non empty TopStruct for f being Collineation of S
holds f" is Collineation of S
proof
let S be non empty TopStruct;
let f be Collineation of S;
A1: f" is bijective open by Def4;
A2: f is bijective by Def4;
then
A3: rng f = [#]S by FUNCT_2:def 3;
then f"" = f by A2,TOPS_2:51;
then
A4: f"" is open by Def4;
f"" is bijective by A2,A3,TOPS_2:51;
hence thesis by A1,A4,Def4;
end;
theorem Th14:
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
proof
let S be non empty TopStruct;
let f be Collineation of S;
let X be Subset of S;
assume X is non trivial;
then 2 c= card X by PENCIL_1:4;
then consider x,y being object such that
A1: x in X and
A2: y in X and
A3: x<>y by PENCIL_1:2;
A4: dom f = the carrier of S by FUNCT_2:def 1;
then
A5: f.x in f.:X by A1,FUNCT_1:def 6;
A6: f.y in f.:X by A4,A2,FUNCT_1:def 6;
f is bijective by Def4;
then f.x <> f.y by A4,A1,A2,A3,FUNCT_1:def 4;
then 2 c= card(f.:X) by A5,A6,PENCIL_1:2;
hence thesis by PENCIL_1:4;
end;
theorem
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
proof
let S be non empty TopStruct;
let f be Collineation of S;
let X be Subset of S;
assume X is non trivial;
then 2 c= card X by PENCIL_1:4;
then consider x,y being object such that
A1: x in X and
A2: y in X and
A3: x<>y by PENCIL_1:2;
f is bijective by Def4;
then
A4: rng f = the carrier of S by FUNCT_2:def 3;
then consider fx being object such that
A5: fx in dom f and
A6: f.fx = x by A1,FUNCT_1:def 3;
consider fy being object such that
A7: fy in dom f and
A8: f.fy = y by A4,A2,FUNCT_1:def 3;
A9: fy in f"X by A2,A7,A8,FUNCT_1:def 7;
fx in f"X by A1,A5,A6,FUNCT_1:def 7;
then 2 c= card(f"X) by A3,A6,A8,A9,PENCIL_1:2;
hence thesis by PENCIL_1:4;
end;
theorem Th16:
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
let S be non empty non void TopStruct;
let f be Collineation of S;
let X be Subset of S;
assume
A1: X is strong;
thus f.:X is strong
proof
let a,b be Point of S;
assume that
A2: a in f.:X and
A3: b in f.:X;
thus a,b are_collinear
proof
per cases;
suppose
a=b;
hence thesis;
end;
suppose
A4: a<>b;
consider B being object such that
A5: B in dom f and
A6: B in X and
A7: b = f.B by A3,FUNCT_1:def 6;
consider A being object such that
A8: A in dom f and
A9: A in X and
A10: a = f.A by A2,FUNCT_1:def 6;
reconsider A,B as Point of S by A8,A5;
A,B are_collinear by A1,A9,A6;
then consider l being Block of S such that
A11: {A,B} c= l by A4,A10,A7;
B in l by A11,ZFMISC_1:32;
then
A12: b in f.:l by A5,A7,FUNCT_1:def 6;
A in l by A11,ZFMISC_1:32;
then a in f.:l by A8,A10,FUNCT_1:def 6;
then {a,b} c= f.:l by A12,ZFMISC_1:32;
hence thesis;
end;
end;
end;
end;
theorem
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
let S be non empty non void TopStruct;
let f be Collineation of S;
reconsider g=f" as Collineation of S by Th13;
let X be Subset of S;
assume X is strong;
then
A1: g.:X is strong by Th16;
A2: f is bijective by Def4;
then rng f = [#]S by FUNCT_2:def 3;
hence thesis by A2,A1,TOPS_2:55;
end;
theorem Th18:
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
let S be non empty non void TopStruct;
let f be Collineation of S;
let X be Subset of S;
assume
A1: X is closed_under_lines;
thus f.:X is closed_under_lines
proof
let l be Block of S;
assume 2 c= card(l /\ (f.:X));
then consider a,b being object such that
A2: a in l /\ (f.:X) and
A3: b in l /\ (f.:X) and
A4: a<>b by PENCIL_1:2;
b in f.:X by A3,XBOOLE_0:def 4;
then consider B being object such that
A5: B in dom f and
A6: B in X and
A7: b=f.B by FUNCT_1:def 6;
b in l by A3,XBOOLE_0:def 4;
then B in (f"l) by A5,A7,FUNCT_1:def 7;
then
A8: B in (f"l) /\ X by A6,XBOOLE_0:def 4;
a in f.:X by A2,XBOOLE_0:def 4;
then consider A being object such that
A9: A in dom f and
A10: A in X and
A11: a=f.A by FUNCT_1:def 6;
a in l by A2,XBOOLE_0:def 4;
then A in (f"l) by A9,A11,FUNCT_1:def 7;
then A in (f"l) /\ X by A10,XBOOLE_0:def 4;
then 2 c= card ((f"l) /\ X) by A4,A11,A7,A8,PENCIL_1:2;
then f"l c= X by A1;
then
A12: f.:(f"l) c= f.:X by RELAT_1:123;
f is bijective by Def4;
then
A13: rng f = the carrier of S by FUNCT_2:def 3;
l in the topology of S;
hence thesis by A13,A12,FUNCT_1:77;
end;
end;
theorem
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
let S be non empty non void TopStruct;
let f be Collineation of S;
reconsider g=f" as Collineation of S by Th13;
let X be Subset of S;
assume X is closed_under_lines;
then
A1: g.:X is closed_under_lines by Th18;
A2: f is bijective by Def4;
then rng f = [#]S by FUNCT_2:def 3;
hence thesis by A2,A1,TOPS_2:55;
end;
theorem Th20:
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
proof
let S be non empty non void TopStruct;
let f be Collineation of S;
let X,Y be Subset of S;
assume that
A1: X is non trivial and
A2: Y is non trivial and
A3: X,Y are_joinable;
consider g being FinSequence of bool the carrier of S such that
A4: X = g.1 and
A5: Y = g.(len g) and
A6: for W being Subset of S st W in rng g holds W is closed_under_lines
strong and
A7: for i being Element of NAT st 1 <= i & i < len g holds 2 c= card((g.
i) /\ (g.(i+1))) by A3;
deffunc F(set) = f.:(g.$1);
consider p being FinSequence such that
A8: len p = len g & for k being Nat st k in dom p holds p.k=F(k) from
FINSEQ_1:sch 2;
A9: dom g = Seg len g by FINSEQ_1:def 3;
A10: dom p = Seg len p by FINSEQ_1:def 3;
rng p c= bool the carrier of S
proof
let o be object;
assume o in rng p;
then consider i being object such that
A11: i in dom p and
A12: o=p.i by FUNCT_1:def 3;
reconsider i as Element of NAT by A11;
g.i in rng g by A8,A10,A9,A11,FUNCT_1:3;
then reconsider gi = g.i as Subset of S;
p.i = f.:(gi) by A8,A11;
hence thesis by A12;
end;
then reconsider p as FinSequence of bool the carrier of S by FINSEQ_1:def 4;
take p;
1 in dom g by A1,A4,FUNCT_1:def 2;
hence f.:X = p.1 by A4,A8,A10,A9;
len g in dom g by A2,A5,FUNCT_1:def 2;
hence f.:Y = p.(len p) by A5,A8,A10,A9;
thus for W being Subset of S st W in rng p holds W is closed_under_lines
strong
proof
let W be Subset of S;
assume W in rng p;
then consider i being object such that
A13: i in dom p and
A14: W=p.i by FUNCT_1:def 3;
reconsider i as Element of NAT by A13;
g.i in rng g by A8,A10,A9,A13,FUNCT_1:3;
then reconsider gi = g.i as Subset of S;
gi in rng g by A8,A10,A9,A13,FUNCT_1:3;
then
A15: gi is strong closed_under_lines by A6;
p.i = f.:(gi) by A8,A13;
hence thesis by A14,A15,Th16,Th18;
end;
A16: f is bijective by Def4;
thus for i being Element of NAT st 1 <= i & i < len p holds 2 c= card((p.i)
/\ (p.(i+1)))
proof
let i be Element of NAT;
assume that
A17: 1 <= i and
A18: i < len p;
A19: (g.i) /\ (g.(i+1)) c= g.i by XBOOLE_1:17;
i in dom g by A8,A17,A18,FINSEQ_3:25;
then g.i in rng g by FUNCT_1:3;
then reconsider gg=(g.i) /\ g.(i+1) as Subset of S by A19,XBOOLE_1:1;
2 c= card((g.i) /\ (g.(i+1))) by A7,A8,A17,A18;
then gg is non trivial by PENCIL_1:4;
then f.:gg is non trivial by Th14;
then
A20: f.:(g.i) /\ f.:(g.(i+1)) is non trivial by A16,FUNCT_1:62;
A21: i+1 <= len p by A18,NAT_1:13;
1 <= i+1 by A17,NAT_1:13;
then i+1 in dom p by A21,FINSEQ_3:25;
then
A22: p.(i+1) = f.:(g.(i+1)) by A8;
i in dom g by A8,A17,A18,FINSEQ_3:25;
then p.i = f.:(g.i) by A8,A10,A9;
hence thesis by A22,A20,PENCIL_1:4;
end;
end;
theorem
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
proof
let S be non empty non void TopStruct;
let f be Collineation of S;
let X,Y be Subset of S;
reconsider g=f" as Collineation of S by Th13;
assume that
A1: X is non trivial and
A2: Y is non trivial and
A3: X,Y are_joinable;
A4: f is bijective by Def4;
then
A5: rng f = [#]S by FUNCT_2:def 3;
then
A6: f"Y = g.:Y by A4,TOPS_2:55;
f"X = g.:X by A4,A5,TOPS_2:55;
hence thesis by A6,A1,A2,A3,Th20;
end;
theorem Th22:
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
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds A.i is strongly_connected;
let W be Subset of Segre_Product A such that
A2: W is non trivial strong closed_under_lines;
consider K being Segre-like non trivial-yielding ManySortedSubset of Carrier
A such that
A3: W = product K and
A4: for S being Subset of A.indx(K) st S=K.indx(K) holds S is strong
closed_under_lines by A2,PENCIL_1:29;
set O = [#](A.indx(K));
set B = union {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & W,Y are_joinable};
B c= the carrier of Segre_Product A
proof
let a be object;
assume a in B;
then consider y being set such that
A5: a in y and
A6: y in {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & W,Y are_joinable} by TARSKI:def 4;
ex Y being Subset of Segre_Product A st y=Y & Y is non trivial
strong closed_under_lines & W,Y are_joinable by A6;
hence thesis by A5;
end;
then reconsider C = B as Subset of Segre_Product A;
dom A = I by PARTFUN1:def 2;
then A.indx(K) in rng A by FUNCT_1:3;
then
A7: A.indx(K) is non trivial by PENCIL_1:def 17;
then reconsider L = K+*(indx(K),O) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by Th7,PENCIL_1:27;
dom K = I by PARTFUN1:def 2;
then L.indx(K) = O by FUNCT_7:31;
then
A8: indx(K)=indx(L) by A7,PENCIL_1:def 21;
A9: product L c= C
proof
K c= Carrier A by PBOOLE:def 18;
then K.indx(K) c= (Carrier A).indx(K);
then reconsider S=K.indx(K) as Subset of A.indx(K) by YELLOW_6:2;
let y be object;
A10: dom K = I by PARTFUN1:def 2;
A11: A.indx(K) is strongly_connected by A1;
assume y in product L;
then consider z being Function such that
A12: z=y and
A13: dom z = dom L and
A14: for a being object st a in dom L holds z.a in L.a by CARD_3:def 5;
A15: dom L = I by PARTFUN1:def 2;
then reconsider z as ManySortedSet of I by A13,PARTFUN1:def 2
,RELAT_1:def 18;
z.indx(K) in L.indx(K) by A14,A15;
then reconsider zi = z.indx(K) as Point of A.indx(K) by A10,FUNCT_7:31;
S is non trivial strong closed_under_lines by A4,PENCIL_1:def 21;
then consider
f being FinSequence of bool the carrier of (A.indx(K)) such that
A16: S = f.1 and
A17: zi in f.(len f) and
A18: for Z being Subset of (A.indx(K)) st Z in rng f holds Z is
closed_under_lines strong and
A19: for i being Nat st 1 <= i & i < len f holds 2 c= card((f.i) /\ (f
.( i+1))) by A11;
A20: len f in dom f by A17,FUNCT_1:def 2;
then 1 in dom f by FINSEQ_5:6,RELAT_1:38;
then
A21: 1 in Seg len f by FINSEQ_1:def 3;
A22: f.len f is non trivial
proof
reconsider l1 = (len f) - 1 as Element of NAT by A20,FINSEQ_3:26;
A23: 1 <= len f by A20,FINSEQ_3:25;
per cases by A23,XXREAL_0:1;
suppose
len f = 1;
hence thesis by A16,PENCIL_1:def 21;
end;
suppose
len f > 1;
then 1+1 <= len f by NAT_1:13;
then
A24: 2-1 <= l1 by XREAL_1:9;
A25: card((f.l1) /\ (f.(l1+1))) c= card (f.(l1+1)) by CARD_1:11,XBOOLE_1:17;
l1 < len f - 0 by XREAL_1:15;
then 2 c= card((f.l1) /\ (f.(l1+1))) by A19,A24;
then 2 c= card (f.(l1+1)) by A25;
hence thesis by PENCIL_1:4;
end;
end;
then reconsider ff=f.len f as non trivial set;
L.indx(K) = O by A10,FUNCT_7:31;
then indx K = indx L by A7,PENCIL_1:def 21;
then reconsider EL=L+*(indx(K),ff) as Segre-like non trivial-yielding
ManySortedSet of I by PENCIL_1:27;
A26: dom z = dom (L+*(indx(K),f.(len f))) by A13,FUNCT_7:30;
deffunc F(set) = product (L+*(indx(K),f.$1));
consider g being FinSequence such that
A27: len g = len f & for k being Nat st k in dom g holds g.k = F(k)
from FINSEQ_1:sch 2;
A28: rng g c= bool the carrier of Segre_Product A
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
A29: dom Carrier A = I by PARTFUN1:def 2;
assume a in rng g;
then consider k being object such that
A30: k in dom g and
A31: a=g.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A30;
A32: k in Seg (len f) by A27,A30,FINSEQ_1:def 3;
A33: now
let o be object;
assume
A34: o in I;
A35: k in dom f by A32,FINSEQ_1:def 3;
per cases;
suppose
A36: o <> indx(K);
then L+*(indx(K),f.k).o = L.o by FUNCT_7:32;
then
A37: L+*(indx(K),f.k).o = K.o by A36,FUNCT_7:32;
K c= Carrier A by PBOOLE:def 18;
hence L+*(indx(K),f.k).o c= (Carrier A).o by A34,A37;
end;
suppose
A38: o = indx(K);
then L+*(indx(K),f.k).o = f.k by A15,FUNCT_7:31;
then L+*(indx(K),f.k).o in rng f by A35,FUNCT_1:3;
then L+*(indx(K),f.k).o c= the carrier of (A.indx(K));
hence L+*(indx(K),f.k).o c= (Carrier A).o by A38,YELLOW_6:2;
end;
end;
dom (L+*(indx(K),f.k)) = I by PARTFUN1:def 2;
then product (L+*(indx(K),f.k)) c= product Carrier A by A29,A33,CARD_3:27
;
then aa c= product Carrier A by A27,A30,A31;
hence thesis;
end;
A39: dom g = Seg len f by A27,FINSEQ_1:def 3;
reconsider g as FinSequence of bool the carrier of Segre_Product A by A28,
FINSEQ_1:def 4;
len f in dom g by A20,A27,FINSEQ_3:29;
then
A40: g.(len f) in rng g by FUNCT_1:3;
then reconsider Yb = g.(len f) as Subset of Segre_Product A;
A41: now
let o be object;
assume o in I;
per cases;
suppose
A42: o <> indx(K);
then L+*(indx(K),f.1).o = L.o by FUNCT_7:32;
hence L+*(indx(K),f.1).o = K.o by A42,FUNCT_7:32;
end;
suppose
o = indx(K);
hence L+*(indx(K),f.1).o = K.o by A15,A16,FUNCT_7:31;
end;
end;
A43: for V being Subset of Segre_Product A st V in rng g holds V is
closed_under_lines strong
proof
let V be Subset of Segre_Product A;
assume V in rng g;
then consider n1 being object such that
A44: n1 in dom g and
A45: V=g.n1 by FUNCT_1:def 3;
reconsider n=n1 as Element of NAT by A44;
n in Seg len f by A27,A44,FINSEQ_1:def 3;
then
A46: n in dom f by FINSEQ_1:def 3;
f.n is non trivial
proof
A47: n <= len f by A46,FINSEQ_3:25;
per cases by A46,A47,FINSEQ_3:25,XXREAL_0:1;
suppose
1<=n & n=len f;
hence thesis by A22;
end;
suppose
A48: 1 <= n & n < len f;
A49: card((f.n) /\ (f.(n+1))) c= card (f.n) by CARD_1:11,XBOOLE_1:17;
2 c= card((f.n) /\ (f.(n+1))) by A19,A48;
then 2 c= card (f.n) by A49;
hence thesis by PENCIL_1:4;
end;
end;
then reconsider fn=f.n as non trivial set;
A50: L+*(indx(K),f.n) c= Carrier A
proof
let o be object;
assume
A51: o in I;
per cases;
suppose
A52: o <> indx(K);
A53: L c= Carrier A by PBOOLE:def 18;
L+*(indx(K),f.n).o = L.o by A52,FUNCT_7:32;
hence thesis by A51,A53;
end;
suppose
A54: o=indx(K);
then L+*(indx(K),f.n).o = f.n by A15,FUNCT_7:31;
then L+*(indx(K),f.n).o in rng f by A46,FUNCT_1:3;
then L+*(indx(K),f.n).o c= the carrier of (A.indx(K));
hence thesis by A54,YELLOW_6:2;
end;
end;
L.indx(K) = O by A10,FUNCT_7:31;
then indx K = indx L by A7,PENCIL_1:def 21;
then reconsider LI = L+*(indx(K),fn) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by A50,PBOOLE:def 18,PENCIL_1:27;
reconsider LI as Segre-like non trivial-yielding ManySortedSubset of
Carrier A;
A55: LI.indx(K) = fn by A15,FUNCT_7:31;
then
A56: indx(LI) = indx(K) by PENCIL_1:def 21;
A57: now
let D be Subset of A.indx(LI);
assume D=LI.indx(LI);
then D in rng f by A46,A55,A56,FUNCT_1:3;
hence D is strong closed_under_lines by A18,A56;
end;
g.n = product (L+*(indx(K),f.n)) by A27,A44;
hence thesis by A45,A57,PENCIL_1:29;
end;
A58: len f in Seg len f by A20,FINSEQ_1:def 3;
then Yb = product EL by A27,A39;
then
A59: Yb is non trivial strong closed_under_lines by A40,A43;
A60: for i being Element of NAT st 1 <= i & i < len g holds 2 c= card((g.
i) /\ (g.(i+1)))
proof
consider l1 being object such that
A61: l1 in product L by XBOOLE_0:def 1;
let i be Element of NAT;
assume that
A62: 1 <= i and
A63: i < len g;
i in Seg (len f) by A27,A62,A63,FINSEQ_1:1;
then
A64: g.i = product (L+*(indx(K),f.i)) by A27,A39;
2 c= card ((f.i) /\ (f.(i+1))) by A19,A27,A62,A63;
then consider a,b being object such that
A65: a in (f.i) /\ (f.(i+1)) and
A66: b in (f.i) /\ (f.(i+1)) and
A67: a <> b by PENCIL_1:2;
consider l being Function such that
l = l1 and
A68: dom l = dom L and
A69: for o being object st o in dom L holds l.o in L.o by A61,CARD_3:def 5;
reconsider l as ManySortedSet of I by A15,A68,PARTFUN1:def 2
,RELAT_1:def 18;
set l1=l+*(indx(K),a),l2=l+*(indx(K),b);
A70: i+1 <= len g by A63,NAT_1:13;
A71: now
let o be object;
assume o in dom (L+*(indx(K),f.i));
then
A72: o in I;
then
A73: o in dom l by PARTFUN1:def 2;
per cases;
suppose
A74: o = indx(K);
then l1.o = a by A73,FUNCT_7:31;
then l1.o in f.i by A65,XBOOLE_0:def 4;
hence l1.o in L+*(indx(K),f.i).o by A15,A74,FUNCT_7:31;
end;
suppose
A75: o <> indx(K);
then
A76: l1.o = l.o by FUNCT_7:32;
l.o in L.o by A15,A69,A72;
hence l1.o in L+*(indx(K),f.i).o by A75,A76,FUNCT_7:32;
end;
end;
1 <= i+1 by A62,NAT_1:13;
then i+1 in Seg (len f) by A27,A70,FINSEQ_1:1;
then
A77: g.(i+1) = product (L+*(indx(K),f.(i+1))) by A27,A39;
A78: now
let o be object;
assume o in dom (L+*(indx(K),f.i));
then
A79: o in I;
then
A80: o in dom l by PARTFUN1:def 2;
per cases;
suppose
A81: o = indx(K);
then l2.o = b by A80,FUNCT_7:31;
then l2.o in f.i by A66,XBOOLE_0:def 4;
hence l2.o in L+*(indx(K),f.i).o by A15,A81,FUNCT_7:31;
end;
suppose
A82: o <> indx(K);
then
A83: l2.o = l.o by FUNCT_7:32;
l.o in L.o by A15,A69,A79;
hence l2.o in L+*(indx(K),f.i).o by A82,A83,FUNCT_7:32;
end;
end;
A84: now
let o be object;
assume o in dom (L+*(indx(K),f.(i+1)));
then
A85: o in I;
then
A86: o in dom l by PARTFUN1:def 2;
per cases;
suppose
A87: o = indx(K);
then l1.o = a by A86,FUNCT_7:31;
then l1.o in f.(i+1) by A65,XBOOLE_0:def 4;
hence l1.o in L+*(indx(K),f.(i+1)).o by A15,A87,FUNCT_7:31;
end;
suppose
A88: o <> indx(K);
then
A89: l1.o = l.o by FUNCT_7:32;
l.o in L.o by A15,A69,A85;
hence l1.o in L+*(indx(K),f.(i+1)).o by A88,A89,FUNCT_7:32;
end;
end;
dom l1 = I by PARTFUN1:def 2
.= dom(L+*(indx(K),f.(i+1))) by PARTFUN1:def 2;
then
A90: l1 in product (L+*(indx(K),f.(i+1))) by A84,CARD_3:9;
A91: now
let o be object;
assume o in dom (L+*(indx(K),f.(i+1)));
then
A92: o in I;
then
A93: o in dom l by PARTFUN1:def 2;
per cases;
suppose
A94: o = indx(K);
then l2.o = b by A93,FUNCT_7:31;
then l2.o in f.(i+1) by A66,XBOOLE_0:def 4;
hence l2.o in L+*(indx(K),f.(i+1)).o by A15,A94,FUNCT_7:31;
end;
suppose
A95: o <> indx(K);
then
A96: l2.o = l.o by FUNCT_7:32;
l.o in L.o by A15,A69,A92;
hence l2.o in L+*(indx(K),f.(i+1)).o by A95,A96,FUNCT_7:32;
end;
end;
dom l2 = I by PARTFUN1:def 2
.= dom(L+*(indx(K),f.(i+1))) by PARTFUN1:def 2;
then
A97: l2 in product (L+*(indx(K),f.(i+1))) by A91,CARD_3:9;
dom l2 = I by PARTFUN1:def 2
.= dom(L+*(indx(K),f.i)) by PARTFUN1:def 2;
then l2 in product (L+*(indx(K),f.i)) by A78,CARD_3:9;
then
A98: l2 in (g.i) /\ (g.(i+1)) by A64,A77,A97,XBOOLE_0:def 4;
l1.indx(K) = a by A15,A68,FUNCT_7:31;
then
A99: l1 <> l2 by A15,A67,A68,FUNCT_7:31;
dom l1 = I by PARTFUN1:def 2
.= dom(L+*(indx(K),f.i)) by PARTFUN1:def 2;
then l1 in product (L+*(indx(K),f.i)) by A71,CARD_3:9;
then l1 in (g.i) /\ (g.(i+1)) by A64,A77,A90,XBOOLE_0:def 4;
hence thesis by A99,A98,PENCIL_1:2;
end;
A100: now
let o be object;
assume o in dom (L+*(indx(K),f.(len f)));
then
A101: o in I;
per cases;
suppose
o = indx(K);
hence z.o in (L+*(indx(K),f.(len f))).o by A15,A17,FUNCT_7:31;
end;
suppose
A102: o <> indx(K);
z.o in L.o by A14,A15,A101;
hence z.o in (L+*(indx(K),f.(len f))).o by A102,FUNCT_7:32;
end;
end;
L+*(indx(K),f.1) = K by A41;
then W = g.1 by A3,A27,A39,A21;
then W,Yb are_joinable by A27,A43,A60;
then
A103: Yb in {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & W,Y are_joinable} by A59;
Yb = product (L+*(indx(K),f.(len f))) by A27,A39,A58;
then y in Yb by A12,A26,A100,CARD_3:9;
hence thesis by A103,TARSKI:def 4;
end;
dom K = I by PARTFUN1:def 2;
then
A104: L.indx(L) = [#](A.indx(L)) by A8,FUNCT_7:31;
C c= product L
proof
let c be object;
assume c in C;
then consider y being set such that
A105: c in y and
A106: y in {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & W,Y are_joinable} by TARSKI:def 4;
consider Y being Subset of Segre_Product A such that
A107: y=Y and
A108: Y is non trivial strong closed_under_lines and
A109: W,Y are_joinable by A106;
reconsider c1 = c as ManySortedSet of I by A105,A107,PENCIL_1:14;
consider M being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A110: Y = product M and
for S being Subset of A.indx(M) st S=M.indx(M) holds S is strong
closed_under_lines by A108,PENCIL_1:29;
A111: dom M = I by PARTFUN1:def 2
.= dom L by PARTFUN1:def 2;
A112: dom K = I by PARTFUN1:def 2
.= dom L by PARTFUN1:def 2;
A113: for a being object st a in dom L holds c1.a in L.a
proof
let a be object;
assume
A114: a in dom L;
then reconsider a1=a as Element of I;
per cases;
suppose
A115: a = indx(K);
M c= Carrier A by PBOOLE:def 18;
then M.a1 c= (Carrier A).a1;
then
A116: M.a1 c= the carrier of (A.a1) by YELLOW_6:2;
c1.a in M.a by A105,A107,A110,A111,A114,CARD_3:9;
then c1.a in O by A115,A116;
hence thesis by A112,A114,A115,FUNCT_7:31;
end;
suppose
A117: a <> indx(K);
c1.a in M.a by A105,A107,A110,A111,A114,CARD_3:9;
then c1.a in K.a by A2,A3,A108,A109,A110,A117,Th11;
hence thesis by A117,FUNCT_7:32;
end;
end;
dom c1 = I by PARTFUN1:def 2
.= dom L by PARTFUN1:def 2;
hence thesis by A113,CARD_3:9;
end;
then C = product L by A9;
hence thesis by A104,Def2;
end;
theorem Th23:
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
}
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds A.i is strongly_connected;
let B be set;
thus B is Segre-Coset of A implies 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
}
proof
assume B is Segre-Coset of A;
then reconsider BB=B as Segre-Coset of A;
consider L being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A2: BB = product L and
A3: L.indx(L) = [#](A.indx(L)) by Def2;
set K1 = the Block of A.indx(L);
consider V being object such that
A4: V in product L by XBOOLE_0:def 1;
K1 in the topology of A.indx(L);
then reconsider K = K1 as Subset of A.indx(L);
A5: ex g being Function st g = V & dom g = dom L &
for i being object st i
in dom L holds g.i in L.i by A4,CARD_3:def 5;
A6: dom L = I by PARTFUN1:def 2;
then reconsider V as ManySortedSet of I by A5,PARTFUN1:def 2,RELAT_1:def 18
;
for i being object st i in I holds V.i is Element of (Carrier A).i
proof
let i be object;
assume
A7: i in I;
L c= Carrier A by PBOOLE:def 18;
then
A8: L.i c= (Carrier A).i by A7;
V.i in L.i by A6,A5,A7;
hence thesis by A8;
end;
then reconsider V as Element of Carrier A by PBOOLE:def 14;
reconsider VV={V} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider X=VV+*(indx(L),K) as ManySortedSubset of Carrier A by Th7;
2 c= card K by PENCIL_1:def 6;
then
A9: K is non trivial by PENCIL_1:4;
then reconsider X as Segre-like non trivial-yielding ManySortedSubset of
Carrier A by PENCIL_1:9,10;
dom VV = I by PARTFUN1:def 2;
then
A10: X.indx(L) = K by FUNCT_7:31;
then indx(X) = indx(L) by A9,PENCIL_1:def 21;
then reconsider pX = product X as Block of Segre_Product A by A10,
PENCIL_1:24;
A11: for i being object st i in I holds X.i c= L.i
proof
let i be object;
assume
A12: i in I;
per cases;
suppose
i <> indx L;
then X.i = VV.i by FUNCT_7:32;
then
A13: X.i = {V.i} by A12,PZFMISC1:def 1;
V.i in L.i by A6,A5,A12;
hence thesis by A13,ZFMISC_1:31;
end;
suppose
i = indx(L);
hence thesis by A3,A10;
end;
end;
pX in the topology of Segre_Product A;
then reconsider psX = pX as Subset of Segre_Product A;
take psX;
thus
A14: psX is non trivial strong closed_under_lines by PENCIL_1:20,21;
then reconsider
Z = union {Y where Y is Subset of Segre_Product A : Y is non
trivial strong closed_under_lines & psX,Y are_joinable} as Segre-Coset of A by
A1,Th22;
psX,psX are_joinable by A14,Th10;
then
A15: psX in {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & psX,Y are_joinable} by A14;
A16: psX c= Z
by A15,TARSKI:def 4;
dom X = I by PARTFUN1:def 2;
then psX c= B by A2,A6,A11,CARD_3:27;
then psX c= (B /\ Z) by A16,XBOOLE_1:19;
then
A17: card psX c= card (B /\ Z) by CARD_1:11;
2 c= card pX by PENCIL_1:def 6;
then BB=Z by A17,Th8,XBOOLE_1:1;
hence thesis;
end;
given W being Subset of Segre_Product A such that
A18: W is non trivial strong closed_under_lines and
A19: B = union {Y where Y is Subset of Segre_Product A : Y is non
trivial strong closed_under_lines & W,Y are_joinable};
thus thesis by A1,A18,A19,Th22;
end;
theorem Th24:
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
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds A.i is strongly_connected;
let B be Segre-Coset of A;
consider W being Subset of Segre_Product A such that
A2: W is non trivial strong closed_under_lines and
A3: B = union {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & W,Y are_joinable} by A1,Th23;
let f be Collineation of Segre_Product A;
reconsider g=f" as Collineation of Segre_Product A by Th13;
A4: dom f = the carrier of Segre_Product A by FUNCT_2:def 1;
A5: dom g = the carrier of Segre_Product A by FUNCT_2:def 1;
A6: f is bijective by Def4;
then
A7: rng f = the carrier of Segre_Product A by FUNCT_2:def 3;
A8: rng f = [#](Segre_Product A) by A6,FUNCT_2:def 3;
A9: f.:B = union {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & f.:W,Y are_joinable}
proof
A10: W c= f"(f.:W) by A4,FUNCT_1:76;
f"(f.:W) c= W by A6,FUNCT_1:82;
then
A11: f"(f.:W) = W by A10;
thus f.:B c= union {Y where Y is Subset of Segre_Product A: Y is non
trivial strong closed_under_lines & f.:W,Y are_joinable}
proof
let o be object;
assume o in f.:B;
then consider u being object such that
A12: u in dom f and
A13: u in B and
A14: o = f.u by FUNCT_1:def 6;
consider y being set such that
A15: u in y and
A16: y in {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & W,Y are_joinable} by A3,A13,TARSKI:def 4;
consider Y being Subset of Segre_Product A such that
A17: y=Y and
A18: Y is non trivial strong closed_under_lines and
A19: W,Y are_joinable by A16;
A20: f.:W,f.:Y are_joinable by A2,A18,A19,Th20;
f.:Y is non trivial strong closed_under_lines by A18,Th14,Th16,Th18;
then
A21: f.:Y in {Z where Z is Subset of Segre_Product A: Z is non trivial
strong closed_under_lines & f.:W,Z are_joinable} by A20;
o in f.:Y by A12,A14,A15,A17,FUNCT_1:def 6;
hence thesis by A21,TARSKI:def 4;
end;
let o be object;
assume o in union {Y where Y is Subset of Segre_Product A : Y is non
trivial strong closed_under_lines & f.:W,Y are_joinable};
then consider u being set such that
A22: o in u and
A23: u in {Y where Y is Subset of Segre_Product A : Y is non trivial
strong closed_under_lines & f.:W,Y are_joinable} by TARSKI:def 4;
consider Y being Subset of Segre_Product A such that
A24: u=Y and
A25: Y is non trivial strong closed_under_lines and
A26: f.: W,Y are_joinable by A23;
A27: g.:Y is non trivial strong closed_under_lines by A25,Th14,Th16,Th18;
f.:W is non trivial strong closed_under_lines by A2,Th14,Th16,Th18;
then g.:(f.:W),g.:Y are_joinable by A25,A26,Th20;
then W,g.:Y are_joinable by A6,A8,A11,TOPS_2:55;
then
A28: g.:Y in {Z where Z is Subset of Segre_Product A : Z is non trivial
strong closed_under_lines & W,Z are_joinable} by A27;
g.o in g.:Y by A5,A22,A24,FUNCT_1:def 6;
then
A29: g.o in B by A3,A28,TARSKI:def 4;
o = f.((f qua Function)".o) by A6,A7,A22,A24,FUNCT_1:35;
then o = f.(g.o) by A6,TOPS_2:def 4;
hence thesis by A4,A29,FUNCT_1:def 6;
end;
f.:W is non trivial strong closed_under_lines by A2,Th14,Th16,Th18;
hence thesis by A1,A9,Th23;
end;
theorem
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
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I such that
A1: for i being Element of I holds A.i is strongly_connected;
let B be Segre-Coset of A;
let f be Collineation of Segre_Product A;
reconsider g=f" as Collineation of Segre_Product A by Th13;
A2: f is bijective by Def4;
then rng f = [#](Segre_Product A) by FUNCT_2:def 3;
then f"B = g.:B by A2,TOPS_2:55;
hence thesis by A1,Th24;
end;