:: On the Characterization of Collineations of the Segre Product of Strongly
:: Connected Partial Linear Spaces
:: by Adam Naumowicz
::
:: Received October 18, 2004
:: Copyright (c) 2004-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, XBOOLE_0, STRUCT_0, PRE_TOPC, PENCIL_2, PENCIL_1,
FUNCT_1, RELAT_1, TARSKI, SUBSET_1, PRALG_1, PBOOLE, ZFMISC_1, RELAT_2,
FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, WAYBEL_3, RLVECT_2,
CARD_3, INTEGRA1, FUNCT_4, FINSET_1, FDIFF_1, PARSP_1, GRAPH_2, FUNCT_2,
CAT_1, RCOMP_1, FUNCOP_1, PENCIL_3, WAYBEL18;
notations TARSKI, XBOOLE_0, ZFMISC_1, XCMPLX_0, XXREAL_0, ORDINAL1, NUMBERS,
NAT_1, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1, CARD_1,
FINSET_1, FINSEQ_1, CARD_3, DOMAIN_1, STRUCT_0, PRE_TOPC, PBOOLE,
PZFMISC1, T_0TOPSP, PRALG_1, WAYBEL_3, WAYBEL18, PENCIL_1, FUNCT_7,
PENCIL_2, TOPS_2, FINSEQ_6, GRAPH_2;
constructors PZFMISC1, TOPS_2, REALSET2, T_0TOPSP, GRAPH_2, PENCIL_2,
RELSET_1, PBOOLE, FUNCT_7, PRE_POLY, FINSEQ_6;
registrations SUBSET_1, RELSET_1, FUNCT_2, XREAL_0, NAT_1, CARD_1, PBOOLE,
STRUCT_0, PENCIL_1, ORDINAL1, FUNCT_1, RELAT_1, FINSEQ_1, PRE_POLY,
WAYBEL18;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, PBOOLE, FUNCT_1, T_0TOPSP;
equalities XBOOLE_0, STRUCT_0, RELAT_1;
expansions TARSKI, XBOOLE_0, PBOOLE, FUNCT_1;
theorems XBOOLE_0, ZFMISC_1, FUNCT_1, FINSEQ_1, FINSEQ_3, NAT_1, CARD_3,
PBOOLE, PRE_TOPC, FUNCT_7, PRALG_1, PZFMISC1, TARSKI, FUNCT_2, TOPS_2,
PENCIL_1, PENCIL_2, CARD_1, XBOOLE_1, PUA2MSS1, FINSET_1, CARD_2,
GRAPH_2, FUNCOP_1, RELAT_1, RELSET_1, XREAL_1, XXREAL_0, ORDINAL1,
PARTFUN1, FINSEQ_6;
schemes TRANSGEO, NAT_1, FINSEQ_2, PENCIL_2, FINSEQ_1, PBOOLE, CLASSES1;
begin :: Preliminaries
theorem Th1:
for S being non empty non void TopStruct for f being Collineation
of S for p,q being Point of S st p,q are_collinear holds f.p,f.q are_collinear
proof
let S be non empty non void TopStruct;
let f be Collineation of S;
A1: dom f = the carrier of S by FUNCT_2:def 1;
let p,q be Point of S;
assume
A2: p,q are_collinear;
per cases;
suppose
p=q;
hence thesis by PENCIL_1:def 1;
end;
suppose
p<>q;
then consider B being Block of S such that
A3: {p,q} c= B by A2,PENCIL_1:def 1;
q in B by A3,ZFMISC_1:32;
then
A4: f.q in f.:B by A1,FUNCT_1:def 6;
p in B by A3,ZFMISC_1:32;
then f.p in f.:B by A1,FUNCT_1:def 6;
then {f.p,f.q} c= f.:B by A4,ZFMISC_1:32;
hence thesis by PENCIL_1:def 1;
end;
end;
theorem Th2:
for I being non empty set for i be Element of I for A being
non-Trivial-yielding 1-sorted-yielding ManySortedSet of I holds A.i is non
trivial
proof
let I be non empty set;
let i be Element of I;
let A be non-Trivial-yielding 1-sorted-yielding ManySortedSet of I;
dom A = I by PARTFUN1:def 2;
then A.i in rng A by FUNCT_1:3;
hence thesis by PENCIL_1:def 17;
end;
theorem Th3:
for S being non void identifying_close_blocks TopStruct st S is
strongly_connected holds S is without_isolated_points
proof
let S be non void identifying_close_blocks TopStruct;
assume
A1: S is strongly_connected;
now
consider X being object such that
A2: X in the topology of S by XBOOLE_0:def 1;
reconsider X as Block of S by A2;
reconsider X1=X as Subset of S by A2;
let x being Point of S;
X1 is closed_under_lines strong by PENCIL_1:20,21;
then consider f being FinSequence of bool the carrier of S such that
A3: X = f.1 and
A4: x in f.(len f) and
A5: for W being Subset of S st W in rng f holds W is
closed_under_lines strong and
A6: for i being Nat st 1 <= i & i < len f holds 2 c= card((f.i) /\ (f.
(i +1))) by A1,PENCIL_1:def 11;
A7: len f in dom f by A4,FUNCT_1:def 2;
then reconsider l=len f - 1 as Nat by FINSEQ_3:26;
A8: f.(len f) in rng f by A7,FUNCT_1:3;
then reconsider W=f.(len f) as Subset of S;
A9: W is closed_under_lines strong by A5,A8;
per cases;
suppose
x in X;
hence ex l being Block of S st x in l;
end;
suppose
A10: not x in X;
1 <= len f by A7,FINSEQ_3:25;
then 1 < len f -1 + 1 by A3,A4,A10,XXREAL_0:1;
then 1 <= l & l < len f by NAT_1:13;
then 2 c= card((f.l) /\ (f.(l+1))) by A6;
then consider a being object such that
A11: a in f.l /\ f.(len f) and
A12: a<>x by PENCIL_1:3;
A13: a in W by A11,XBOOLE_0:def 4;
then reconsider a as Point of S;
x,a are_collinear by A4,A9,A13,PENCIL_1:def 3;
then consider l being Block of S such that
A14: {x,a} c= l by A12,PENCIL_1:def 1;
x in l by A14,ZFMISC_1:32;
hence ex l being Block of S st x in l;
end;
end;
hence thesis by PENCIL_1:def 9;
end;
theorem Th4:
for S being non empty non void identifying_close_blocks TopStruct
holds S is strongly_connected implies S is connected
proof
let S being non empty non void identifying_close_blocks TopStruct;
assume
A1: S is strongly_connected;
then S is without_isolated_points by Th3;
hence thesis by A1,PENCIL_1:28;
end;
theorem
for S being non void non degenerated TopStruct for L being Block of S
ex x being Point of S st not x in L
proof
let S be non void non degenerated TopStruct;
let L be Block of S;
A1: L in the topology of S;
now
assume [#]S c= L;
then [#]S=L by A1;
hence contradiction by PENCIL_1:def 5;
end;
then consider x being object such that
A2: x in [#]S and
A3: not x in L;
reconsider x as Point of S by A2;
take x;
thus thesis by A3;
end;
theorem Th6:
for I being non empty set for A being non-Empty
TopStruct-yielding ManySortedSet of I for p being Point of Segre_Product A
holds p is Element of Carrier A
proof
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
let p be Point of Segre_Product A;
Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by
PENCIL_1:def 23;
then consider f being Function such that
A1: f=p and
A2: dom f = dom Carrier A and
A3: for x being object st x in dom Carrier A holds f.x in (Carrier A).x by
CARD_3:def 5;
A4: dom f = I by A2,PARTFUN1:def 2;
then reconsider f as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
for i being object st i in I holds f.i is Element of (Carrier A).i
by A2,A3,A4;
hence thesis by A1,PBOOLE:def 14;
end;
theorem Th7:
for I being non empty set for A be 1-sorted-yielding
ManySortedSet of I for x being Element of I holds (Carrier A).x = [#](A.x)
proof
let I be non empty set;
let A be 1-sorted-yielding ManySortedSet of I;
let x be Element of I;
ex R being 1-sorted st R=A.x & (Carrier A).x = the carrier of R by
PRALG_1:def 15;
hence thesis;
end;
theorem Th8:
for I being non empty set for i being Element of I for A be
non-Trivial-yielding TopStruct-yielding ManySortedSet of I ex L being
Segre-like non trivial-yielding ManySortedSubset of Carrier A st indx(L)=i &
product L is Segre-Coset of A
proof
let I being non empty set;
let x being Element of I;
let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I;
set p0 = the Point of Segre_Product A;
dom A = I by PARTFUN1:def 2;
then A.x in rng A by FUNCT_1:3;
then A.x is non trivial by PENCIL_1:def 18;
then reconsider C=[#](A.x) as non trivial set;
reconsider p0 as Element of Carrier A by Th6;
reconsider p={p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider b=p+*(x,C) as Segre-like non trivial-yielding ManySortedSubset of
Carrier A by PENCIL_1:9,10,PENCIL_2:7;
take b;
dom p=I by PARTFUN1:def 2;
then
A1: b.x = C by FUNCT_7:31;
hence
A2: indx(b)=x by PENCIL_1:def 21;
product b c= the carrier of Segre_Product A
proof
let a be object;
assume a in product b;
then consider f being Function such that
A3: a=f and
A4: dom f=dom b and
A5: for x being object st x in dom b holds f.x in b.x by CARD_3:def 5;
dom Carrier A = I by PARTFUN1:def 2;
then
A6: dom f = dom Carrier A by A4,PARTFUN1:def 2;
A7: now
let i be object;
assume
A8: i in dom Carrier A;
then reconsider i1=i as Element of I;
A9: f.i in b.i by A4,A5,A6,A8;
per cases;
suppose
i1=x;
hence f.i in (Carrier A).i by A1,A9,Th7;
end;
suppose
A10: i1<>x;
I = dom A by PARTFUN1:def 2;
then A.i1 in rng A by FUNCT_1:3;
then A.i1 is non trivial by PENCIL_1:def 18;
then reconsider AA=the carrier of A.i1 as non trivial set;
f.i1 in p.i1 by A9,A10,FUNCT_7:32;
then f.i1 in {p0.i1} by PZFMISC1:def 1;
then f.i1 = p0.i1 by TARSKI:def 1;
then
A11: f.i1 is Element of (Carrier A).i1 by PBOOLE:def 14;
AA is non empty;
then [#](A.i1) is non empty;
then (Carrier A).i1 is non empty by Th7;
hence f.i in (Carrier A).i by A11;
end;
end;
Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by
PENCIL_1:def 23;
hence thesis by A3,A6,A7,CARD_3:def 5;
end;
hence thesis by A1,A2,PENCIL_2:def 2;
end;
theorem Th9:
for I being non empty set for i being Element of I for A be
non-Trivial-yielding TopStruct-yielding ManySortedSet of I for p being Point
of Segre_Product A ex L being Segre-like non trivial-yielding ManySortedSubset
of Carrier A st indx(L)=i & product L is Segre-Coset of A & p in product L
proof
let I being non empty set;
let x being Element of I;
let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I;
let p0 be Point of Segre_Product A;
dom A = I by PARTFUN1:def 2;
then A.x in rng A by FUNCT_1:3;
then A.x is non trivial by PENCIL_1:def 18;
then reconsider C=[#](A.x) as non trivial set;
reconsider p09=p0 as Element of Carrier A by Th6;
reconsider p={p09} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider b=p+*(x,C) as Segre-like non trivial-yielding ManySortedSubset of
Carrier A by PENCIL_1:9,10,PENCIL_2:7;
take b;
dom p=I by PARTFUN1:def 2;
then
A1: b.x = C by FUNCT_7:31;
hence
A2: indx(b)=x by PENCIL_1:def 21;
product b c= the carrier of Segre_Product A
proof
let a be object;
assume a in product b;
then consider f being Function such that
A3: a=f and
A4: dom f=dom b and
A5: for x being object st x in dom b holds f.x in b.x by CARD_3:def 5;
dom Carrier A = I by PARTFUN1:def 2;
then
A6: dom f = dom Carrier A by A4,PARTFUN1:def 2;
A7: now
let i be object;
assume
A8: i in dom Carrier A;
then reconsider i1=i as Element of I;
A9: f.i in b.i by A4,A5,A6,A8;
per cases;
suppose
i1=x;
hence f.i in (Carrier A).i by A1,A9,Th7;
end;
suppose
A10: i1<>x;
I = dom A by PARTFUN1:def 2;
then A.i1 in rng A by FUNCT_1:3;
then A.i1 is non trivial by PENCIL_1:def 18;
then reconsider AA=the carrier of A.i1 as non trivial set;
f.i1 in p.i1 by A9,A10,FUNCT_7:32;
then f.i1 in {p09.i1} by PZFMISC1:def 1;
then f.i1 = p09.i1 by TARSKI:def 1;
then
A11: f.i1 is Element of (Carrier A).i1 by PBOOLE:def 14;
AA is non empty;
then [#](A.i1) is non empty;
then (Carrier A).i1 is non empty by Th7;
hence f.i in (Carrier A).i by A11;
end;
end;
Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by
PENCIL_1:def 23;
hence thesis by A3,A6,A7,CARD_3:def 5;
end;
hence product b is Segre-Coset of A by A1,A2,PENCIL_2:def 2;
A12: dom p = I by PARTFUN1:def 2;
A13: now
let z be object;
assume
A14: z in I;
then reconsider z1=z as Element of I;
dom A = I by PARTFUN1:def 2;
then A.z in rng A by A14,FUNCT_1:def 3;
then A.z is non trivial 1-sorted by PENCIL_1:def 18;
then reconsider tc = the carrier of A.z1 as non trivial set;
A15: tc is non empty;
per cases;
suppose
A16: z=x;
p09.z1 is Element of (Carrier A).z1 by PBOOLE:def 14;
then p09.z1 is Element of [#](A.z1) by Th7;
then p09.z1 in the carrier of A.z1 by A15;
hence p09.z in p+*(x,C).z by A12,A16,FUNCT_7:31;
end;
suppose
z<>x;
then p+*(x,C).z = p.z by FUNCT_7:32;
then p+*(x,C).z = {p09.z} by A14,PZFMISC1:def 1;
hence p09.z in p+*(x,C).z by TARSKI:def 1;
end;
end;
dom p09 = I & dom (p+*(x,C)) = I by PARTFUN1:def 2;
hence thesis by A13,CARD_3:9;
end;
theorem Th10:
for I being non empty set for A being non-Trivial-yielding
TopStruct-yielding ManySortedSet of I for b being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b is Segre-Coset of A
holds b.indx(b) = [#](A.indx(b))
proof
let I be non empty set;
let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I;
let b be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
assume product b is Segre-Coset of A;
then consider
L being Segre-like non trivial-yielding ManySortedSubset of Carrier
A such that
A1: product b = product L and
A2: L.indx(L) = [#](A.indx(L)) by PENCIL_2:def 2;
b=L by A1,PUA2MSS1:2;
hence thesis by A2;
end;
theorem Th11:
for I being non empty set for A be non-Trivial-yielding
TopStruct-yielding ManySortedSet of I for L1,L2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product L1 is Segre-Coset of
A & product L2 is Segre-Coset of A & indx(L1) = indx(L2) & product L1 meets
product L2 holds L1=L2
proof
let I be non empty set;
let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I;
let L1,L2 being Segre-like non trivial-yielding ManySortedSubset of Carrier
A;
assume that
A1: product L1 is Segre-Coset of A & product L2 is Segre-Coset of A and
A2: indx(L1) = indx(L2) and
A3: product L1 meets product L2;
reconsider B1=product L1, B2=product L2 as Segre-Coset of A by A1;
B1 /\ B2 <> {} by A3;
then consider x being object such that
A4: x in B1 /\ B2 by XBOOLE_0:def 1;
A5: x in B2 by A4,XBOOLE_0:def 4;
A6: x in B1 by A4,XBOOLE_0:def 4;
reconsider x as Element of Carrier A by A4,Th6;
consider b1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A7: B1=product b1 and
A8: b1.indx(b1)=[#](A.indx(b1)) by PENCIL_2:def 2;
consider b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A9: B2=product b2 and
A10: b2.indx(b2)=[#](A.indx(b2)) by PENCIL_2:def 2;
A11: b2=L2 by A9,PUA2MSS1:2;
A12: dom L1 = I by PARTFUN1:def 2
.= dom L2 by PARTFUN1:def 2;
A13: b1=L1 by A7,PUA2MSS1:2;
now
let a be object;
assume
A14: a in dom L1;
then reconsider i=a as Element of I;
per cases;
suppose
i=indx(L1);
hence L1.a = L2.a by A2,A8,A10,A13,A11;
end;
suppose
A15: i<>indx(L1);
then L1.i is non empty trivial by PENCIL_1:def 21;
then L1.i is 1-element;
then consider o1 being object such that
A16: L1.i = {o1} by ZFMISC_1:131;
L2.i is non empty trivial by A2,A15,PENCIL_1:def 21;
then L2.i is 1-element;
then consider o2 being object such that
A17: L2.i = {o2} by ZFMISC_1:131;
A18: x.i in L2.i by A5,A12,A14,CARD_3:9;
x.i in L1.i by A6,A14,CARD_3:9;
then o1 = x.i by A16,TARSKI:def 1
.= o2 by A17,A18,TARSKI:def 1;
hence L1.a = L2.a by A16,A17;
end;
end;
hence thesis by A12;
end;
theorem Th12:
for I being non empty set for A be PLS-yielding ManySortedSet of
I for L being Segre-like non trivial-yielding ManySortedSubset of Carrier A for
B being Block of A.indx(L) holds product(L+*(indx(L),B)) is Block of
Segre_Product A
proof
let I being non empty set;
let A be PLS-yielding ManySortedSet of I;
let L being Segre-like non trivial-yielding ManySortedSubset of Carrier A;
let B being Block of A.indx(L);
B in the topology of A.indx(L);
then reconsider B1=B as Subset of A.indx(L);
A1: now
let i be Element of I;
assume
A2: i <> indx(L);
then L+*(indx(L),B1).i = L.i by FUNCT_7:32;
hence L+*(indx(L),B1).i is 1-element by A2,PENCIL_1:12;
end;
2 c= card B by PENCIL_1:def 6;
then B1 is non trivial by PENCIL_1:4;
then reconsider S=L+*(indx(L),B1) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by A1,PENCIL_1:9,def 20,PENCIL_2:7;
A3: now
assume indx(S)<>indx(L);
then S.indx(S) is 1-element by A1;
hence contradiction by PENCIL_1:def 21;
end;
dom L = I by PARTFUN1:def 2;
then S.indx(S) = B1 by A3,FUNCT_7:31;
hence thesis by A3,PENCIL_1:24;
end;
theorem Th13:
for I being non empty set for A be PLS-yielding ManySortedSet of
I for i being Element of I for p being Point of A.i for L being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st i<>indx(L) holds L+*(i,{p})
is Segre-like non trivial-yielding ManySortedSubset of Carrier A
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let i be Element of I;
let p be Point of A.i;
let L be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
A1: now
let j be Element of I;
A2: dom L=I by PARTFUN1:def 2;
assume
A3: j<>indx(L);
per cases;
suppose
j=i;
hence L+*(i,{p}).j is 1-element by A2,FUNCT_7:31;
end;
suppose
j<>i;
then L+*(i,{p}).j = L.j by FUNCT_7:32;
hence L+*(i,{p}).j is 1-element by A3,PENCIL_1:12;
end;
end;
A4: L+*(i,{p}) c= Carrier A
proof
let a be object;
assume
A5: a in I;
then reconsider a1=a as Element of I;
A6: a1 in dom L by A5,PARTFUN1:def 2;
per cases;
suppose
A7: a=i;
then L+*(i,{p}).a1 = {p} by A6,FUNCT_7:31;
then L+*(i,{p}).a1 c= [#](A.a1) by A7;
hence thesis by Th7;
end;
suppose
A8: a<>i;
A9: L c= Carrier A by PBOOLE:def 18;
L+*(i,{p}).a1 = L.a1 by A8,FUNCT_7:32;
hence thesis by A9;
end;
end;
assume i<>indx(L);
then L+*(i,{p}).indx(L) = L.indx(L) by FUNCT_7:32;
then
A10: L+*(i,{p}).indx(L) is non trivial by PENCIL_1:def 21;
dom (L+*(i,{p})) = I by PARTFUN1:def 2;
then L+*(i,{p}).indx(L) in rng (L+*(i,{p})) by FUNCT_1:3;
hence thesis by A4,A1,A10,PBOOLE:def 18,PENCIL_1:def 16,def 20;
end;
theorem Th14:
for I being non empty set for A being PLS-yielding ManySortedSet
of I for i being Element of I for S being Subset of A.i for L being Segre-like
non trivial-yielding ManySortedSubset of Carrier A holds product (L+*(i,S)) is
Subset of Segre_Product A
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let i be Element of I;
let S be Subset of A.i;
let L be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
A1: dom (L+*(i,S)) = I by PARTFUN1:def 2
.= dom Carrier A by PARTFUN1:def 2;
A2: now
let a be object;
assume a in dom (L+*(i,S));
then
A3: a in I;
then
A4: a in dom L by PARTFUN1:def 2;
per cases;
suppose
A5: a=i;
then (L+*(i,S)).a = S by A4,FUNCT_7:31;
then (L+*(i,S)).a c= [#](A.i);
hence (L+*(i,S)).a c= (Carrier A).a by A5,Th7;
end;
suppose
A6: a<>i;
A7: L c= Carrier A by PBOOLE:def 18;
(L+*(i,S)).a = L.a by A6,FUNCT_7:32;
hence (L+*(i,S)).a c= (Carrier A).a by A3,A7;
end;
end;
Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by
PENCIL_1:def 23;
hence thesis by A1,A2,CARD_3:27;
end;
theorem Th15:
for I being non empty set for P being ManySortedSet of I for i
being Element of I holds {P}.i is 1-element
proof
let I being non empty set;
let P be ManySortedSet of I;
let i be Element of I;
{P}.i = {P.i} by PZFMISC1:def 1;
hence thesis;
end;
theorem Th16:
for I being non empty set for i being Element of I for A be
PLS-yielding ManySortedSet of I for B being Block of A.i for P being Element of
Carrier A holds product({P}+*(i,B)) is Block of Segre_Product A
proof
let I being non empty set;
let i be Element of I;
let A be PLS-yielding ManySortedSet of I;
let B being Block of A.i;
let P being Element of Carrier A;
reconsider PP={P} as ManySortedSubset of Carrier A by PENCIL_1:11;
B in the topology of A.i;
then reconsider B1=B as Subset of A.i;
A1: now
let j be Element of I;
assume j <> i;
then {P}+*(i,B1).j = {P}.j by FUNCT_7:32;
hence {P}+*(i,B1).j is 1-element by Th15;
end;
2 c= card B by PENCIL_1:def 6;
then B1 is non trivial by PENCIL_1:4;
then reconsider
S=PP+*(i,B1) as Segre-like non trivial-yielding ManySortedSubset
of Carrier A by A1,PENCIL_1:9,def 20,PENCIL_2:7;
A2: now
assume indx(S)<>i;
then S.indx(S) is 1-element by A1;
hence contradiction by PENCIL_1:def 21;
end;
dom {P} = I by PARTFUN1:def 2;
then S.indx(S) = B1 by A2,FUNCT_7:31;
hence thesis by A2,PENCIL_1:24;
end;
theorem Th17:
for I being non empty set for A being PLS-yielding ManySortedSet
of I for p,q being Point of Segre_Product A st p<>q holds p,q are_collinear iff
for p1,q1 being ManySortedSet of I st p1=p & q1=q ex i being Element of I st (
for a,b being Point of A.i st a=p1.i & b=q1.i holds a<>b & a,b are_collinear) &
for j being Element of I st j<>i holds p1.j = q1.j
proof
let I being non empty set;
let A being PLS-yielding ManySortedSet of I;
let p,q being Point of Segre_Product A;
assume
A1: p<>q;
thus p,q are_collinear implies for p1,q1 being ManySortedSet of I st p1=p &
q1=q ex i being Element of I st (for a,b being Point of A.i st a=p1.i & b=q1.i
holds a<>b & a,b are_collinear) & for j being Element of I st j<>i holds p1.j =
q1.j
proof
assume p,q are_collinear;
then consider l being Block of Segre_Product A such that
A2: {p,q} c= l by A1,PENCIL_1:def 1;
let p1,q1 be ManySortedSet of I;
assume that
A3: p1=p and
A4: q1=q;
A5: q1 in l by A2,A4,ZFMISC_1:32;
consider L being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A6: l = product L and
A7: L.indx(L) is Block of A.indx(L) by PENCIL_1:24;
take i=indx(L);
A8: p1 in l by A2,A3,ZFMISC_1:32;
thus for a,b being Point of A.i st a=p1.i & b=q1.i holds a<>b & a,b
are_collinear
proof
reconsider LI=L.indx(L) as Block of A.indx(L) by A7;
let a,b being Point of A.i;
A9: ex p0 being Function st p0=p1 & dom p0=dom L &
for o being object st o
in dom L holds p0.o in L.o by A6,A8,CARD_3:def 5;
A10: ex q0 being Function st q0=q1 & dom q0=dom L &
for o being object st o
in dom L holds q0.o in L.o by A6,A5,CARD_3:def 5;
assume
A11: a=p1.i & b=q1.i;
now
assume
A12: a=b;
A13: now
let o be object;
assume
A14: o in dom p1;
then reconsider o1=o as Element of I;
per cases;
suppose
o1=i;
hence p1.o = q1.o by A11,A12;
end;
suppose
o1<>i;
then L.o1 is 1-element by PENCIL_1:12;
then consider s being object such that
A15: L.o1 = {s} by ZFMISC_1:131;
p1.o in {s} by A9,A14,A15;
then
A16: p1.o = s by TARSKI:def 1;
q1.o in {s} by A9,A10,A14,A15;
hence p1.o = q1.o by A16,TARSKI:def 1;
end;
end;
dom p1 = I by PARTFUN1:def 2
.= dom q1 by PARTFUN1:def 2;
hence contradiction by A1,A3,A4,A13,FUNCT_1:2;
end;
hence a<>b;
A17: dom L = I by PARTFUN1:def 2;
then
A18: q1.i in LI by A10;
p1.i in LI by A9,A17;
then {a,b} c= LI by A11,A18,ZFMISC_1:32;
hence thesis by PENCIL_1:def 1;
end;
let j being Element of I;
assume j<>i;
hence thesis by A6,A8,A5,PENCIL_1:23;
end;
reconsider p1=p,q1=q as Element of Carrier A by Th6;
assume for p1,q1 being ManySortedSet of I st p1=p & q1=q ex i being
Element of I st (for a,b being Point of A.i st a=p1.i & b=q1.i holds a<>b & a,b
are_collinear) & for j being Element of I st j<>i holds p1.j = q1.j;
then consider i being Element of I such that
A19: for a,b being Point of A.i st a=p1.i & b=q1.i holds a<>b & a,b
are_collinear and
A20: for j being Element of I st j<>i holds p1.j = q1.j;
q1.i is Element of (Carrier A).i by PBOOLE:def 14;
then q1.i is Element of [#](A.i) by Th7;
then reconsider b=q1.i as Point of A.i;
p1.i is Element of (Carrier A).i by PBOOLE:def 14;
then p1.i is Element of [#](A.i) by Th7;
then reconsider a=p1.i as Point of A.i;
A21: a,b are_collinear by A19;
per cases by A21,PENCIL_1:def 1;
suppose
a=b;
hence thesis by A19;
end;
suppose
ex l being Block of A.i st {a,b} c= l;
then consider l being Block of A.i such that
A22: {a,b} c= l;
reconsider L=product ({p1}+*(i,l)) as Block of Segre_Product A by Th16;
A23: dom ({p1}+*(i,l)) = I by PARTFUN1:def 2;
then
A24: dom {p1} = dom ({p1}+*(i,l)) by PARTFUN1:def 2;
A25: for o being object st o in dom ({p1}+*(i,l))
holds q1.o in ({p1}+*(i,l)) .o
proof
let o be object;
assume
A26: o in dom ({p1}+*(i,l));
then reconsider o1=o as Element of I;
per cases;
suppose
A27: o1 = i;
then ({p1}+*(i,l)).o = l by A24,A26,FUNCT_7:31;
hence thesis by A22,A27,ZFMISC_1:32;
end;
suppose
A28: o1 <> i;
then ({p1}+*(i,l)).o = {p1}.o by FUNCT_7:32;
then ({p1}+*(i,l)).o = {p1.o} by A26,PZFMISC1:def 1;
then ({p1}+*(i,l)).o = {q1.o1} by A20,A28;
hence thesis by TARSKI:def 1;
end;
end;
A29: for o being object st o in dom ({p1}+*(i,l))
holds p1.o in ({p1}+*(i,l)) .o
proof
let o be object;
assume
A30: o in dom ({p1}+*(i,l));
per cases;
suppose
A31: o = i;
then ({p1}+*(i,l)).o = l by A24,A30,FUNCT_7:31;
hence thesis by A22,A31,ZFMISC_1:32;
end;
suppose
o <> i;
then ({p1}+*(i,l)).o = {p1}.o by FUNCT_7:32;
then ({p1}+*(i,l)).o = {p1.o} by A30,PZFMISC1:def 1;
hence thesis by TARSKI:def 1;
end;
end;
dom q1 = dom ({p1}+*(i,l)) by A23,PARTFUN1:def 2;
then
A32: q in L by A25,CARD_3:def 5;
dom p1 = dom ({p1}+*(i,l)) by A23,PARTFUN1:def 2;
then p in L by A29,CARD_3:def 5;
then {p,q} c= L by A32,ZFMISC_1:32;
hence thesis by PENCIL_1:def 1;
end;
end;
theorem Th18:
for I being non empty set for A being PLS-yielding ManySortedSet
of I for b being Segre-like non trivial-yielding ManySortedSubset of Carrier A
for x being Point of A.indx(b) ex p being ManySortedSet of I st p in product b
& {p+*(indx(b),x) qua set} = product(b+*(indx(b),{x}))
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let b1 be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
set i=indx(b1);
let x be Point of A.i;
consider bb being object such that
A1: bb in product b1 by XBOOLE_0:def 1;
A2: ex bf being Function st bf=bb & dom bf=dom b1 &
for o being object st o in
dom b1 holds bf.o in b1.o by A1,CARD_3:def 5;
A3: dom b1=I by PARTFUN1:def 2;
then reconsider bb as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
take p=bb;
thus p in product b1 by A1;
set bbx=bb+*(i,x);
thus {p+*(i,x) qua set}=product(b1+*(i,{x}))
proof
thus {p+*(i,x) qua set} c= product(b1+*(i,{x}))
proof
A4: now
let z be object;
assume z in dom (b1+*(i,{x}));
then
A5: z in I;
then
A6: z in dom bb by PARTFUN1:def 2;
per cases;
suppose
A7: z=i;
then bbx.z = x by A6,FUNCT_7:31;
then bbx.z in {x} by TARSKI:def 1;
hence bbx.z in (b1+*(i,{x})).z by A3,A7,FUNCT_7:31;
end;
suppose
A8: z<>i;
then bbx.z = bb.z by FUNCT_7:32;
then bbx.z in b1.z by A1,A3,A5,CARD_3:9;
hence bbx.z in (b1+*(i,{x})).z by A8,FUNCT_7:32;
end;
end;
let o be object;
assume o in {p+*(i,x) qua set};
then
A9: o = bbx by TARSKI:def 1;
dom bbx = I by PARTFUN1:def 2
.= dom (b1+*(i,{x})) by PARTFUN1:def 2;
hence thesis by A9,A4,CARD_3:9;
end;
let o be object;
assume o in product(b1+*(i,{x}));
then consider u being Function such that
A10: u=o and
A11: dom u=dom (b1+*(i,{x})) and
A12: for z being object st z in dom (b1+*(i,{x})) holds u.z in (b1+*(i,{x
}) ).z by CARD_3:def 5;
A13: now
let z be object;
assume
A14: z in dom u;
then
A15: z in I by A11;
reconsider zz=z as Element of I by A11,A14;
A16: u.z in (b1+*(i,{x})).z by A11,A12,A14;
per cases;
suppose
A17: zz=i;
then u.z in {x} by A3,A16,FUNCT_7:31;
then u.z = x by TARSKI:def 1;
hence u.z = bbx.z by A2,A3,A17,FUNCT_7:31;
end;
suppose
A18: zz<>i;
then b1.zz is non empty trivial by PENCIL_1:def 21;
then b1.zz is 1-element;
then consider o being object such that
A19: b1.z = {o} by ZFMISC_1:131;
u.z in b1.z by A16,A18,FUNCT_7:32;
then
A20: u.z = o by A19,TARSKI:def 1;
bbx.z = bb.z by A18,FUNCT_7:32;
then bbx.z in {o} by A2,A3,A15,A19;
hence u.z = bbx.z by A20,TARSKI:def 1;
end;
end;
dom u = I by A11,PARTFUN1:def 2
.= dom bbx by PARTFUN1:def 2;
then u=bbx by A13;
hence thesis by A10,TARSKI:def 1;
end;
end;
definition
let I be finite non empty set;
let b1,b2 be ManySortedSet of I;
func diff(b1,b2) -> Nat equals
card {i where i is Element of I: b1.i <> b2.i};
correctness
proof
{i where i is Element of I: b1.i <> b2.i} c= I
proof
let a be object;
assume a in {i where i is Element of I: b1.i <> b2.i};
then ex i being Element of I st a=i & b1.i<>b2.i;
hence thesis;
end;
then reconsider
F={i where i is Element of I: b1.i <> b2.i} as finite set by FINSET_1:1;
card F = card F;
hence thesis;
end;
end;
theorem Th19:
for I being finite non empty set for b1,b2 being ManySortedSet
of I for i being Element of I st b1.i<>b2.i holds diff(b1,b2) = diff(b1,b2+*(i,
b1.i)) + 1
proof
let I be finite non empty set;
let b1,b2 be ManySortedSet of I;
let j be Element of I;
set b3=b2+*(j,b1.j);
{i where i is Element of I: b1.i <> b2.i} c= I
proof
let a be object;
assume a in {i where i is Element of I: b1.i <> b2.i};
then ex i being Element of I st a=i & b1.i<>b2.i;
hence thesis;
end;
then reconsider
F={i where i is Element of I: b1.i <> b2.i} as finite set by FINSET_1:1;
{i where i is Element of I: b1.i <> b3.i} c= I
proof
let a be object;
assume a in {i where i is Element of I: b1.i <> b3.i};
then ex i being Element of I st a=i & b1.i<>b3.i;
hence thesis;
end;
then reconsider
G={i where i is Element of I: b1.i <> b3.i} as finite set by FINSET_1:1;
assume
A1: b1.j<>b2.j;
A2: F = G \/ {j}
proof
thus F c= G \/ {j}
proof
let o be object;
assume o in F;
then consider i being Element of I such that
A3: o=i and
A4: b1.i <> b2.i;
per cases;
suppose
i=j;
then o in {j} by A3,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
i<>j;
then b3.i=b2.i by FUNCT_7:32;
then i in G by A4;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
let o be object;
assume
A5: o in G \/ {j};
per cases by A5,XBOOLE_0:def 3;
suppose
o in G;
then consider i being Element of I such that
A6: o=i and
A7: b1.i <> b3.i;
now
assume
A8: b1.i = b2.i;
then i=j by A7,FUNCT_7:32;
hence contradiction by A1,A8;
end;
hence thesis by A6;
end;
suppose
o in {j};
then o=j by TARSKI:def 1;
hence thesis by A1;
end;
end;
now
assume j in G;
then
A9: ex jj being Element of I st jj=j & b1.jj <> b3.jj;
dom b2=I by PARTFUN1:def 2;
hence contradiction by A9,FUNCT_7:31;
end;
hence thesis by A2,CARD_2:41;
end;
begin :: The adherence of Segre cosets
definition
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let B1,B2 be Segre-Coset of A;
pred B1 '||' B2 means
for x being Point of Segre_Product A st x in B1
ex y being Point of Segre_Product A st y in B2 & x,y are_collinear;
end;
theorem Th20:
for I being non empty set for A being PLS-yielding ManySortedSet
of I for B1,B2 being Segre-Coset of A st B1 '||' B2 for f being Collineation of
Segre_Product A for C1,C2 being Segre-Coset of A st C1=f.:B1 & C2=f.:B2 holds
C1 '||' C2
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let B1,B2 be Segre-Coset of A such that
A1: B1 '||' B2;
let f be Collineation of Segre_Product A;
let C1,C2 be Segre-Coset of A such that
A2: C1=f.:B1 and
A3: C2=f.:B2;
let x be Point of Segre_Product A;
assume x in C1;
then consider a being object such that
A4: a in dom f and
A5: a in B1 and
A6: x=f.a by A2,FUNCT_1:def 6;
reconsider a as Point of Segre_Product A by A4;
consider b being Point of Segre_Product A such that
A7: b in B2 and
A8: a,b are_collinear by A1,A5;
take y=f.b;
A9: dom f = the carrier of Segre_Product A by FUNCT_2:def 1;
hence y in C2 by A3,A7,FUNCT_1:def 6;
per cases;
suppose
a=b;
hence thesis by A6,PENCIL_1:def 1;
end;
suppose
a<>b;
then consider l being Block of Segre_Product A such that
A10: {a,b} c= l by A8,PENCIL_1:def 1;
reconsider k=f.:l as Block of Segre_Product A;
b in l by A10,ZFMISC_1:32;
then
A11: y in k by A9,FUNCT_1:def 6;
a in l by A10,ZFMISC_1:32;
then x in k by A4,A6,FUNCT_1:def 6;
then {x,y} c= k by A11,ZFMISC_1:32;
hence thesis by PENCIL_1:def 1;
end;
end;
theorem Th21:
for I being non empty set for A being PLS-yielding ManySortedSet
of I for B1,B2 being Segre-Coset of A st B1 misses B2 holds B1 '||' B2 iff for
b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1
= product b1 & B2 = product b2 holds indx(b1)=indx(b2) & ex r being Element of
I st r<>indx(b1) & (for i being Element of I st i<>r holds b1.i=b2.i) & for c1,
c2 being Point of A.r st b1.r = {c1} & b2.r = {c2} holds c1,c2 are_collinear
proof
let I being non empty set;
let A being PLS-yielding ManySortedSet of I;
let B1,B2 being Segre-Coset of A;
consider L1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A1: B1 = product L1 and
L1.indx(L1) = [#](A.indx(L1)) by PENCIL_2:def 2;
assume
A2: B1 misses B2;
thus B1 '||' B2 implies for b1,b2 being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds indx(
b1)=indx(b2) & ex r being Element of I st r<>indx(b1) & (for i being Element of
I st i<>r holds b1.i=b2.i) & for c1,c2 being Point of A.r st b1.r={c1} & b2.r={
c2} holds c1,c2 are_collinear
proof
assume
A3: B1 '||' B2;
consider L2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A4: B2 = product L2 and
A5: L2.indx(L2) = [#](A.indx(L2)) by PENCIL_2:def 2;
consider L1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A6: B1 = product L1 and
A7: L1.indx(L1) = [#](A.indx(L1)) by PENCIL_2:def 2;
let b1,b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A;
assume that
A8: B1 = product b1 and
A9: B2 = product b2;
A10: b1 = L1 by A8,A6,PUA2MSS1:2;
thus
A11: indx(b1)=indx(b2)
proof
assume indx(b1)<>indx(b2);
then b2.indx(b1) is 1-element by PENCIL_1:12;
then consider c2 being object such that
A12: b2.indx(b1)={c2} by ZFMISC_1:131;
set bl = the Block of A.indx(b1);
consider p0 being object such that
A13: p0 in B1 by A8,XBOOLE_0:def 1;
reconsider p0 as Point of Segre_Product A by A13;
reconsider p=p0 as Element of Carrier A by Th6;
bl in the topology of A.indx(b1);
then 2 c= card bl & card bl c= card (the carrier of (A.indx(b1))) by
CARD_1:11,PENCIL_1:def 6;
then consider a being object such that
A14: a in the carrier of (A.indx(b1)) and
A15: a <> c2 by PENCIL_1:3,XBOOLE_1:1;
reconsider a as Point of A.indx(b1) by A14;
reconsider x=p+*(indx(b1),a) as Point of Segre_Product A by PENCIL_1:25;
reconsider x1=x as Element of Carrier A by Th6;
A16: dom x1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2;
now
let i be object;
assume
A17: i in dom x1;
then i in I;
then
A18: i in dom p by PARTFUN1:def 2;
per cases;
suppose
A19: i=indx(b1);
then x1.i = a by A18,FUNCT_7:31;
hence x1.i in b1.i by A7,A10,A19;
end;
suppose
i<>indx(b1);
then
A20: x1.i = p.i by FUNCT_7:32;
ex f being Function st f=p & dom f = dom b1 &
for a being object st
a in dom b1 holds f.a in b1.a by A8,A13,CARD_3:def 5;
hence x1.i in b1.i by A16,A17,A20;
end;
end;
then
A21: x in B1 by A8,A16,CARD_3:def 5;
then consider y being Point of Segre_Product A such that
A22: y in B2 and
A23: x,y are_collinear by A3;
reconsider y1=y as Element of Carrier A by Th6;
per cases;
suppose
y=x;
then y in B1 /\ B2 by A21,A22,XBOOLE_0:def 4;
hence contradiction by A2;
end;
suppose
y<>x;
then consider i0 being Element of I such that
for a,b being Point of A.i0 st a=x1.i0 & b=y1.i0 holds a<>b & a,b
are_collinear and
A24: for j being Element of I st j<>i0 holds x1.j = y1.j by A23,Th17;
A25: dom y1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2;
now
let i be object;
assume
A26: i in dom y1;
then reconsider i5=i as Element of I;
per cases;
suppose
A27: i=indx(b1);
reconsider i1=i as Element of I by A26;
y1.i1 is Element of (Carrier A).i1 by PBOOLE:def 14;
then y1.i1 is Element of [#](A.i1) by Th7;
hence y1.i in b1.i by A7,A10,A27;
end;
suppose
A28: i<>indx(b1);
(ex g being Function st g=y1 & dom g = dom b2 &
for a being object st a in dom b2 holds g.a in b2.a )& dom b2 = I
by A9,A22,CARD_3:def 5
,PARTFUN1:def 2;
then y1.indx(b1) in b2.indx(b1);
then
A29: y1.indx(b1) = c2 by A12,TARSKI:def 1;
dom p = I by PARTFUN1:def 2;
then x1.indx(b1) = a by FUNCT_7:31;
then i0 = indx(b1) by A15,A24,A29;
then
A30: y1.i5 = x1.i5 by A24,A28;
A31: x1.i = p.i by A28,FUNCT_7:32;
ex f being Function st f=p & dom f = dom b1 & for a being object
st a in dom b1 holds f.a in b1.a by A8,A13,CARD_3:def 5;
hence y1.i in b1.i by A25,A26,A30,A31;
end;
end;
then y in B1 by A8,A25,CARD_3:def 5;
then y in B1 /\ B2 by A22,XBOOLE_0:def 4;
hence contradiction by A2;
end;
end;
A32: b2 = L2 by A9,A4,PUA2MSS1:2;
thus ex r being Element of I st r<>indx(b1) & (for i being Element of I st
i<>r holds b1.i=b2.i) & for c1,c2 being Point of A.r st b1.r={c1} & b2.r={c2}
holds c1,c2 are_collinear
proof
consider x being object such that
A33: x in B1 by A8,XBOOLE_0:def 1;
reconsider x as Point of Segre_Product A by A33;
consider y being Point of Segre_Product A such that
A34: y in B2 and
A35: x,y are_collinear by A3,A33;
reconsider y1=y as Element of Carrier A by Th6;
reconsider x1=x as Element of Carrier A by Th6;
x <> y by A2,A33,A34,XBOOLE_0:def 4;
then consider r being Element of I such that
A36: for a,b being Point of A.r st a=x1.r & b=y1.r holds a<>b & a,b
are_collinear and
A37: for j being Element of I st j<>r holds x1.j = y1.j by A35,Th17;
take r;
now
assume
A38: r=indx(b1);
A39: now
let o be object;
assume
A40: o in dom b1;
then reconsider o1=o as Element of I;
per cases;
suppose
A41: o1=r;
y1.o1 is Element of (Carrier A).o1 by PBOOLE:def 14;
then y1.o1 is Element of [#](A.o1) by Th7;
hence y1.o in b1.o by A7,A10,A38,A41;
end;
suppose
A42: o1<>r;
then b1.o1 is 1-element by A38,PENCIL_1:12;
then consider c being object such that
A43: b1.o1 = {c} by ZFMISC_1:131;
x1.o1 in b1.o1 by A8,A33,A40,CARD_3:9;
then c = x1.o1 by A43,TARSKI:def 1
.= y1.o1 by A37,A42;
hence y1.o in b1.o by A43,TARSKI:def 1;
end;
end;
dom y1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2;
then y1 in B1 by A8,A39,CARD_3:9;
then B1 /\ B2 <> {} by A34,XBOOLE_0:def 4;
hence contradiction by A2;
end;
hence r<>indx(b1);
thus for i being Element of I st i<>r holds b1.i=b2.i
proof
let i be Element of I;
assume
A44: i<>r;
per cases;
suppose
i=indx(b1);
hence thesis by A7,A5,A10,A32,A11;
end;
suppose
A45: i<>indx(b1);
then b2.i is 1-element by A11,PENCIL_1:12;
then
A46: ex d being object st b2.i = {d} by ZFMISC_1:131;
dom b2 = I by PARTFUN1:def 2;
then
A47: y1.i in b2.i by A9,A34,CARD_3:9;
b1.i is 1-element by A45,PENCIL_1:12;
then consider c being object such that
A48: b1.i = {c} by ZFMISC_1:131;
dom b1 = I by PARTFUN1:def 2;
then x1.i in b1.i by A8,A33,CARD_3:9;
then c = x1.i by A48,TARSKI:def 1
.= y1.i by A37,A44;
hence thesis by A48,A46,A47,TARSKI:def 1;
end;
end;
let c1,c2 being Point of A.r;
assume that
A49: b1.r={c1} and
A50: b2.r={c2};
dom L2 = I by PARTFUN1:def 2;
then y1.r in b2.r by A4,A32,A34,CARD_3:9;
then
A51: c2 = y1.r by A50,TARSKI:def 1;
dom L1 = I by PARTFUN1:def 2;
then x1.r in b1.r by A6,A10,A33,CARD_3:9;
then c1 = x1.r by A49,TARSKI:def 1;
hence thesis by A36,A51;
end;
end;
consider L2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A52: B2 = product L2 and
L2.indx(L2) = [#](A.indx(L2)) by PENCIL_2:def 2;
assume
A53: for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A st B1 = product b1 & B2 = product b2 holds indx(b1)=indx(b2) & ex r
being Element of I st r<>indx(b1) & (for i being Element of I st i<>r holds b1.
i=b2.i) & for c1,c2 being Point of A.r st b1.r={c1} & b2.r={c2} holds c1,c2
are_collinear;
then consider r being Element of I such that
A54: r<>indx(L1) and
A55: for i being Element of I st i<>r holds L1.i=L2.i and
A56: for c1,c2 being Point of A.r st L1.r={c1} & L2.r={c2} holds c1,c2
are_collinear by A1,A52;
indx(L1)=indx(L2) by A53,A1,A52;
then L2.r is 1-element by A54,PENCIL_1:12;
then consider c2 being object such that
A57: L2.r = {c2} by ZFMISC_1:131;
L2 c= Carrier A by PBOOLE:def 18;
then L2.r c= (Carrier A).r;
then {c2} c= [#](A.r) by A57,Th7;
then reconsider c2 as Point of A.r by ZFMISC_1:31;
L1.r is 1-element by A54,PENCIL_1:12;
then consider c1 being object such that
A58: L1.r = {c1} by ZFMISC_1:131;
L1 c= Carrier A by PBOOLE:def 18;
then L1.r c= (Carrier A).r;
then {c1} c= [#](A.r) by A58,Th7;
then reconsider c1 as Point of A.r by ZFMISC_1:31;
A59: now
assume
A60: c1=c2;
A61: now
let s be object;
assume s in dom L1;
then reconsider s1=s as Element of I;
per cases;
suppose
s1=r;
hence L1.s=L2.s by A58,A57,A60;
end;
suppose
s1<>r;
hence L1.s=L2.s by A55;
end;
end;
dom L1 = I by PARTFUN1:def 2
.= dom L2 by PARTFUN1:def 2;
then L1=L2 by A61;
then B1 /\ B1 = {} by A2,A1,A52;
hence contradiction by A1;
end;
c1,c2 are_collinear by A56,A58,A57;
then consider bb being Block of A.r such that
A62: {c1,c2} c= bb by A59,PENCIL_1:def 1;
let x being Point of Segre_Product A;
reconsider x1=x as Element of Carrier A by Th6;
reconsider y=x1+*(r,c2) as Point of Segre_Product A by PENCIL_1:25;
reconsider y1=y as ManySortedSet of I;
assume x in B1;
then
A63: ex x2 being Function st x2=x & dom x2=dom L1 &
for o being object st o in
dom L1 holds x2.o in L1.o by A1,CARD_3:def 5;
A64: now
let a be object;
assume a in dom L2;
then reconsider a1=a as Element of I;
per cases;
suppose
A65: a1=r;
dom x1 = I by PARTFUN1:def 2;
then y1.a = c2 by A65,FUNCT_7:31;
hence y1.a in L2.a by A57,A65,TARSKI:def 1;
end;
suppose
A66: a1<>r;
then dom x1 = I & y1.a1 = x1.a1 by FUNCT_7:32,PARTFUN1:def 2;
then y1.a1 in L1.a1 by A63;
hence y1.a in L2.a by A55,A66;
end;
end;
take y;
dom y1 = I by PARTFUN1:def 2
.= dom L2 by PARTFUN1:def 2;
hence y in B2 by A52,A64,CARD_3:def 5;
reconsider B=product({x1}+*(r,bb)) as Block of Segre_Product A by Th16;
A67: now
let s be object;
assume s in dom y1;
then
A68: s in I;
then
A69: s in dom {x1} & s in dom x1 by PARTFUN1:def 2;
per cases;
suppose
s=r;
then y1.s = c2 & bb = ({x1}+*(r,bb)).s by A69,FUNCT_7:31;
hence y1.s in ({x1}+*(r,bb)).s by A62,ZFMISC_1:32;
end;
suppose
A70: s<>r;
then {x1}.s = ({x1}+*(r,bb)).s by FUNCT_7:32;
then
A71: {x1.s} = ({x1}+*(r,bb)).s by A68,PZFMISC1:def 1;
y1.s = x1.s by A70,FUNCT_7:32;
hence y1.s in ({x1}+*(r,bb)).s by A71,TARSKI:def 1;
end;
end;
dom y1 = I by PARTFUN1:def 2
.= dom({x1}+*(r,bb)) by PARTFUN1:def 2;
then
A72: y in B by A67,CARD_3:def 5;
A73: now
let s be object;
assume
A74: s in dom x1;
then
A75: s in I;
then
A76: s in dom {x1} by PARTFUN1:def 2;
per cases;
suppose
A77: s=r;
x1.s in L1.s by A63,A74;
then
A78: x1.s = c1 by A58,A77,TARSKI:def 1;
bb = ({x1}+*(r,bb)).s by A76,A77,FUNCT_7:31;
hence x1.s in ({x1}+*(r,bb)).s by A62,A78,ZFMISC_1:32;
end;
suppose
s<>r;
then {x1}.s = ({x1}+*(r,bb)).s by FUNCT_7:32;
then {x1.s} = ({x1}+*(r,bb)).s by A75,PZFMISC1:def 1;
hence x1.s in ({x1}+*(r,bb)).s by TARSKI:def 1;
end;
end;
dom x1 = I by PARTFUN1:def 2
.= dom ({x1}+*(r,bb)) by PARTFUN1:def 2;
then x in B by A73,CARD_3:def 5;
then {x,y} c= B by A72,ZFMISC_1:32;
hence thesis by PENCIL_1:def 1;
end;
theorem Th22:
for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is connected for i
being Element of I for p being Point of A.i for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b2 is Segre-Coset of
A & b1=b2+*(i,{p}) & not p in b2.i ex D being FinSequence of bool the carrier
of Segre_Product A st D.1=product b1 & D.(len D)=product b2 & (for i being Nat
st i in dom D holds D.i is Segre-Coset of A) & for i being Nat st 1<=i & i<len
D for Di,Di1 being Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1
& Di '||' Di1
proof
let I be finite non empty set;
let A be PLS-yielding ManySortedSet of I such that
A1: for i being Element of I holds A.i is connected;
let i be Element of I;
let p be Point of A.i;
let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A
such that
A2: product b2 is Segre-Coset of A and
A3: b1=b2+*(i,{p}) and
A4: not p in b2.i;
defpred P[set,set] means for a,b being Point of A.i st $1=a & $2=b holds a,b
are_collinear;
A5: now
assume i=indx(b2);
then b2.i = [#](A.i) by A2,Th10;
hence contradiction by A4;
end;
then b2.i is 1-element by PENCIL_1:12;
then consider q being object such that
A6: b2.i = {q} by ZFMISC_1:131;
b2 c= Carrier A by PBOOLE:def 18;
then b2.i c= (Carrier A).i;
then {q} c= [#](A.i) by A6,Th7;
then reconsider q as Point of A.i by ZFMISC_1:31;
A.i is connected by A1;
then consider f being FinSequence of the carrier of A.i such that
A7: p=f.1 & q=f.(len f) and
A8: for j being Nat st 1 <= j & j < len f for a,b being Point of A.i st
a = f.j & b = f.(j+1) holds a,b are_collinear by PENCIL_1:def 10;
A9: for j being Element of NAT, x,y being set st 1 <= j & j < len f & x=f.j
& y=f.(j+1) holds P[x,y] by A8;
consider F being one-to-one FinSequence of the carrier of A.i such that
A10: p=F.1 & q=F.len F & rng F c= rng f & for j being Element of NAT st
1 <= j & j < len F holds P[F.j,F.(j+1)] from PENCIL_2:sch 1(A7,A9);
A11: now
assume F={};
then dom F = {};
then F.1 = {} & F.(len F) = {} by FUNCT_1:def 2;
hence contradiction by A4,A6,A10,TARSKI:def 1;
end;
deffunc H(set) = product (b2+*(i,{F.$1}));
consider G being FinSequence such that
A12: len G = len F & for j being Nat st j in dom G holds G.j=H(j) from
FINSEQ_1:sch 2;
rng G c= bool the carrier of Segre_Product A
proof
let a be object;
assume a in rng G;
then consider o being object such that
A13: o in dom G and
A14: G.o=a by FUNCT_1:def 3;
reconsider o as Element of NAT by A13;
dom G = dom F by A12,FINSEQ_3:29;
then F.o in rng F by A13,FUNCT_1:3;
then {F.o} is Subset of A.i by ZFMISC_1:31;
then
A15: product (b2+*(i,{F.o})) is Subset of Segre_Product A by Th14;
G.o = product (b2+*(i,{F.o})) by A12,A13;
hence thesis by A14,A15;
end;
then reconsider
D=G as FinSequence of bool the carrier of Segre_Product A by FINSEQ_1:def 4;
take D;
A16: dom G = Seg len F by A12,FINSEQ_1:def 3;
dom F = Seg (len F) by FINSEQ_1:def 3;
hence D.1=product b1 by A3,A10,A12,A16,A11,FINSEQ_3:32;
D.(len D) = product (b2+*(i,{F.(len F)})) by A12,A16,A11,FINSEQ_1:3;
hence D.(len D)=product b2 by A6,A10,FUNCT_7:35;
thus for j being Nat st j in dom D holds D.j is Segre-Coset of A
proof
let j be Nat;
assume
A17: j in dom D;
then j in Seg (len F) by A12,FINSEQ_1:def 3;
then j in dom F by FINSEQ_1:def 3;
then F.j in rng F by FUNCT_1:3;
then reconsider Fj=F.j as Point of A.i;
reconsider BB=b2+*(i,{Fj}) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by A5,Th13;
BB.indx(b2) = b2.indx(b2) by A5,FUNCT_7:32;
then BB.indx(b2) is non trivial by PENCIL_1:def 21;
then
A18: indx(BB)=indx(b2) by PENCIL_1:def 21;
then
A19: BB.indx(BB)=b2.indx(b2) by A5,FUNCT_7:32
.=[#](A.indx(BB)) by A2,A18,Th10;
A20: D.j = product BB by A12,A17;
then D.j is Subset of Segre_Product A by Th14;
hence thesis by A20,A19,PENCIL_2:def 2;
end;
A21: dom b2=I by PARTFUN1:def 2;
thus for i being Nat st 1<=i & i<len D for Di,Di1 being Segre-Coset of A st
Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1
proof
let j be Nat;
assume
A22: 1<=j & j<len D;
let Di,Di1 be Segre-Coset of A such that
A23: Di=D.j and
A24: Di1=D.(j+1);
reconsider j as Element of NAT by ORDINAL1:def 12;
j in dom D by A22,FINSEQ_3:25;
then j in Seg (len F) by A12,FINSEQ_1:def 3;
then j in dom F by FINSEQ_1:def 3;
then F.j in rng F by FUNCT_1:3;
then reconsider Fj=F.j as Point of A.i;
reconsider BB1=b2+*(i,{Fj}) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by A5,Th13;
A25: j in dom D by A22,FINSEQ_3:25;
then
A26: D.j = product BB1 by A12;
1<=j+1 & j+1 <= len D by A22,NAT_1:13;
then j+1 in dom D by FINSEQ_3:25;
then j+1 in Seg (len F) by A12,FINSEQ_1:def 3;
then j+1 in dom F by FINSEQ_1:def 3;
then F.(j+1) in rng F by FUNCT_1:3;
then reconsider Fj2=F.(j+1) as Point of A.i;
reconsider BB2=b2+*(i,{Fj2}) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by A5,Th13;
1<=j+1 & j+1<=len D by A22,NAT_1:13;
then
A27: j+1 in dom D by FINSEQ_3:25;
then
A28: j+1 in Seg len F by A12,FINSEQ_1:def 3;
A29: D.(j+1) = product BB2 by A12,A27;
A30: j in Seg len F by A12,A25,FINSEQ_1:def 3;
thus
A31: Di misses Di1
proof
A32: j<>j+1;
assume Di /\ Di1 <> {};
then consider x being object such that
A33: x in Di /\ Di1 by XBOOLE_0:def 1;
x in Di1 by A33,XBOOLE_0:def 4;
then consider x2 being Function such that
A34: x2=x and
dom x2=dom (b2+*(i,{F.(j+1)})) and
A35: for o being object st o in dom (b2+*(i,{F.(j+1)})) holds x2.o in (
b2+* (i,{F.(j+1)})).o by A24,A29,CARD_3:def 5;
dom (b2+*(i,{F.(j+1)})) = I by PARTFUN1:def 2;
then x2.i in (b2+*(i,{F.(j+1)})).i by A35;
then x2.i in {F.(j+1)} by A21,FUNCT_7:31;
then
A36: x2.i = F.(j+1) by TARSKI:def 1;
x in Di by A33,XBOOLE_0:def 4;
then consider x1 being Function such that
A37: x1=x and
dom x1=dom (b2+*(i,{F.j})) and
A38: for o being object st o in dom (b2+*(i,{F.j})) holds x1.o in (b2+*
(i,{ F.j})).o by A23,A26,CARD_3:def 5;
dom (b2+*(i,{F.j})) = I by PARTFUN1:def 2;
then x1.i in (b2+*(i,{F.j})).i by A38;
then x1.i in {F.j} by A21,FUNCT_7:31;
then
A39: x1.i = F.j by TARSKI:def 1;
j in dom F & j+1 in dom F by A30,A28,FINSEQ_1:def 3;
hence contradiction by A37,A34,A39,A36,A32,FUNCT_1:def 4;
end;
now
let c1,c2 be Segre-like non trivial-yielding ManySortedSubset of Carrier
A such that
A40: Di = product c1 and
A41: Di1 = product c2;
A42: c2 = b2+*(i,{F.(j+1)}) by A24,A29,A41,PUA2MSS1:2;
then c2.indx(b2)=b2.indx(b2) by A5,FUNCT_7:32;
then
A43: c2.indx(b2) is non trivial by PENCIL_1:def 21;
A44: c1 = b2+*(i,{F.j}) by A23,A26,A40,PUA2MSS1:2;
then c1.indx(b2)=b2.indx(b2) by A5,FUNCT_7:32;
then
A45: c1.indx(b2) is non trivial by PENCIL_1:def 21;
then indx(c1) = indx(b2) by PENCIL_1:def 21;
hence indx(c1)=indx(c2) by A43,PENCIL_1:def 21;
take r=i;
thus r<>indx(c1) by A5,A45,PENCIL_1:def 21;
thus for j being Element of I st j<>r holds c1.j=c2.j
proof
let j be Element of I;
assume
A46: j<>r;
hence c1.j = b2.j by A44,FUNCT_7:32
.= c2.j by A42,A46,FUNCT_7:32;
end;
thus for p1,p2 being Point of A.r st c1.r={p1} & c2.r={p2} holds p1,p2
are_collinear
proof
let p1,p2 be Point of A.r such that
A47: c1.r={p1} and
A48: c2.r={p2};
c2.r = {F.(j+1)} by A21,A42,FUNCT_7:31;
then
A49: F.(j+1)=p2 by A48,ZFMISC_1:3;
c1.r = {F.j} by A21,A44,FUNCT_7:31;
then F.j=p1 by A47,ZFMISC_1:3;
hence thesis by A10,A12,A22,A49;
end;
end;
hence thesis by A31,Th21;
end;
end;
theorem Th23:
for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is connected for B1,B2
being Segre-Coset of A st B1 misses B2 for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & B2 =
product b2 holds indx(b1)=indx(b2) iff ex D being FinSequence of bool the
carrier of Segre_Product A st D.1=B1 & D.(len D)=B2 & (for i being Nat st i in
dom D holds D.i is Segre-Coset of A) & for i being Nat st 1<=i & i<len D for Di
,Di1 being Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di
'||' Di1
proof
let I be finite non empty set;
let A be PLS-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds A.i is connected;
let B1,B2 be Segre-Coset of A such that
A2: B1 misses B2;
let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A
such that
A3: B1 = product b1 and
A4: B2 = product b2;
thus indx(b1)=indx(b2) implies ex D being FinSequence of bool the carrier of
Segre_Product A st D.1=B1 & D.(len D)=B2 & (for i being Nat st i in dom D holds
D.i is Segre-Coset of A) & for i being Nat st 1<=i & i<len D for Di,Di1 being
Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1
proof
defpred P[Nat] means for c1,c2 being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st indx(c1) = indx(c2) & product c1 is
Segre-Coset of A & product c2 is Segre-Coset of A & product c1 misses product
c2 & diff(c1,c2)=$1 ex D being FinSequence of bool the carrier of Segre_Product
A st D.1=product c1 & D.(len D)=product c2 & (for i being Nat st i in dom D
holds D.i is Segre-Coset of A) & for i being Nat st 1<=i & i<len D for Di,Di1
being Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||'
Di1;
A5: now
let k be Nat;
assume
A6: P[k];
thus P[k+1]
proof
let c1,c2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A7: indx(c1) = indx(c2) and
A8: product c1 is Segre-Coset of A and
A9: product c2 is Segre-Coset of A and
product c1 misses product c2 and
A10: diff(c1,c2)=k+1;
{i where i is Element of I: c1.i<>c2.i} <> {} by A10;
then consider j0 being object such that
A11: j0 in {i where i is Element of I: c1.i<>c2.i} by XBOOLE_0:def 1;
consider j being Element of I such that
j0=j and
A12: c1.j<>c2.j by A11;
A13: c2.indx(c1)=[#](A.indx(c1)) by A7,A9,Th10;
then
A14: j <> indx(c1) by A8,A12,Th10;
then c1.j is 1-element by PENCIL_1:12;
then consider p being object such that
A15: c1.j={p} by ZFMISC_1:131;
c1 c= Carrier A by PBOOLE:def 18;
then {p} c= (Carrier A).j by A15;
then p in (Carrier A).j by ZFMISC_1:31;
then p in [#](A.j) by Th7;
then reconsider p as Point of A.j;
reconsider c3=c2+*(j,{p}) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by A7,A14,Th13;
A16: c3.indx(c1)=[#](A.indx(c1)) by A13,A14,FUNCT_7:32;
c2.j is 1-element by A7,A14,PENCIL_1:12;
then
A17: ex r being object st c2.j={r} by ZFMISC_1:131;
A.indx(c1) is non trivial by Th2;
then
A18: indx(c3) = indx(c1) by A16,PENCIL_1:def 21;
product c3 is Subset of Segre_Product A by Th14;
then
A19: product c3 is Segre-Coset of A by A16,A18,PENCIL_2:def 2;
per cases;
suppose
A20: product c1 misses product c3;
diff(c1,c2) = diff(c1,c3) + 1 by A12,A15,Th19;
then consider
E being FinSequence of bool the carrier of Segre_Product A
such that
A21: E.1=product c1 and
A22: E.(len E)=product c3 and
A23: for i being Nat st i in dom E holds E.i is Segre-Coset of A and
A24: for i being Nat st 1<=i & i<len E for Ei,Ei1 being
Segre-Coset of A st Ei=E.i & Ei1=E.(i+1) holds Ei misses Ei1 & Ei '||' Ei1 by
A6,A8,A10,A18,A19,A20;
not p in c2.j by A12,A15,A17,TARSKI:def 1;
then consider
F being FinSequence of bool the carrier of Segre_Product A
such that
A25: F.1=product c3 and
A26: F.(len F)=product c2 and
A27: for i being Nat st i in dom F holds F.i is Segre-Coset of A and
A28: for i being Nat st 1<=i & i<len F for Di,Di1 being
Segre-Coset of A st Di=F.i & Di1=F.(i+1) holds Di misses Di1 & Di '||' Di1 by
A1,A9,Th22;
A29: now
dom c2 = I by PARTFUN1:def 2;
then
A30: c3.j = {p} by FUNCT_7:31;
assume len F=1;
hence contradiction by A12,A15,A25,A26,A30,PUA2MSS1:2;
end;
reconsider D = E ^' F as FinSequence of bool the carrier of
Segre_Product A;
take D;
1 in dom E by A21,FUNCT_1:def 2;
then 1 <= len E by FINSEQ_3:25;
hence D.1=product c1 by A21,FINSEQ_6:140;
A31: 1 in dom F by A25,FUNCT_1:def 2;
then 1 <= len F by FINSEQ_3:25;
then
A32: len F > 1 by A29,XXREAL_0:1;
hence D.(len D)=product c2 by A26,FINSEQ_6:142;
thus for i being Nat st i in dom D holds D.i is Segre-Coset of A
proof
let i be Nat;
A33: rng D c= rng E \/ rng F by FINSEQ_6:143;
assume i in dom D;
then
A34: D.i in rng D by FUNCT_1:3;
per cases by A34,A33,XBOOLE_0:def 3;
suppose
D.i in rng E;
then consider i0 being object such that
A35: i0 in dom E and
A36: D.i = E.i0 by FUNCT_1:def 3;
thus thesis by A23,A35,A36;
end;
suppose
D.i in rng F;
then consider i0 being object such that
A37: i0 in dom F and
A38: D.i = F.i0 by FUNCT_1:def 3;
thus thesis by A27,A37,A38;
end;
end;
thus for i being Nat st 1<=i & i<len D for Di,Di1 being Segre-Coset
of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1
proof
let i be Nat;
assume that
A39: 1<=i and
A40: i<len D;
let Di,Di1 be Segre-Coset of A such that
A41: Di=D.i and
A42: Di1=D.(i+1);
reconsider i as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
A43: i<len E;
then i+1 <= len E by NAT_1:13;
then
A44: Di1=E.(i+1) by A42,FINSEQ_6:140,NAT_1:11;
Di=E.i by A39,A41,A43,FINSEQ_6:140;
hence thesis by A24,A39,A43,A44;
end;
suppose
i>=len E;
then consider k being Nat such that
A45: i=len E+k by NAT_1:10;
A46: F <> {} by A31;
reconsider k as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
A47: k>0;
len E + k + 1 < len D + 1 by A40,A45,XREAL_1:6;
then
A48: len E + (k + 1) < len E + len F by A46,FINSEQ_6:139;
then
A49: k+1 < len F by XREAL_1:6;
then
A50: k < len F by NAT_1:13;
Di1=D.(len E + (k + 1)) by A42,A45;
then
A51: Di1=F.((k+1)+1) by A49,FINSEQ_6:141,NAT_1:11;
0+1<=k by A47,NAT_1:13;
then
A52: Di=F.(k+1) by A41,A45,A50,FINSEQ_6:141;
1 <= k+1 & k+1 < len F by A48,NAT_1:11,XREAL_1:6;
hence thesis by A28,A52,A51;
end;
suppose
k=0;
then Di = F.1 & Di1 = F.(1+1) by A22,A25,A32,A39,A41,A42,A45,
FINSEQ_6:140,141;
hence thesis by A28,A32;
end;
end;
end;
end;
suppose
A53: product c1 meets product c3;
not p in c2.j by A12,A15,A17,TARSKI:def 1;
hence thesis by A1,A8,A9,A18,A19,A53,Th11,Th22;
end;
end;
end;
A54: P[ 0 ]
proof
let c1,c2 be Segre-like non trivial-yielding ManySortedSubset of Carrier
A;
assume that
indx(c1)=indx(c2) and
product c1 is Segre-Coset of A and
product c2 is Segre-Coset of A and
A55: product c1 misses product c2 and
A56: diff(c1,c2)=0;
A57: now
let a be object;
assume a in dom c1;
then reconsider j=a as Element of I;
assume c1.a<>c2.a;
then j in {i where i is Element of I: c1.i <> c2.i};
hence contradiction by A56;
end;
dom c1 = I by PARTFUN1:def 2
.= dom c2 by PARTFUN1:def 2;
hence thesis by A55,A57,FUNCT_1:2;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A54,A5);
then
A58: P[diff(b1,b2)];
assume indx(b1)=indx(b2);
then consider
D being FinSequence of bool the carrier of Segre_Product A such
that
A59: D.1=product b1 & D.(len D)=product b2 and
A60: ( for i being Nat st i in dom D holds D.i is Segre-Coset of A)&
for i being Nat st 1<=i & i<len D for Di,Di1 being Segre-Coset of A st Di=D.i &
Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1 by A2,A3,A4,A58;
take D;
thus D.1=B1 & D.(len D)=B2 by A3,A4,A59;
thus thesis by A60;
end;
given D being FinSequence of bool the carrier of Segre_Product A such that
A61: D.1=B1 and
A62: D.(len D)=B2 and
A63: for i being Nat st i in dom D holds D.i is Segre-Coset of A and
A64: for i being Nat st 1<=i & i<len D for Di,Di1 being Segre-Coset of A
st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1;
defpred P[Nat] means for bb being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st product bb = D.$1 holds indx(b1) = indx(bb);
A65: now
let k be Nat;
assume
A66: P[k];
thus P[k+1]
proof
let bb be Segre-like non trivial-yielding ManySortedSubset of Carrier A
such that
A67: product bb = D.(k+1);
A68: k+1 in dom D by A67,FUNCT_1:def 2;
then
A69: k+1 <= len D by FINSEQ_3:25;
per cases;
suppose
k=0;
hence thesis by A3,A61,A67,PUA2MSS1:2;
end;
suppose
0<k;
then 0+1<k+1 by XREAL_1:6;
then
A70: 1<=k by NAT_1:13;
k <= len D by A69,NAT_1:13;
then k in dom D by A70,FINSEQ_3:25;
then reconsider B0=D.k as Segre-Coset of A by A63;
reconsider B3=D.(k+1) as Segre-Coset of A by A63,A68;
consider b0 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A71: B0 = product b0 and
b0.indx(b0)=[#](A.indx(b0)) by PENCIL_2:def 2;
k < len D by A69,NAT_1:13;
then
A72: B0 misses B3 & B0 '||' B3 by A64,A70;
indx(b1) = indx(b0) by A66,A71;
hence thesis by A67,A71,A72,Th21;
end;
end;
end;
A73: P[ 0 ]
proof
A74: not 0 in dom D by FINSEQ_3:24;
let bb be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
assume product bb = D.0;
hence thesis by A74,FUNCT_1:def 2;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A73,A65);
hence thesis by A4,A62;
end;
theorem Th24:
for I being finite 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 f being Collineation of Segre_Product A for B1,B2 being Segre-Coset of A
for b1,b2,b3,b4 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A st B1 = product b1 & B2 = product b2 & f.:B1 = product b3 & f.:B2 =
product b4 holds indx(b1)=indx(b2) implies indx(b3)=indx(b4)
proof
let I be finite 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;
A2: now
let i be Element of I;
A.i is strongly_connected by A1;
hence A.i is connected by Th4;
end;
let f be Collineation of Segre_Product A;
let B1,B2 be Segre-Coset of A;
let b1,b2,b3,b4 be Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A3: B1 = product b1 and
A4: B2 = product b2 and
A5: f.:B1 = product b3 & f.:B2 = product b4;
assume
A6: indx(b1)=indx(b2);
per cases;
suppose
A7: B1 misses B2;
reconsider fB1=f.:B1,fB2=f.:B2 as Segre-Coset of A by A1,PENCIL_2:24;
f is bijective Function of the carrier of Segre_Product A, the
carrier of Segre_Product A by PENCIL_2:def 4;
then
A8: fB1 misses fB2 by A7,FUNCT_1:66;
consider D being FinSequence of bool the carrier of Segre_Product A such
that
A9: D.1=B1 and
A10: D.(len D)=B2 and
A11: for i being Nat st i in dom D holds D.i is Segre-Coset of A and
A12: for i being Nat st 1<=i & i<len D for Di,Di1 being Segre-Coset of
A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1 by A2,A3,A4,A6,A7
,Th23;
deffunc F(Nat)=f.:(D.$1);
consider E being FinSequence of bool the carrier of Segre_Product A such
that
A13: len E = len D & for j being Nat st j in dom E holds E.j = F(j)
from FINSEQ_2:sch 1;
A14: dom E = Seg len D by A13,FINSEQ_1:def 3;
A15: for i being Nat st 1<=i & i<len E for Ei,Ei1 being Segre-Coset of A
st Ei=E.i & Ei1=E.(i+1) holds Ei misses Ei1 & Ei '||' Ei1
proof
let i be Nat;
A16: f is bijective Function of the carrier of Segre_Product A, the
carrier of Segre_Product A by PENCIL_2:def 4;
assume
A17: 1<=i & i<len E;
then i in dom D by A13,FINSEQ_3:25;
then reconsider Di=D.i as Segre-Coset of A by A11;
1<=i+1 & i+1 <= len E by A17,NAT_1:13;
then i+1 in dom D by A13,FINSEQ_3:25;
then reconsider Di1=D.(i+1) as Segre-Coset of A by A11;
let Ei,Ei1 be Segre-Coset of A;
assume that
A18: Ei=E.i and
A19: Ei1=E.(i+1);
i in Seg len D by A13,A17,FINSEQ_1:1;
then
A20: Ei=f.:(D.i) by A13,A14,A18;
1<=i+1 & i+1 <= len E by A17,NAT_1:13;
then i+1 in Seg len D by A13,FINSEQ_1:1;
then
A21: Ei1=f.:(D.(i+1)) by A13,A14,A19;
Di misses Di1 by A12,A13,A17;
hence Ei misses Ei1 by A20,A21,A16,FUNCT_1:66;
Di '||' Di1 by A12,A13,A17;
hence thesis by A20,A21,Th20;
end;
A22: for i being Nat st i in dom E holds E.i is Segre-Coset of A
proof
let i be Nat;
assume
A23: i in dom E;
then i in Seg len D by A13,FINSEQ_1:def 3;
then i in dom D by FINSEQ_1:def 3;
then reconsider di=D.i as Segre-Coset of A by A11;
E.i = f.:di by A13,A23;
hence thesis by A1,PENCIL_2:24;
end;
len E in dom D by A4,A10,A13,FUNCT_1:def 2;
then len E in Seg len D by FINSEQ_1:def 3;
then
A24: E.(len E) = f.:B2 by A10,A13,A14;
1 in dom D by A3,A9,FUNCT_1:def 2;
then 1 in Seg len D by FINSEQ_1:def 3;
then E.1 = f.:B1 by A9,A13,A14;
hence thesis by A2,A5,A24,A22,A15,A8,Th23;
end;
suppose
B1 meets B2;
then B1=B2 by A3,A4,A6,Th11;
hence thesis by A5,PUA2MSS1:2;
end;
end;
theorem Th25:
for I being finite 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 f being Collineation of Segre_Product A ex s being Permutation of I st for
i,j being Element of I holds s.i=j iff for B1 being Segre-Coset of A for b1,b2
being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 =
product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j
proof
let I be finite non empty set;
let A be PLS-yielding ManySortedSet of I;
assume
A1: for i be Element of I holds A.i is strongly_connected;
let f be Collineation of Segre_Product A;
defpred P[set,set] means for B1 being Segre-Coset of A for b1,b2 being
Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 = product
b1 & f.:B1 = product b2 holds indx(b1)=$1 implies indx(b2)=$2;
A2: for x,y,x9 being Element of I st P[x,y] & P[x9,y] holds x=x9
proof
reconsider ff=f" as Collineation of Segre_Product A by PENCIL_2:13;
let x,y,x9 be Element of I;
assume that
A3: for B1 being Segre-Coset of A for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 =
product b2 holds indx(b1)=x implies indx(b2)=y and
A4: for B1 being Segre-Coset of A for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 =
product b2 holds indx(b1)=x9 implies indx(b2)=y;
consider b1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A5: indx(b1) = x and
A6: product b1 is Segre-Coset of A by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A6;
reconsider fB1=f.:B1 as Segre-Coset of A by A1,PENCIL_2:24;
consider L1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A7: fB1 = product L1 and
L1.indx(L1) = [#](A.indx(L1)) by PENCIL_2:def 2;
consider b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A8: indx(b2) = x9 and
A9: product b2 is Segre-Coset of A by Th8;
reconsider B2 = product b2 as Segre-Coset of A by A9;
reconsider fB2=f.:B2 as Segre-Coset of A by A1,PENCIL_2:24;
consider L2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A10: fB2 = product L2 and
L2.indx(L2) = [#](A.indx(L2)) by PENCIL_2:def 2;
A11: indx(L2)=y by A4,A8,A10;
A12: f is bijective by PENCIL_2:def 4;
A13: ff = (f qua Function)" by A12,TOPS_2:def 4;
then
A14: ff.:fB2 = f"fB2 by A12,FUNCT_1:85;
A15: ff.:fB1 = f"fB1 by A12,A13,FUNCT_1:85;
dom f = the carrier of Segre_Product A by FUNCT_2:def 1;
then
A16: B2 c= ff.:fB2 by A14,FUNCT_1:76;
ff.:fB2 c= B2 by A12,A14,FUNCT_1:82;
then
A17: B2=ff.:fB2 by A16;
dom f = the carrier of Segre_Product A by FUNCT_2:def 1;
then
A18: B1 c= ff.:fB1 by A15,FUNCT_1:76;
ff.:fB1 c= B1 by A12,A15,FUNCT_1:82;
then
A19: B1=ff.:fB1 by A18;
indx(L1)=y by A3,A5,A7;
hence thesis by A1,A5,A7,A8,A10,A11,A19,A17,Th24;
end;
A20: for y being Element of I ex x being Element of I st P[x,y]
proof
set p0 = the Point of Segre_Product A;
reconsider p0 as Element of Carrier A by Th6;
let x be Element of I;
reconsider p={p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
dom A = I by PARTFUN1:def 2;
then A.x in rng A by FUNCT_1:3;
then A.x is non trivial by PENCIL_1:def 18;
then reconsider C=[#](A.x) as non trivial set;
reconsider b=p+*(x,C) as Segre-like non trivial-yielding ManySortedSubset
of Carrier A by PENCIL_1:9,10,PENCIL_2:7;
dom p=I by PARTFUN1:def 2;
then
A21: b.x = C by FUNCT_7:31;
then
A22: indx(b)=x by PENCIL_1:def 21;
product b c= the carrier of Segre_Product A
proof
let a be object;
assume a in product b;
then consider f being Function such that
A23: a=f and
A24: dom f=dom b and
A25: for x being object st x in dom b holds f.x in b.x by CARD_3:def 5;
dom Carrier A = I by PARTFUN1:def 2;
then
A26: dom f = dom Carrier A by A24,PARTFUN1:def 2;
A27: now
let i be object;
assume
A28: i in dom Carrier A;
then reconsider i1=i as Element of I;
A29: f.i in b.i by A24,A25,A26,A28;
per cases;
suppose
i1=x;
hence f.i in (Carrier A).i by A21,A29,Th7;
end;
suppose
i1<>x;
then f.i1 in p.i1 by A29,FUNCT_7:32;
then f.i1 in {p0.i1} by PZFMISC1:def 1;
then f.i1 = p0.i1 by TARSKI:def 1;
then
A30: f.i1 is Element of (Carrier A).i1 by PBOOLE:def 14;
[#](A.i1) is non empty;
then (Carrier A).i1 is non empty by Th7;
hence f.i in (Carrier A).i by A30;
end;
end;
Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by
PENCIL_1:def 23;
hence thesis by A23,A26,A27,CARD_3:def 5;
end;
then reconsider B=product b as Segre-Coset of A by A21,A22,PENCIL_2:def 2;
reconsider fB=f"B as Segre-Coset of A by A1,PENCIL_2:25;
consider b0 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A31: fB = product b0 and
b0.indx(b0)=[#](A.indx(b0)) by PENCIL_2:def 2;
take y=indx(b0);
let B1 being Segre-Coset of A;
let b1,b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A;
f is bijective by PENCIL_2:def 4;
then rng f = the carrier of Segre_Product A by FUNCT_2:def 3;
then
A32: f.:fB = product b by FUNCT_1:77;
assume B1 = product b1 & f.:B1 = product b2 & indx(b1)=y;
hence thesis by A1,A22,A31,A32,Th24;
end;
A33: for x being Element of I ex y being Element of I st P[x,y]
proof
set p0 = the Point of Segre_Product A;
reconsider p0 as Element of Carrier A by Th6;
let x be Element of I;
reconsider p={p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
dom A = I by PARTFUN1:def 2;
then A.x in rng A by FUNCT_1:3;
then A.x is non trivial by PENCIL_1:def 18;
then reconsider C=[#](A.x) as non trivial set;
reconsider b=p+*(x,C) as Segre-like non trivial-yielding ManySortedSubset
of Carrier A by PENCIL_1:9,10,PENCIL_2:7;
dom p=I by PARTFUN1:def 2;
then
A34: b.x = C by FUNCT_7:31;
then
A35: indx(b)=x by PENCIL_1:def 21;
product b c= the carrier of Segre_Product A
proof
let a be object;
assume a in product b;
then consider f being Function such that
A36: a=f and
A37: dom f=dom b and
A38: for x being object st x in dom b holds f.x in b.x by CARD_3:def 5;
dom Carrier A = I by PARTFUN1:def 2;
then
A39: dom f = dom Carrier A by A37,PARTFUN1:def 2;
A40: now
let i be object;
assume
A41: i in dom Carrier A;
then reconsider i1=i as Element of I;
A42: f.i in b.i by A37,A38,A39,A41;
per cases;
suppose
i1=x;
hence f.i in (Carrier A).i by A34,A42,Th7;
end;
suppose
i1<>x;
then f.i1 in p.i1 by A42,FUNCT_7:32;
then f.i1 in {p0.i1} by PZFMISC1:def 1;
then f.i1 = p0.i1 by TARSKI:def 1;
then
A43: f.i1 is Element of (Carrier A).i1 by PBOOLE:def 14;
[#](A.i1) is non empty;
then (Carrier A).i1 is non empty by Th7;
hence f.i in (Carrier A).i by A43;
end;
end;
Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by
PENCIL_1:def 23;
hence thesis by A36,A39,A40,CARD_3:def 5;
end;
then reconsider B=product b as Segre-Coset of A by A34,A35,PENCIL_2:def 2;
reconsider fB=f.:B as Segre-Coset of A by A1,PENCIL_2:24;
consider b0 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A44: fB = product b0 and
b0.indx(b0)=[#](A.indx(b0)) by PENCIL_2:def 2;
take indx(b0);
let B1 being Segre-Coset of A;
let b1,b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A;
assume B1 = product b1 & f.:B1 = product b2 & indx(b1)=x;
hence thesis by A1,A35,A44,Th24;
end;
A45: for x,y,y9 being Element of I st P[x,y] & P[x,y9] holds y=y9
proof
let x,y,y9 be Element of I;
assume that
A46: for B1 being Segre-Coset of A for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 =
product b2 holds indx(b1)=x implies indx(b2)=y and
A47: for B1 being Segre-Coset of A for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 =
product b2 holds indx(b1)=x implies indx(b2)=y9;
consider b1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A48: indx(b1) = x and
A49: product b1 is Segre-Coset of A by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A49;
reconsider fB1=f.:B1 as Segre-Coset of A by A1,PENCIL_2:24;
consider L1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A50: fB1 = product L1 and
L1.indx(L1) = [#](A.indx(L1)) by PENCIL_2:def 2;
indx(L1)=y by A46,A48,A50;
hence thesis by A47,A48,A50;
end;
thus ex f being Permutation of I st for x,y being Element of I holds f.x=y
iff P[x,y] from TRANSGEO:sch 1(A33,A20,A2,A45);
end;
definition
let I be finite 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 f be Collineation of Segre_Product A;
func permutation_of_indices(f) -> Permutation of I means
:Def3:
for i,j
being Element of I holds it.i=j iff for B1 being Segre-Coset of A for b1,b2
being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 =
product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j;
existence by A1,Th25;
uniqueness
proof
let s,t be Permutation of I such that
A2: for i,j being Element of I holds s.i=j iff for B1 being
Segre-Coset of A for b1,b2 being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 = product b2 holds
indx(b1)=i implies indx(b2)=j and
A3: for i,j being Element of I holds t.i=j iff for B1 being
Segre-Coset of A for b1,b2 being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 = product b2 holds
indx(b1)=i implies indx(b2)=j;
A4: now
let a be object;
assume a in I;
then reconsider i=a as Element of I;
reconsider j2=t.i as Element of I;
reconsider j1=s.i as Element of I;
consider b1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A5: indx(b1)=i and
A6: product b1 is Segre-Coset of A by Th8;
reconsider B1=product b1 as Segre-Coset of A by A6;
reconsider fB=f.:B1 as Segre-Coset of A by A1,PENCIL_2:24;
consider b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A7: fB = product b2 and
b2.indx(b2) = [#](A.indx(b2)) by PENCIL_2:def 2;
j1 = indx(b2) by A2,A5,A7
.= j2 by A3,A5,A7;
hence s.a=t.a;
end;
thus s=t by A4;
end;
end;
begin :: Canonical embeddings and automorphisms of Segre product
definition
let I be finite 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 f be Collineation of Segre_Product A;
let b1 be Segre-like non trivial-yielding ManySortedSubset of Carrier A such
that
A2: product b1 is Segre-Coset of A;
func canonical_embedding(f,b1) -> Function of A.indx(b1),A.(
permutation_of_indices(f).indx(b1)) means
:Def4:
it is isomorphic & for a being
ManySortedSet of I st a is Point of Segre_Product A & a in product b1 for b
being ManySortedSet of I st b=f.a holds b.(permutation_of_indices(f).indx(b1))=
it.(a.indx(b1));
existence
proof
reconsider B1=product b1 as Segre-Coset of A by A2;
set s=permutation_of_indices(f);
set i=indx(b1);
defpred P[object,object] means
for J being ManySortedSet of I st J in f.:(
product(b1+*(i,{$1}))) holds $2 = J.(s.i);
set B = the carrier of A.i;
set t=s;
reconsider B2=f.:B1 as Segre-Coset of A by A1,PENCIL_2:24;
consider b2 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A3: product b2=B2 and
A4: b2.indx(b2) = [#](A.indx(b2)) by PENCIL_2:def 2;
set j=indx(b2);
A5: f is bijective by PENCIL_2:def 4;
then
A6: f"B2 c= B1 by FUNCT_1:82;
A7: Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by
PENCIL_1:def 23;
A8: for x being object st x in B ex y being object st P[x,y]
proof
let x be object;
consider bb being object such that
A9: bb in B1 by XBOOLE_0:def 1;
A10: ex bf being Function st bf=bb & dom bf=dom b1 &
for o being object st o
in dom b1 holds bf.o in b1.o by A9,CARD_3:def 5;
A11: dom b1=I by PARTFUN1:def 2;
then reconsider bb as ManySortedSet of I by A10,PARTFUN1:def 2
,RELAT_1:def 18;
set bbx=bb+*(i,x);
A12: {bbx qua set} = product(b1+*(i,{x}))
proof
thus {bbx qua set} c= product(b1+*(i,{x}))
proof
A13: now
let z be object;
assume z in dom (b1+*(i,{x}));
then
A14: z in I;
then
A15: z in dom bb by PARTFUN1:def 2;
per cases;
suppose
A16: z=i;
then bbx.z = x by A15,FUNCT_7:31;
then bbx.z in {x} by TARSKI:def 1;
hence bbx.z in (b1+*(i,{x})).z by A11,A16,FUNCT_7:31;
end;
suppose
A17: z<>i;
then bbx.z = bb.z by FUNCT_7:32;
then bbx.z in b1.z by A9,A11,A14,CARD_3:9;
hence bbx.z in (b1+*(i,{x})).z by A17,FUNCT_7:32;
end;
end;
let o be object;
assume o in {bbx qua set};
then
A18: o = bbx by TARSKI:def 1;
dom bbx = I by PARTFUN1:def 2
.= dom (b1+*(i,{x})) by PARTFUN1:def 2;
hence thesis by A18,A13,CARD_3:9;
end;
let o be object;
assume o in product(b1+*(i,{x}));
then consider u being Function such that
A19: u=o and
A20: dom u=dom (b1+*(i,{x})) and
A21: for z being object st z in dom (b1+*(i,{x})) holds u.z in (b1+*(
i,{x}) ).z by CARD_3:def 5;
A22: now
let z be object;
assume
A23: z in dom u;
then
A24: z in I by A20;
reconsider zz=z as Element of I by A20,A23;
A25: u.z in (b1+*(i,{x})).z by A20,A21,A23;
per cases;
suppose
A26: zz=i;
then u.z in {x} by A11,A25,FUNCT_7:31;
then u.z = x by TARSKI:def 1;
hence u.z = bbx.z by A10,A11,A26,FUNCT_7:31;
end;
suppose
A27: zz<>i;
then b1.zz is non empty trivial by PENCIL_1:def 21;
then b1.zz is 1-element;
then consider o being object such that
A28: b1.z = {o} by ZFMISC_1:131;
u.z in b1.z by A25,A27,FUNCT_7:32;
then
A29: u.z = o by A28,TARSKI:def 1;
bbx.z = bb.z by A27,FUNCT_7:32;
then bbx.z in {o} by A10,A11,A24,A28;
hence u.z = bbx.z by A29,TARSKI:def 1;
end;
end;
dom u = I by A20,PARTFUN1:def 2
.= dom bbx by PARTFUN1:def 2;
then u=bbx by A22;
hence thesis by A19,TARSKI:def 1;
end;
assume
A30: x in B;
A31: now
let o be object;
assume
A32: o in dom Carrier A;
then reconsider u=o as Element of I;
per cases;
suppose
A33: u=i;
then bbx.u in [#](A.i) by A30,A10,A11,FUNCT_7:31;
hence bbx.o in (Carrier A).o by A33,Th7;
end;
suppose
A34: u<>i;
b1 c= Carrier A by PBOOLE:def 18;
then
A35: b1.o c= (Carrier A).o by A32;
bbx.u = bb.u by A34,FUNCT_7:32;
then bbx.u in b1.u by A9,A11,CARD_3:9;
hence bbx.o in (Carrier A).o by A35;
end;
end;
dom bbx= I by PARTFUN1:def 2
.= dom Carrier A by PARTFUN1:def 2;
then reconsider bbx1=bbx as Point of Segre_Product A by A7,A31,CARD_3:9;
reconsider fbbx=f.bbx1 as ManySortedSet of I by PENCIL_1:14;
take fbbx.(s.i);
dom f = the carrier of Segre_Product A by FUNCT_2:def 1;
then bbx1 in dom f;
then
A36: Im(f,bbx) = {f.bbx} by FUNCT_1:59;
let J be ManySortedSet of I;
assume J in f.:product(b1+*(i,{x}));
hence thesis by A12,A36,TARSKI:def 1;
end;
consider M being Function such that
A37: dom M = B & for x being object st x in B holds P[x,M.x] from
CLASSES1:sch 1(A8);
A38: dom f = the carrier of Segre_Product A by FUNCT_2:def 1;
then B1 c= f"B2 by FUNCT_1:76;
then
A39: f"B2 = B1 by A6;
rng M c= the carrier of A.(t.i)
proof
let x be object;
assume x in rng M;
then consider o being object such that
A40: o in dom M and
A41: x=M.o by FUNCT_1:def 3;
reconsider o as Point of A.i by A37,A40;
consider p being ManySortedSet of I such that
A42: p in product b1 and
A43: {p+*(i,o) qua set} = product(b1+*(i,{o})) by Th18;
reconsider pio=p+*(i,o) as Point of Segre_Product A by A2,A42,PENCIL_1:25
;
reconsider J=f.pio as ManySortedSet of I by PENCIL_1:14;
Im(f,p+*(i,o)) = {f.pio} by A38,FUNCT_1:59;
then
A44: J in f.:(product(b1+*(i,{o}))) by A43,TARSKI:def 1;
s.i in I;
then s.i in dom Carrier A by PARTFUN1:def 2;
then J.(s.i) in (Carrier A).(s.i) by A7,CARD_3:9;
then J.(s.i) in [#](A.(s.i)) by Th7;
hence thesis by A37,A41,A44;
end;
then reconsider M as Function of A.i,A.(t.i) by A37,FUNCT_2:def 1
,RELSET_1:4;
set m=M;
A45: indx(b2)=s.i by A1,A3,Def3;
A46: m is one-to-one
proof
let x1,x2 be object;
assume that
A47: x1 in dom m & x2 in dom m and
A48: m.x1 = m.x2;
reconsider o1=x1,o2=x2 as Point of A.i by A47;
consider p1 being ManySortedSet of I such that
A49: p1 in product b1 and
A50: {p1+*(i,o1) qua set} = product(b1+*(i,{o1})) by Th18;
reconsider p1io=p1+*(i,o1) as Point of Segre_Product A by A2,A49,
PENCIL_1:25;
reconsider J1=f.p1io as ManySortedSet of I by PENCIL_1:14;
consider p2 being ManySortedSet of I such that
A51: p2 in product b1 and
A52: {p2+*(i,o2) qua set} = product(b1+*(i,{o2})) by Th18;
A53: dom b1=I by PARTFUN1:def 2;
A54: dom p1=I by PARTFUN1:def 2;
A55: now
let o be object;
assume
A56: o in I;
per cases;
suppose
A57: o=indx(b1);
then p1+*(i,o1).o = o1 by A54,FUNCT_7:31;
then p1+*(i,o1).o in [#](A.i);
hence p1+*(i,o1).o in b1.o by A2,A57,Th10;
end;
suppose
o<>indx(b1);
then p1+*(i,o1).o = p1.o by FUNCT_7:32;
hence p1+*(i,o1).o in b1.o by A49,A53,A56,CARD_3:9;
end;
end;
dom (p1+*(i,o1))=I by PARTFUN1:def 2;
then p1io in product b1 by A53,A55,CARD_3:9;
then
A58: J1 in B2 by A38,FUNCT_1:def 6;
reconsider p2io=p2+*(i,o2) as Point of Segre_Product A by A2,A51,
PENCIL_1:25;
reconsider J2=f.p2io as ManySortedSet of I by PENCIL_1:14;
Im(f,p2+*(i,o2)) = {f.p2io} by A38,FUNCT_1:59;
then J2 in f.:(product(b1+*(i,{o2}))) by A52,TARSKI:def 1;
then
A59: M.o2 = J2.(s.i) by A37;
dom p1 = I by PARTFUN1:def 2;
then
A60: p1+*(i,o1).i = o1 by FUNCT_7:31;
A61: dom b1=I by PARTFUN1:def 2;
A62: dom p2=I by PARTFUN1:def 2;
A63: now
let o be object;
assume
A64: o in I;
per cases;
suppose
A65: o=indx(b1);
then p2+*(i,o2).o = o2 by A62,FUNCT_7:31;
then p2+*(i,o2).o in [#](A.i);
hence p2+*(i,o2).o in b1.o by A2,A65,Th10;
end;
suppose
o<>indx(b1);
then p2+*(i,o2).o = p2.o by FUNCT_7:32;
hence p2+*(i,o2).o in b1.o by A51,A61,A64,CARD_3:9;
end;
end;
dom (p2+*(i,o2))=I by PARTFUN1:def 2;
then p2io in product b1 by A61,A63,CARD_3:9;
then
A66: J2 in B2 by A38,FUNCT_1:def 6;
Im(f,p1+*(i,o1)) = {f.p1io} by A38,FUNCT_1:59;
then
A67: J1 in f.:(product(b1+*(i,{o1}))) by A50,TARSKI:def 1;
A68: now
let o be object;
assume o in I;
then reconsider l=o as Element of I;
per cases;
suppose
l=indx(b2);
hence J1.o=J2.o by A45,A37,A48,A67,A59;
end;
suppose
l<>indx(b2);
hence J1.o=J2.o by A3,A58,A66,PENCIL_1:23;
end;
end;
dom p2 = I by PARTFUN1:def 2;
then
A69: p2+*(i,o2).i = o2 by FUNCT_7:31;
J1=J2 by A68;
hence thesis by A38,A5,A60,A69,FUNCT_1:def 4;
end;
f is bijective by PENCIL_2:def 4;
then
A70: rng f = the carrier of Segre_Product A by FUNCT_2:def 3;
A71: f" = (f qua Function)" by A5,TOPS_2:def 4;
the carrier of A.(t.i) c= rng m
proof
let x be object;
assume x in the carrier of A.(t.i);
then reconsider x1=x as Point of A.(t.i);
consider p0 being ManySortedSet of I such that
A72: p0 in product b2 and
{p0+*(indx(b2),x1) qua set} = product(b2+*(indx(b2),{x1})) by A45,Th18;
reconsider p=p0+*(indx(b2),x1) as Point of Segre_Product A by A3,A45,A72,
PENCIL_1:25;
reconsider p1=p as ManySortedSet of I;
reconsider q=f".p as ManySortedSet of I by PENCIL_1:14;
A73: p=f.(f".p) by A70,A5,A71,FUNCT_1:35;
A74: dom b1=I by PARTFUN1:def 2;
A75: now
let o be object;
assume o in I;
then reconsider l=o as Element of I;
per cases;
suppose
l=i;
then b1+*(i,{q.i}).l = {q.o} by A74,FUNCT_7:31;
hence q.o in b1+*(i,{q.i}).o by TARSKI:def 1;
end;
suppose
l<>i;
then
A76: b1+*(i,{q.i}).l = b1.l by FUNCT_7:32;
A77: dom b2 = I by PARTFUN1:def 2;
A78: dom p0 = I by PARTFUN1:def 2;
A79: now
let o be object;
assume
A80: o in I;
per cases;
suppose
A81: o=indx(b2);
then p1.o = x1 by A78,FUNCT_7:31;
then p1.o in the carrier of A.(t.i);
hence p1.o in b2.o by A1,A3,A4,A81,Def3;
end;
suppose
o<>indx(b2);
then p1.o = p0.o by FUNCT_7:32;
hence p1.o in b2.o by A72,A77,A80,CARD_3:9;
end;
end;
dom p1 = I by PARTFUN1:def 2;
then p in product b2 by A77,A79,CARD_3:9;
then consider q0 being object such that
A82: q0 in dom f and
A83: q0 in B1 and
A84: p=f.q0 by A3,FUNCT_1:def 6;
q=q0 by A38,A5,A73,A82,A84,FUNCT_1:def 4;
hence q.o in b1+*(i,{q.i}).o by A74,A76,A83,CARD_3:9;
end;
end;
I = dom Carrier A by PARTFUN1:def 2;
then q.i in (Carrier A).i by A7,CARD_3:9;
then
A85: q.i in [#](A.i) by Th7;
dom q = I & dom (b1+*(i,{q.i})) = I by PARTFUN1:def 2;
then q in product(b1+*(i,{q.i})) by A75,CARD_3:9;
then p0+*(indx(b2),x1) in f.:(product(b1+*(i,{q.i}))) by A38,A73,
FUNCT_1:def 6;
then dom p0 = I & m.(q.i) = p0+*(indx(b2),x1).(s.i) by A37,A85,
PARTFUN1:def 2;
then dom m = the carrier of A.i & m.(q.i)=x by A45,FUNCT_2:def 1
,FUNCT_7:31;
hence thesis by A85,FUNCT_1:3;
end;
then
A86: rng m = the carrier of A.(t.i);
then m is onto by FUNCT_2:def 3;
then
A87: m" = (m qua Function)" by A46,TOPS_2:def 4;
A88: m" is open
proof
let S0 be Subset of A.(t.i);
assume S0 is open;
then reconsider S=S0 as Block of A.(t.i) by PRE_TOPC:def 2;
reconsider L=product(b2+*(j,S)) as Block of Segre_Product A by A45,Th12;
reconsider K=f"L as Block of Segre_Product A;
consider k being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A89: K = product k and
A90: k.indx(k) is Block of A.indx(k) by PENCIL_1:24;
A91: dom b2 = I by PARTFUN1:def 2;
A92: now
let x be object;
assume x in I;
per cases;
suppose
A93: x=j;
then b2+*(j,S).x = S by A91,FUNCT_7:31;
then b2+*(j,S).x c= the carrier of A.(t.i);
hence b2+*(j,S).x c= b2.x by A1,A3,A4,A93,Def3;
end;
suppose
x<>j;
hence b2+*(j,S).x c= b2.x by FUNCT_7:32;
end;
end;
dom (b2+*(j,S)) = I by PARTFUN1:def 2;
then L c= product b2 by A91,A92,CARD_3:27;
then product b1 /\ product k = K by A3,A39,A89,RELAT_1:143,XBOOLE_1:28;
then
A94: 2 c= card(product b1 /\ product k) by PENCIL_1:def 6;
then
A95: indx(k)=i by PENCIL_1:26;
m"S=k.indx(k)
proof
thus m"S c= k.indx(k)
proof
let o be object;
A96: dom b2 = I by PARTFUN1:def 2;
assume
A97: o in m"S;
then reconsider u=o as Point of A.i;
consider p being ManySortedSet of I such that
A98: p in product b1 and
A99: {p+*(i,u) qua set} = product(b1+*(i,{u})) by Th18;
reconsider q=p+*(i,u) as Point of Segre_Product A by A2,A98,
PENCIL_1:25;
reconsider fq=f.q as ManySortedSet of I by PENCIL_1:14;
Im(f,p+*(i,u)) = {f.q} by A38,FUNCT_1:59;
then
A100: fq in f.:product(b1+*(i,{u})) by A99,TARSKI:def 1;
product(b1+*(i,{u})) c= product b1
proof
let a be object;
A101: dom b1 = I by PARTFUN1:def 2;
assume a in product(b1+*(i,{u}));
then consider g being Function such that
A102: a=g and
A103: dom g=dom (b1+*(i,{u})) and
A104: for o being object st o in dom (b1+*(i,{u})) holds g.o in
b1+*(i,{u}) .o by CARD_3:def 5;
A105: dom g = I by A103,PARTFUN1:def 2;
now
let o be object;
assume o in I;
then
A106: g.o in b1+*(i,{u}).o by A103,A104,A105;
per cases;
suppose
A107: o=i;
then g.o in {u} by A101,A106,FUNCT_7:31;
then g.o in [#](A.i);
hence g.o in b1.o by A2,A107,Th10;
end;
suppose
o<>i;
hence g.o in b1.o by A106,FUNCT_7:32;
end;
end;
hence thesis by A102,A105,A101,CARD_3:9;
end;
then
A108: f.:product(b1+*(i,{u})) c= product b2 by A3,RELAT_1:123;
m.o in S by A97,FUNCT_1:def 7;
then
A109: fq.(s.i) in S by A37,A100;
A110: now
let o be object;
assume
A111: o in I;
per cases;
suppose
o=j;
hence fq.o in b2+*(j,S).o by A45,A109,A96,FUNCT_7:31;
end;
suppose
o<>j;
then b2+*(j,S).o = b2.o by FUNCT_7:32;
hence fq.o in b2+*(j,S).o by A100,A108,A96,A111,CARD_3:9;
end;
end;
dom fq = I & dom (b2+*(j,S)) = I by PARTFUN1:def 2;
then fq in L by A110,CARD_3:9;
then dom k = I & q in K by A38,FUNCT_1:def 7,PARTFUN1:def 2;
then dom p = I & p+*(i,u).i in k.i by A89,CARD_3:9,PARTFUN1:def 2;
hence thesis by A95,FUNCT_7:31;
end;
let o be object;
assume
A112: o in k.indx(k);
k.indx(k) in the topology of A.i by A90,A95;
then reconsider u=o as Point of A.i by A112;
consider p0 being ManySortedSet of I such that
A113: p0 in product b1 and
A114: {p0+*(i,u) qua set} = product(b1+*(i,{u})) by Th18;
reconsider p=p0+*(i,u) as Point of Segre_Product A by A2,A113,
PENCIL_1:25;
reconsider fp=f.p as ManySortedSet of I by PENCIL_1:14;
A115: dom b1 = I by PARTFUN1:def 2;
A116: dom p0 = I by PARTFUN1:def 2;
A117: now
let a be object;
assume
A118: a in I;
per cases;
suppose
a=i;
hence p0+*(i,u).a in k.a by A95,A112,A116,FUNCT_7:31;
end;
suppose
A119: a<>i;
then p0+*(i,u).a = p0.a by FUNCT_7:32;
then p0+*(i,u).a in b1.a by A113,A115,A118,CARD_3:9;
hence p0+*(i,u).a in k.a by A94,A119,PENCIL_1:26;
end;
end;
dom (p0+*(i,u)) = I & dom k = I by PARTFUN1:def 2;
then p in K by A89,A117,CARD_3:9;
then dom (b2+*(j,S)) = I & fp in L by FUNCT_1:def 7,PARTFUN1:def 2;
then dom b2 = I & fp.j in b2+*(j,S).j by CARD_3:9,PARTFUN1:def 2;
then
A120: fp.(s.i) in S by A45,FUNCT_7:31;
Im(f,p0+*(i,u)) = {f.p} by A38,FUNCT_1:59;
then fp in f.:product(b1+*(i,{u})) by A114,TARSKI:def 1;
then m.u = fp.(s.i) by A37;
hence thesis by A37,A120,FUNCT_1:def 7;
end;
then m".:S is Block of A.i by A46,A87,A90,A95,FUNCT_1:85;
hence thesis by PRE_TOPC:def 2;
end;
A121: m is open
proof
let S0 be Subset of A.i;
assume S0 is open;
then reconsider S=S0 as Block of A.i by PRE_TOPC:def 2;
reconsider L=product(b1+*(i,S)) as Block of Segre_Product A by Th12;
reconsider K=f.:L as Block of Segre_Product A;
consider k being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A122: K = product k and
A123: k.indx(k) is Block of A.indx(k) by PENCIL_1:24;
A124: dom b1 = I by PARTFUN1:def 2;
A125: now
let x be object;
assume x in I;
per cases;
suppose
A126: x=i;
then b1+*(i,S).x = S by A124,FUNCT_7:31;
then b1+*(i,S).x c= [#](A.i);
hence b1+*(i,S).x c= b1.x by A2,A126,Th10;
end;
suppose
x<>i;
hence b1+*(i,S).x c= b1.x by FUNCT_7:32;
end;
end;
dom (b1+*(i,S)) = I by PARTFUN1:def 2;
then
A127: L c= product b1 by A124,A125,CARD_3:27;
then product b2 /\ product k = K by A3,A122,RELAT_1:123,XBOOLE_1:28;
then 2 c= card(product b2 /\ product k) by PENCIL_1:def 6;
then
A128: indx(k)=t.i by A45,PENCIL_1:26;
A129: dom k = I by PARTFUN1:def 2;
m.:S=k.indx(k)
proof
thus m.:S c= k.indx(k)
proof
let o be object;
A130: dom b1 = I by PARTFUN1:def 2;
assume o in m.:S;
then consider u being object such that
A131: u in dom m and
A132: u in S and
A133: o=m.u by FUNCT_1:def 6;
reconsider u as Point of A.i by A131;
consider p0 being ManySortedSet of I such that
A134: p0 in product b1 and
A135: {p0+*(indx(b1),u) qua set} = product(b1+*(indx(b1),{u})) by Th18;
reconsider p=p0+*(indx(b1),u) as Point of Segre_Product A by A2,A134,
PENCIL_1:25;
reconsider q=f.p as ManySortedSet of I by PENCIL_1:14;
Im(f,p0+*(indx(b1),u)) = {f.p} by A38,FUNCT_1:59;
then q in f.:product(b1+*(indx(b1),{u})) by A135,TARSKI:def 1;
then
A136: m.u = q.(s.i) by A37;
A137: dom p0 = I by PARTFUN1:def 2;
A138: now
let a be object;
assume
A139: a in I;
per cases;
suppose
A140: a=i;
then p0+*(i,u).a = u by A137,FUNCT_7:31;
hence p0+*(i,u).a in b1+*(i,S).a by A132,A130,A140,FUNCT_7:31;
end;
suppose
A141: a<>i;
then p0+*(i,u).a = p0.a by FUNCT_7:32;
then p0+*(i,u).a in b1.a by A134,A130,A139,CARD_3:9;
hence p0+*(i,u).a in b1+*(i,S).a by A141,FUNCT_7:32;
end;
end;
dom (p0+*(i,u)) = I & dom (b1+*(i,S)) = I by PARTFUN1:def 2;
then p in L by A138,CARD_3:9;
then q in product k by A38,A122,FUNCT_1:def 6;
hence thesis by A129,A128,A133,A136,CARD_3:9;
end;
let o be object;
assume
A142: o in k.indx(k);
k.indx(k) in the topology of A.(s.i) by A123,A128;
then reconsider u=o as Point of A.(s.i) by A142;
consider p0 being ManySortedSet of I such that
A143: p0 in product k and
{p0+*(s.i,u) qua set} = product(k+*(s.i,{u})) by A128,Th18;
K in the topology of Segre_Product A;
then reconsider
p=p0+*(s.i,u) as Point of Segre_Product A by A122,A143,PENCIL_1:25;
reconsider q=f".p as ManySortedSet of I by PENCIL_1:14;
A144: dom k = I by PARTFUN1:def 2;
A145: dom p0 = I by PARTFUN1:def 2;
A146: now
let z be object;
assume
A147: z in I;
per cases;
suppose
z=s.i;
hence p0+*(s.i,u).z in k.z by A128,A142,A145,FUNCT_7:31;
end;
suppose
z<>s.i;
then p0+*(s.i,u).z = p0.z by FUNCT_7:32;
hence p0+*(s.i,u).z in k.z by A143,A144,A147,CARD_3:9;
end;
end;
A148: p=f.q by A70,A5,A71,FUNCT_1:35;
dom (p0+*(s.i,u)) = I by PARTFUN1:def 2;
then p in f.:L by A122,A144,A146,CARD_3:9;
then ex qq being object st qq in dom f & qq in L & p=f.qq
by FUNCT_1:def 6;
then
A149: q in L by A38,A5,A148,FUNCT_1:def 4;
dom(b1+*(i,S)) = I by PARTFUN1:def 2;
then q.i in b1+*(i,S).i by A149,CARD_3:9;
then
A150: q.i in S by A124,FUNCT_7:31;
then reconsider qi=q.i as Point of A.i;
consider q0 being ManySortedSet of I such that
A151: q0 in product b1 and
A152: {q0+*(i,qi) qua set} = product(b1+*(i,{qi})) by Th18;
A153: dom q0 = I by PARTFUN1:def 2;
A154: now
let a be object;
assume a in I;
per cases;
suppose
a=i;
hence q0+*(i,qi).a = q.a by A153,FUNCT_7:31;
end;
suppose
A155: a<>i;
then q0+*(i,qi).a = q0.a by FUNCT_7:32;
hence q0+*(i,qi).a = q.a by A127,A149,A151,A155,PENCIL_1:23;
end;
end;
q0+*(i,qi) = q by A154;
then Im(f,q0+*(i,qi))={f.q} by A38,FUNCT_1:59;
then p in f.:product(b1+*(i,{qi})) by A148,A152,TARSKI:def 1;
then m.(q.i) = p0+*(s.i,u).(s.i) by A37;
then m.(q.i) = o by A145,FUNCT_7:31;
hence thesis by A37,A150,FUNCT_1:def 6;
end;
hence thesis by A123,A128,PRE_TOPC:def 2;
end;
take M;
A156: m is onto by A86,FUNCT_2:def 3;
then m" is bijective by A46,PENCIL_2:12;
hence m is isomorphic by A46,A156,A121,A88,PENCIL_2:def 4;
let a be ManySortedSet of I such that
A157: a is Point of Segre_Product A and
A158: a in product b1;
dom Carrier A = I by PARTFUN1:def 2;
then a.i in (Carrier A).i by A7,A157,CARD_3:9;
then a.i in [#](A.i) by Th7;
then reconsider ai=a.i as Point of A.i;
A159: dom b1 = I by PARTFUN1:def 2;
A160: now
let o be object;
assume
A161: o in I;
per cases;
suppose
A162: o=i;
then b1+*(i,{ai}).o = {ai} by A159,FUNCT_7:31;
hence a.o in b1+*(i,{ai}).o by A162,TARSKI:def 1;
end;
suppose
o<>i;
then b1+*(i,{ai}).o = b1.o by FUNCT_7:32;
hence a.o in b1+*(i,{ai}).o by A158,A159,A161,CARD_3:9;
end;
end;
dom a = I & dom (b1+*(i,{ai})) = I by PARTFUN1:def 2;
then
A163: a in product(b1+*(i,{ai})) by A160,CARD_3:9;
let b be ManySortedSet of I;
assume b=f.a;
then b in f.:product(b1+*(i,{ai})) by A38,A157,A163,FUNCT_1:def 6;
hence thesis by A37;
end;
uniqueness
proof
set i=indx(b1);
set s=permutation_of_indices(f);
let f1,f2 be Function of A.i,A.(permutation_of_indices(f).i) such that
f1 is isomorphic and
A164: for a being ManySortedSet of I st a is Point of Segre_Product A
& a in product b1 for b being ManySortedSet of I st b=f.a holds b.(s.i)=f1.(a.i
) and
f2 is isomorphic and
A165: for a being ManySortedSet of I st a is Point of Segre_Product A
& a in product b1 for b being ManySortedSet of I st b=f.a holds b.(s.i)=f2.(a.i
);
A166: now
let x be object;
consider p being object such that
A167: p in product b1 by XBOOLE_0:def 1;
assume x in dom f1;
then reconsider x0=x as Point of A.i;
reconsider p as Point of Segre_Product A by A2,A167;
reconsider P=p as ManySortedSet of I by PENCIL_1:14;
set a=P+*(i,x0);
reconsider a1=a as Point of Segre_Product A by PENCIL_1:25;
A168: dom b1 = I by PARTFUN1:def 2;
A169: dom P = I by PARTFUN1:def 2;
A170: now
let e be object;
assume
A171: e in I;
per cases;
suppose
A172: e=i;
then a.e = x0 by A169,FUNCT_7:31;
then a.e in [#](A.i);
hence a.e in b1.e by A2,A172,Th10;
end;
suppose
e<>i;
then a.e = P.e by FUNCT_7:32;
hence a.e in b1.e by A167,A168,A171,CARD_3:9;
end;
end;
reconsider b=f.a1 as ManySortedSet of I by PENCIL_1:14;
dom P = I by PARTFUN1:def 2;
then
A173: a.i=x by FUNCT_7:31;
dom a = I by PARTFUN1:def 2;
then
A174: a in product b1 by A168,A170,CARD_3:9;
then f2.(a.i)=b.(s.i) by A165;
hence f1.x = f2.x by A164,A174,A173;
end;
dom f1 = the carrier of A.i by FUNCT_2:def 1
.= dom f2 by FUNCT_2:def 1;
hence f1=f2 by A166;
end;
end;
theorem Th26:
for I being finite 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 f being Collineation of Segre_Product A for B1,B2 being Segre-Coset of A st
B1 misses B2 & B1 '||' B2 for b1,b2 being Segre-like non trivial-yielding
ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding(f,b1) = canonical_embedding(f,b2)
proof
let I be finite 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 f be Collineation of Segre_Product A;
let B1,B2 be Segre-Coset of A such that
A2: B1 misses B2 and
A3: B1 '||' B2;
let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A
such that
A4: product b1 = B1 and
A5: product b2 = B2;
A6: indx(b1)=indx(b2) by A2,A3,A4,A5,Th21;
reconsider B3=f.:B1,B4=f.:B2 as Segre-Coset of A by A1,PENCIL_2:24;
A7: f is bijective by PENCIL_2:def 4;
then
A8: B3 misses B4 by A2,FUNCT_1:66;
set i = indx(b1);
consider r being Element of I such that
A9: r<>indx(b1) and
A10: for i being Element of I st i<>r holds b1.i=b2.i and
A11: for c1,c2 being Point of A.r st b1.r={c1} & b2.r={c2} holds c1,c2
are_collinear by A2,A3,A4,A5,Th21;
consider b4 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A12: product b4 = B4 and
A13: b4.indx(b4) = [#](A.indx(b4)) by PENCIL_2:def 2;
consider b3 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A14: product b3 = B3 and
A15: b3.indx(b3) = [#](A.indx(b3)) by PENCIL_2:def 2;
B3 '||' B4 by A3,Th20;
then
A16: indx(b3)=indx(b4) by A8,A14,A12,Th21;
set j = indx(b3);
A17: dom f = the carrier of Segre_Product A by FUNCT_2:def 1;
A18: dom b1 = I by PARTFUN1:def 2;
A19: now
b2.r is trivial by A6,A9,PENCIL_1:def 21;
then consider c2 being object such that
A20: b2.r = {c2} by ZFMISC_1:131;
b2 c= Carrier A by PBOOLE:def 18;
then b2.r c= (Carrier A).r;
then
A21: {c2} c= [#](A.r) by A20,Th7;
let o be object;
consider p0 being object such that
A22: p0 in product b1 by XBOOLE_0:def 1;
assume o in the carrier of A.i;
then reconsider u=o as Point of A.i;
reconsider p1=p0 as Point of Segre_Product A by A4,A22;
reconsider p=p1 as ManySortedSet of I by PENCIL_1:14;
set q=p+*(i,u);
reconsider q1=q as Point of Segre_Product A by PENCIL_1:25;
b1.r is trivial by A9,PENCIL_1:def 21;
then consider c1 being object such that
A23: b1.r = {c1} by ZFMISC_1:131;
b1 c= Carrier A by PBOOLE:def 18;
then b1.r c= (Carrier A).r;
then {c1} c= [#](A.r) by A23,Th7;
then reconsider c1 as Point of A.r by ZFMISC_1:31;
reconsider c2 as Point of A.r by A21,ZFMISC_1:31;
set t=q+*(r,c2);
q is Point of Segre_Product A by PENCIL_1:25;
then reconsider t1=t as Point of Segre_Product A by PENCIL_1:25;
per cases;
suppose
A24: c1<>c2;
q.r = p.r by A9,FUNCT_7:32;
then q.r in b1.r by A18,A22,CARD_3:9;
then
A25: q.r = c1 by A23,TARSKI:def 1;
dom q = I by PARTFUN1:def 2;
then
A26: t.r=c2 by FUNCT_7:31;
now
let q3,t3 be ManySortedSet of I such that
A27: q3=q1 & t3=t1;
take r;
thus for a,b being Point of A.r st a=q3.r & b=t3.r holds a<>b & a,b
are_collinear by A11,A23,A20,A24,A25,A26,A27;
let j be Element of I;
assume j<>r;
hence q3.j = t3.j by A27,FUNCT_7:32;
end;
then q1,t1 are_collinear by A24,A25,A26,Th17;
then
A28: f.q1,f.t1 are_collinear by Th1;
reconsider fq=f.q1,ft=f.t1 as ManySortedSet of I by PENCIL_1:14;
A29: dom b1 = I by PARTFUN1:def 2;
A30: dom p = I by PARTFUN1:def 2;
A31: now
let a be object;
assume
A32: a in I;
per cases;
suppose
a=i;
then q.a = u & b1.a = [#](A.i) by A4,A30,Th10,FUNCT_7:31;
hence q.a in b1.a;
end;
suppose
a<>i;
then q.a = p.a by FUNCT_7:32;
hence q.a in b1.a by A22,A29,A32,CARD_3:9;
end;
end;
A33: dom q = I by PARTFUN1:def 2;
then
A34: q in product b1 by A29,A31,CARD_3:9;
A35: now
let a be object;
assume
A36: a in I;
per cases;
suppose
A37: a=r;
then t.a = c2 by A33,FUNCT_7:31;
hence t.a in b2.a by A20,A37,TARSKI:def 1;
end;
suppose
A38: a<>r;
then t.a = q.a by FUNCT_7:32;
then t.a in b1.a by A31,A36;
hence t.a in b2.a by A10,A36,A38;
end;
end;
dom t = I & dom b2 = I by PARTFUN1:def 2;
then
A39: t in product b2 by A35,CARD_3:9;
then
A40: canonical_embedding(f,b2).(t.i)=ft.(permutation_of_indices(f) .i)
by A1,A5,A6,Def4;
A41: f.q1 <> f.t1 by A17,A7,A24,A25,A26,FUNCT_1:def 4;
A42: now
consider l being Element of I such that
for a,b being Point of A.l st a=fq.l & b=ft.l holds a<>b & a,b
are_collinear and
A43: for j being Element of I st j<>l holds fq.j = ft.j by A41,A28,Th17;
assume fq.j<>ft.j;
then
A44: j=l by A43;
A45: dom b4=I by PARTFUN1:def 2;
A46: fq in B3 by A17,A4,A34,FUNCT_1:def 6;
A47: dom b3 = I by PARTFUN1:def 2;
A48: now
let o be object;
assume o in I;
then reconsider o1=o as Element of I;
per cases;
suppose
o1=j;
hence fq.o in b4.o by A14,A15,A13,A16,A46,A47,CARD_3:9;
end;
suppose
o1<>j;
then
A49: fq.o1 = ft.o1 by A43,A44;
ft in product b4 by A17,A5,A12,A39,FUNCT_1:def 6;
hence fq.o in b4.o by A45,A49,CARD_3:9;
end;
end;
dom fq = I by PARTFUN1:def 2;
then fq in product b4 by A45,A48,CARD_3:9;
then fq in product b3 /\ product b4 by A14,A46,XBOOLE_0:def 4;
hence contradiction by A8,A14,A12;
end;
A50: j=permutation_of_indices(f).i by A1,A4,A14,Def3;
dom p = I by PARTFUN1:def 2;
then
A51: q.i=o by FUNCT_7:31;
then t.i=o by A9,FUNCT_7:32;
hence
canonical_embedding(f,b1).o = canonical_embedding(f,b2).o by A1,A4,A50
,A34,A40,A42,A51,Def4;
end;
suppose
A52: c1=c2;
A53: now
let o be object;
assume o in I;
then reconsider o1=o as Element of I;
per cases;
suppose
r=o1;
hence b1.o=b2.o by A23,A20,A52;
end;
suppose
r<>o1;
hence b1.o=b2.o by A10;
end;
end;
dom b1 = I & dom b2 = I by PARTFUN1:def 2;
hence canonical_embedding(f,b1).o = canonical_embedding(f,b2).o by A53,
FUNCT_1:2;
end;
end;
dom canonical_embedding(f,b1) = the carrier of A.i & dom
canonical_embedding (f,b2) = the carrier of A.i by A6,FUNCT_2:def 1;
hence thesis by A19;
end;
theorem Th27:
for I being finite 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 f being Collineation of Segre_Product A for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b1 is Segre-Coset of
A & product b2 is Segre-Coset of A & indx(b1)=indx(b2) holds
canonical_embedding(f,b1) = canonical_embedding(f,b2)
proof
let I be finite 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;
A2: now
let o be Element of I;
A.o is strongly_connected by A1;
hence A.o is connected by Th4;
end;
let f be Collineation of Segre_Product A;
let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A
such that
A3: product b1 is Segre-Coset of A & product b2 is Segre-Coset of A and
A4: indx(b1)=indx(b2);
reconsider B1=product b1, B2=product b2 as Segre-Coset of A by A3;
per cases;
suppose
B1 misses B2;
then consider
D being FinSequence of bool the carrier of Segre_Product A such
that
A5: D.1=B1 and
A6: D.(len D)=B2 and
A7: for i being Nat st i in dom D holds D.i is Segre-Coset of A and
A8: for i being Nat st 1<=i & i<len D for Di,Di1 being Segre-Coset of
A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1 by A2,A4,Th23;
defpred P[Nat] means $1 in dom D implies for D1 being Segre-Coset of A st
D1=D.$1 for d1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A st D1=product d1 holds canonical_embedding(f,b1)=canonical_embedding(
f,d1);
A9: now
let k be Nat;
assume
A10: P[k];
thus P[k+1]
proof
assume k+1 in dom D;
then k+1 <= len D by FINSEQ_3:25;
then
A11: k < len D by NAT_1:13;
let D2 be Segre-Coset of A such that
A12: D2=D.(k+1);
let d2 be Segre-like non trivial-yielding ManySortedSubset of Carrier
A such that
A13: D2=product d2;
per cases by NAT_1:14;
suppose
k=0;
hence thesis by A5,A12,A13,PUA2MSS1:2;
end;
suppose
A14: 1<=k;
then k in dom D by A11,FINSEQ_3:25;
then reconsider D1=D.k as Segre-Coset of A by A7;
consider d1 being Segre-like non trivial-yielding ManySortedSubset
of Carrier A such that
A15: product d1 = D1 and
d1.indx(d1)=[#](A.indx(d1)) by PENCIL_2:def 2;
D1 misses D2 & D1 '||' D2 by A8,A11,A12,A14;
then canonical_embedding(f,d1)=canonical_embedding(f,d2) by A1,A13
,A15,Th26;
hence thesis by A10,A11,A14,A15,FINSEQ_3:25;
end;
end;
end;
A16: P[ 0 ] by FINSEQ_3:24;
for n being Nat holds P[n] from NAT_1:sch 2(A16,A9);
then
A17: P[len D];
1 in dom D by A5,FUNCT_1:def 2;
then 1 <= len D by FINSEQ_3:25;
hence thesis by A6,A17,FINSEQ_3:25;
end;
suppose
B1 meets B2;
hence thesis by A4,Th11;
end;
end;
definition
let I be finite 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 f be Collineation of Segre_Product A;
let i be Element of I;
func canonical_embedding(f,i) -> Function of A.i,A.(permutation_of_indices(f
).i) means
:Def5:
for b being Segre-like non trivial-yielding ManySortedSubset
of Carrier A st product b is Segre-Coset of A & indx(b)=i holds it=
canonical_embedding(f,b);
existence
proof
consider L being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A2: indx(L)=i and
A3: product L is Segre-Coset of A by Th8;
reconsider n=canonical_embedding(f,L) as Function of A.i,A.(
permutation_of_indices(f).i) by A2;
take n;
let b be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
assume product b is Segre-Coset of A & indx(b)=i;
hence thesis by A1,A2,A3,Th27;
end;
uniqueness
proof
let n1,n2 be Function of A.i,A.(permutation_of_indices(f).i) such that
A4: for b being Segre-like non trivial-yielding ManySortedSubset of
Carrier A st product b is Segre-Coset of A & indx(b)=i holds n1=
canonical_embedding(f,b) and
A5: for b being Segre-like non trivial-yielding ManySortedSubset of
Carrier A st product b is Segre-Coset of A & indx(b)=i holds n2=
canonical_embedding(f,b);
consider L being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A6: indx(L)=i & product L is Segre-Coset of A by Th8;
thus n1=canonical_embedding(f,L) by A4,A6
.= n2 by A5,A6;
end;
end;
theorem
for I being finite 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 f being Collineation of Segre_Product A ex s being Permutation of I, B
being Function-yielding ManySortedSet of I st for i being Element of I holds (B
.i is Function of A.i,A.(s.i) & for m being Function of A.i,A.(s.i) st m=B.i
holds m is isomorphic) & for p being Point of Segre_Product A for a being
ManySortedSet of I st a=p for b being ManySortedSet of I st b=f.p for m being
Function of A.i,A.(s.i) st m=B.i holds b.(s.i)=m.(a.i)
proof
let I be finite 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 f be Collineation of Segre_Product A;
set s=permutation_of_indices(f);
take s;
defpred P[object,object] means
for i being Element of I st i=$1 holds $2= canonical_embedding(f,i);
A2: for i being object st i in I ex j being object st P[i,j]
proof
let i be object;
assume i in I;
then reconsider i1=i as Element of I;
P[i1,canonical_embedding(f,i1)];
hence thesis;
end;
consider B being ManySortedSet of I such that
A3: for i being object st i in I holds P[i,B.i] from PBOOLE:sch 3(A2);
now
let x be object;
assume x in dom B;
then reconsider y=x as Element of I;
B.y = canonical_embedding(f,y) by A3;
hence B.x is Function;
end;
then reconsider B as Function-yielding ManySortedSet of I by FUNCOP_1:def 6;
take B;
let i be Element of I;
A4: B.i = canonical_embedding(f,i) by A3;
thus B.i is Function of A.i,A.(s.i) & for m being Function of A.i,A.(s.i) st
m=B.i holds m is isomorphic
proof
thus B.i is Function of A.i,A.(s.i) by A4;
let m be Function of A.i,A.(s.i);
assume
A5: m=B.i;
consider L being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A6: indx(L)=i & product L is Segre-Coset of A by Th8;
B.i=canonical_embedding(f,L) by A1,A4,A6,Def5;
hence thesis by A1,A5,A6,Def4;
end;
let p be Point of Segre_Product A;
let a be ManySortedSet of I such that
A7: a=p;
consider b1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A such that
A8: indx(b1)=i & product b1 is Segre-Coset of A and
A9: a in product b1 by A7,Th9;
let b be ManySortedSet of I such that
A10: b=f.p;
let m be Function of A.i,A.(s.i);
assume m=B.i;
then m=canonical_embedding(f,b1) by A1,A4,A8,Def5;
hence thesis by A1,A7,A10,A8,A9,Def4;
end;