:: PENCIL_3 semantic presentation
begin
theorem Th1: :: PENCIL_3:1
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 ; ::_thesis: 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
let f be Collineation of S; ::_thesis: for p, q being Point of S st p,q are_collinear holds
f . p,f . q are_collinear
A1: dom f = the carrier of S by FUNCT_2:def_1;
let p, q be Point of S; ::_thesis: ( p,q are_collinear implies f . p,f . q are_collinear )
assume A2: p,q are_collinear ; ::_thesis: f . p,f . q are_collinear
percases ( p = q or p <> q ) ;
suppose p = q ; ::_thesis: f . p,f . q are_collinear
hence f . p,f . q are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
suppose p <> q ; ::_thesis: f . p,f . q are_collinear
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 f . p,f . q are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
end;
end;
theorem Th2: :: PENCIL_3:2
for I being non empty set
for i being Element of I
for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial
proof
let I be non empty set ; ::_thesis: for i being Element of I
for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial
let i be Element of I; ::_thesis: for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial
let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: not A . i is trivial
dom A = I by PARTFUN1:def_2;
then A . i in rng A by FUNCT_1:3;
hence not A . i is trivial by PENCIL_1:def_17; ::_thesis: verum
end;
theorem Th3: :: PENCIL_3:3
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 ; ::_thesis: ( S is strongly_connected implies S is without_isolated_points )
assume A1: S is strongly_connected ; ::_thesis: S is without_isolated_points
now__::_thesis:_for_x_being_Point_of_S_ex_l_being_Block_of_S_st_x_in_l
consider X being set such that
A2: X in the topology of S by XBOOLE_0:def_1;
reconsider X = X as Block of S by A2;
reconsider X1 = X as Subset of S by A2;
let x be Point of S; ::_thesis: ex l being Block of S st l in b2
( X1 is closed_under_lines & X1 is strong ) by PENCIL_1:20, PENCIL_1: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 & W is 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 & W is strong ) by A5, A8;
percases ( x in X or not x in X ) ;
suppose x in X ; ::_thesis: ex l being Block of S st l in b2
hence ex l being Block of S st x in l ; ::_thesis: verum
end;
supposeA10: not x in X ; ::_thesis: ex l being Block of S st l in b2
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 set 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 = 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 ; ::_thesis: verum
end;
end;
end;
hence S is without_isolated_points by PENCIL_1:def_9; ::_thesis: verum
end;
theorem Th4: :: PENCIL_3:4
for S being non empty non void identifying_close_blocks TopStruct st S is strongly_connected holds
S is connected
proof
let S be non empty non void identifying_close_blocks TopStruct ; ::_thesis: ( S is strongly_connected implies S is connected )
assume A1: S is strongly_connected ; ::_thesis: S is connected
then S is without_isolated_points by Th3;
hence S is connected by A1, PENCIL_1:28; ::_thesis: verum
end;
theorem :: PENCIL_3:5
for S being non void non degenerated TopStruct
for L being Block of S holds
not for x being Point of S holds x in L
proof
let S be non void non degenerated TopStruct ; ::_thesis: for L being Block of S holds
not for x being Point of S holds x in L
let L be Block of S; ::_thesis: not for x being Point of S holds x in L
A1: L in the topology of S ;
now__::_thesis:_not_[#]_S_c=_L
assume [#] S c= L ; ::_thesis: contradiction
then [#] S = L by A1, XBOOLE_0:def_10;
hence contradiction by PENCIL_1:def_5; ::_thesis: verum
end;
then consider x being set such that
A2: x in [#] S and
A3: not x in L by TARSKI:def_3;
reconsider x = x as Point of S by A2;
take x ; ::_thesis: not x in L
thus not x in L by A3; ::_thesis: verum
end;
theorem Th6: :: PENCIL_3:6
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 ; ::_thesis: 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
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for p being Point of (Segre_Product A) holds p is Element of Carrier A
let p be Point of (Segre_Product A); ::_thesis: p is Element of Carrier 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 set 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 = f as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in I holds
f . i is Element of (Carrier A) . i by A2, A3, A4;
hence p is Element of Carrier A by A1, PBOOLE:def_14; ::_thesis: verum
end;
theorem Th7: :: PENCIL_3:7
for I being non empty set
for A being 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 ; ::_thesis: for A being 1-sorted-yielding ManySortedSet of I
for x being Element of I holds (Carrier A) . x = [#] (A . x)
let A be 1-sorted-yielding ManySortedSet of I; ::_thesis: for x being Element of I holds (Carrier A) . x = [#] (A . x)
let x be Element of I; ::_thesis: (Carrier A) . x = [#] (A . x)
ex R being 1-sorted st
( R = A . x & (Carrier A) . x = the carrier of R ) by PRALG_1:def_13;
hence (Carrier A) . x = [#] (A . x) ; ::_thesis: verum
end;
theorem Th8: :: PENCIL_3:8
for I being non empty set
for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A )
proof
let I be non empty set ; ::_thesis: for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A )
let x be Element of I; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A )
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A )
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 not A . x is trivial by PENCIL_1:def_18;
then reconsider C = [#] (A . x) as non trivial set ;
reconsider p0 = the Point of (Segre_Product A) 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 non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;
take b ; ::_thesis: ( indx b = x & product b is Segre-Coset of A )
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; ::_thesis: product b is Segre-Coset of A
product b c= the carrier of (Segre_Product A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) )
assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A)
then consider f being Function such that
A3: a = f and
A4: dom f = dom b and
A5: for x being set 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__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_
f_._i_in_(Carrier_A)_._i
let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 )
assume A8: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1
then reconsider i1 = i as Element of I ;
A9: f . i in b . i by A4, A5, A6, A8;
percases ( i1 = x or i1 <> x ) ;
suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1
hence f . i in (Carrier A) . i by A1, A9, Th7; ::_thesis: verum
end;
supposeA10: i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1
I = dom A by PARTFUN1:def_2;
then A . i1 in rng A by FUNCT_1:3;
then not A . i1 is 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;
not AA is empty ;
then not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A11; ::_thesis: verum
end;
end;
end;
Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23;
hence a in the carrier of (Segre_Product A) by A3, A6, A7, CARD_3:def_5; ::_thesis: verum
end;
hence product b is Segre-Coset of A by A1, A2, PENCIL_2:def_2; ::_thesis: verum
end;
theorem Th9: :: PENCIL_3:9
for I being non empty set
for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A & p in product L )
proof
let I be non empty set ; ::_thesis: for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A & p in product L )
let x be Element of I; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A & p in product L )
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A & p in product L )
let p0 be Point of (Segre_Product A); ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = x & product L is Segre-Coset of A & p0 in product L )
dom A = I by PARTFUN1:def_2;
then A . x in rng A by FUNCT_1:3;
then not A . x is 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 non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;
take b ; ::_thesis: ( indx b = x & product b is Segre-Coset of A & p0 in product 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; ::_thesis: ( product b is Segre-Coset of A & p0 in product b )
product b c= the carrier of (Segre_Product A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) )
assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A)
then consider f being Function such that
A3: a = f and
A4: dom f = dom b and
A5: for x being set 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__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_
f_._i_in_(Carrier_A)_._i
let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 )
assume A8: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1
then reconsider i1 = i as Element of I ;
A9: f . i in b . i by A4, A5, A6, A8;
percases ( i1 = x or i1 <> x ) ;
suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1
hence f . i in (Carrier A) . i by A1, A9, Th7; ::_thesis: verum
end;
supposeA10: i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1
I = dom A by PARTFUN1:def_2;
then A . i1 in rng A by FUNCT_1:3;
then not A . i1 is 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;
not AA is empty ;
then not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A11; ::_thesis: verum
end;
end;
end;
Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23;
hence a in the carrier of (Segre_Product A) by A3, A6, A7, CARD_3:def_5; ::_thesis: verum
end;
hence product b is Segre-Coset of A by A1, A2, PENCIL_2:def_2; ::_thesis: p0 in product b
A12: dom p = I by PARTFUN1:def_2;
A13: now__::_thesis:_for_z_being_set_st_z_in_I_holds_
p09_._z_in_(p_+*_(x,C))_._z
let z be set ; ::_thesis: ( z in I implies p09 . b1 in (p +* (x,C)) . b1 )
assume A14: z in I ; ::_thesis: p09 . b1 in (p +* (x,C)) . b1
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: not tc is empty ;
percases ( z = x or z <> x ) ;
supposeA16: z = x ; ::_thesis: p09 . b1 in (p +* (x,C)) . b1
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; ::_thesis: verum
end;
suppose z <> x ; ::_thesis: p09 . b1 in (p +* (x,C)) . b1
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; ::_thesis: verum
end;
end;
end;
( dom p09 = I & dom (p +* (x,C)) = I ) by PARTFUN1:def_2;
hence p0 in product b by A13, CARD_3:9; ::_thesis: verum
end;
theorem Th10: :: PENCIL_3:10
for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for b being non trivial-yielding Segre-like 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 ; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A holds
b . (indx b) = [#] (A . (indx b))
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A holds
b . (indx b) = [#] (A . (indx b))
let b be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b is Segre-Coset of A implies b . (indx b) = [#] (A . (indx b)) )
assume product b is Segre-Coset of A ; ::_thesis: b . (indx b) = [#] (A . (indx b))
then consider L being non trivial-yielding Segre-like 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 b . (indx b) = [#] (A . (indx b)) by A2; ::_thesis: verum
end;
theorem Th11: :: PENCIL_3:11
for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for L1, L2 being non trivial-yielding Segre-like 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 ; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for L1, L2 being non trivial-yielding Segre-like 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
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for L1, L2 being non trivial-yielding Segre-like 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
let L1, L2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 implies L1 = L2 )
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 ; ::_thesis: L1 = L2
reconsider B1 = product L1, B2 = product L2 as Segre-Coset of A by A1;
B1 /\ B2 <> {} by A3, XBOOLE_0:def_7;
then consider x being set 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 = x as Element of Carrier A by A4, Th6;
consider b1 being non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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__::_thesis:_for_a_being_set_st_a_in_dom_L1_holds_
L1_._a_=_L2_._a
let a be set ; ::_thesis: ( a in dom L1 implies L1 . b1 = L2 . b1 )
assume A14: a in dom L1 ; ::_thesis: L1 . b1 = L2 . b1
then reconsider i = a as Element of I ;
percases ( i = indx L1 or i <> indx L1 ) ;
suppose i = indx L1 ; ::_thesis: L1 . b1 = L2 . b1
hence L1 . a = L2 . a by A2, A8, A10, A13, A11; ::_thesis: verum
end;
supposeA15: i <> indx L1 ; ::_thesis: L1 . b1 = L2 . b1
then ( not L1 . i is empty & L1 . i is trivial ) by PENCIL_1:def_21;
then L1 . i is 1 -element ;
then consider o1 being set such that
A16: L1 . i = {o1} by ZFMISC_1:131;
( not L2 . i is empty & L2 . i is trivial ) by A2, A15, PENCIL_1:def_21;
then L2 . i is 1 -element ;
then consider o2 being set 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; ::_thesis: verum
end;
end;
end;
hence L1 = L2 by A12, FUNCT_1:2; ::_thesis: verum
end;
theorem Th12: :: PENCIL_3:12
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for L being non trivial-yielding Segre-like 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 be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A)
let A be PLS-yielding ManySortedSet of I; ::_thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A)
let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A)
let B be Block of (A . (indx L)); ::_thesis: product (L +* ((indx L),B)) is Block of (Segre_Product A)
B in the topology of (A . (indx L)) ;
then reconsider B1 = B as Subset of (A . (indx L)) ;
A1: now__::_thesis:_for_i_being_Element_of_I_st_i_<>_indx_L_holds_
(L_+*_((indx_L),B1))_._i_is_1_-element
let i be Element of I; ::_thesis: ( i <> indx L implies (L +* ((indx L),B1)) . i is 1 -element )
assume A2: i <> indx L ; ::_thesis: (L +* ((indx L),B1)) . i is 1 -element
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; ::_thesis: verum
end;
2 c= card B by PENCIL_1:def_6;
then not B1 is trivial by PENCIL_1:4;
then reconsider S = L +* ((indx L),B1) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A1, PENCIL_1:9, PENCIL_1:def_20, PENCIL_2:7;
A3: now__::_thesis:_not_indx_S_<>_indx_L
assume indx S <> indx L ; ::_thesis: contradiction
then S . (indx S) is 1 -element by A1;
hence contradiction by PENCIL_1:def_21; ::_thesis: verum
end;
dom L = I by PARTFUN1:def_2;
then S . (indx S) = B1 by A3, FUNCT_7:31;
hence product (L +* ((indx L),B)) is Block of (Segre_Product A) by A3, PENCIL_1:24; ::_thesis: verum
end;
theorem Th13: :: PENCIL_3:13
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for i being Element of I
for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for i being Element of I
for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let A be PLS-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let i be Element of I; ::_thesis: for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let p be Point of (A . i); ::_thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( i <> indx L implies L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A )
A1: now__::_thesis:_for_j_being_Element_of_I_st_j_<>_indx_L_holds_
(L_+*_(i,{p}))_._j_is_1_-element
let j be Element of I; ::_thesis: ( j <> indx L implies (L +* (i,{p})) . b1 is 1 -element )
A2: dom L = I by PARTFUN1:def_2;
assume A3: j <> indx L ; ::_thesis: (L +* (i,{p})) . b1 is 1 -element
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: (L +* (i,{p})) . b1 is 1 -element
hence (L +* (i,{p})) . j is 1 -element by A2, FUNCT_7:31; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: (L +* (i,{p})) . b1 is 1 -element
then (L +* (i,{p})) . j = L . j by FUNCT_7:32;
hence (L +* (i,{p})) . j is 1 -element by A3, PENCIL_1:12; ::_thesis: verum
end;
end;
end;
A4: L +* (i,{p}) c= Carrier A
proof
let a be set ; :: according to PBOOLE:def_2 ::_thesis: ( not a in I or (L +* (i,{p})) . a c= (Carrier A) . a )
assume A5: a in I ; ::_thesis: (L +* (i,{p})) . a c= (Carrier A) . a
then reconsider a1 = a as Element of I ;
A6: a1 in dom L by A5, PARTFUN1:def_2;
percases ( a = i or a <> i ) ;
supposeA7: a = i ; ::_thesis: (L +* (i,{p})) . a c= (Carrier A) . a
then (L +* (i,{p})) . a1 = {p} by A6, FUNCT_7:31;
then (L +* (i,{p})) . a1 c= [#] (A . a1) by A7;
hence (L +* (i,{p})) . a c= (Carrier A) . a by Th7; ::_thesis: verum
end;
supposeA8: a <> i ; ::_thesis: (L +* (i,{p})) . a c= (Carrier A) . a
A9: L c= Carrier A by PBOOLE:def_18;
(L +* (i,{p})) . a1 = L . a1 by A8, FUNCT_7:32;
hence (L +* (i,{p})) . a c= (Carrier A) . a by A9, PBOOLE:def_2; ::_thesis: verum
end;
end;
end;
assume i <> indx L ; ::_thesis: L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A
then (L +* (i,{p})) . (indx L) = L . (indx L) by FUNCT_7:32;
then A10: not (L +* (i,{p})) . (indx L) is 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 L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A by A4, A1, A10, PBOOLE:def_18, PENCIL_1:def_16, PENCIL_1:def_20; ::_thesis: verum
end;
theorem Th14: :: PENCIL_3:14
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 non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for i being Element of I
for S being Subset of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)
let A be PLS-yielding ManySortedSet of I; ::_thesis: for i being Element of I
for S being Subset of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)
let i be Element of I; ::_thesis: for S being Subset of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)
let S be Subset of (A . i); ::_thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A)
let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: product (L +* (i,S)) is Subset of (Segre_Product A)
A1: dom (L +* (i,S)) = I by PARTFUN1:def_2
.= dom (Carrier A) by PARTFUN1:def_2 ;
A2: now__::_thesis:_for_a_being_set_st_a_in_dom_(L_+*_(i,S))_holds_
(L_+*_(i,S))_._a_c=_(Carrier_A)_._a
let a be set ; ::_thesis: ( a in dom (L +* (i,S)) implies (L +* (i,S)) . b1 c= (Carrier A) . b1 )
assume a in dom (L +* (i,S)) ; ::_thesis: (L +* (i,S)) . b1 c= (Carrier A) . b1
then A3: a in I ;
then A4: a in dom L by PARTFUN1:def_2;
percases ( a = i or a <> i ) ;
supposeA5: a = i ; ::_thesis: (L +* (i,S)) . b1 c= (Carrier A) . b1
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; ::_thesis: verum
end;
supposeA6: a <> i ; ::_thesis: (L +* (i,S)) . b1 c= (Carrier A) . b1
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, PBOOLE:def_2; ::_thesis: verum
end;
end;
end;
Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23;
hence product (L +* (i,S)) is Subset of (Segre_Product A) by A1, A2, CARD_3:27; ::_thesis: verum
end;
theorem Th15: :: PENCIL_3:15
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 be non empty set ; ::_thesis: for P being ManySortedSet of I
for i being Element of I holds {P} . i is 1 -element
let P be ManySortedSet of I; ::_thesis: for i being Element of I holds {P} . i is 1 -element
let i be Element of I; ::_thesis: {P} . i is 1 -element
{P} . i = {(P . i)} by PZFMISC1:def_1;
hence {P} . i is 1 -element ; ::_thesis: verum
end;
theorem Th16: :: PENCIL_3:16
for I being non empty set
for i being Element of I
for A being 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 be non empty set ; ::_thesis: for i being Element of I
for A being 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)
let i be Element of I; ::_thesis: for A being 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)
let A be PLS-yielding ManySortedSet of I; ::_thesis: 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)
let B be Block of (A . i); ::_thesis: for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of (Segre_Product A)
let P be Element of Carrier A; ::_thesis: product ({P} +* (i,B)) is Block of (Segre_Product 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__::_thesis:_for_j_being_Element_of_I_st_j_<>_i_holds_
({P}_+*_(i,B1))_._j_is_1_-element
let j be Element of I; ::_thesis: ( j <> i implies ({P} +* (i,B1)) . j is 1 -element )
assume j <> i ; ::_thesis: ({P} +* (i,B1)) . j is 1 -element
then ({P} +* (i,B1)) . j = {P} . j by FUNCT_7:32;
hence ({P} +* (i,B1)) . j is 1 -element by Th15; ::_thesis: verum
end;
2 c= card B by PENCIL_1:def_6;
then not B1 is trivial by PENCIL_1:4;
then reconsider S = PP +* (i,B1) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A1, PENCIL_1:9, PENCIL_1:def_20, PENCIL_2:7;
A2: now__::_thesis:_not_indx_S_<>_i
assume indx S <> i ; ::_thesis: contradiction
then S . (indx S) is 1 -element by A1;
hence contradiction by PENCIL_1:def_21; ::_thesis: verum
end;
dom {P} = I by PARTFUN1:def_2;
then S . (indx S) = B1 by A2, FUNCT_7:31;
hence product ({P} +* (i,B)) is Block of (Segre_Product A) by A2, PENCIL_1:24; ::_thesis: verum
end;
theorem Th17: :: PENCIL_3:17
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 holds
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 be non empty set ; ::_thesis: 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 holds
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 ) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: 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 holds
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 ) ) )
let p, q be Point of (Segre_Product A); ::_thesis: ( p <> q implies ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
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 ) ) ) )
assume A1: p <> q ; ::_thesis: ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
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 ) ) )
thus ( p,q are_collinear implies for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
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 ) ) ) ::_thesis: ( ( for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
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 ) ) ) implies p,q are_collinear )
proof
assume p,q are_collinear ; ::_thesis: for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
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 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; ::_thesis: ( p1 = p & q1 = q implies 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 ) ) )
assume that
A3: p1 = p and
A4: q1 = q ; ::_thesis: 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 ) )
A5: q1 in l by A2, A4, ZFMISC_1:32;
consider L being non trivial-yielding Segre-like 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; ::_thesis: ( ( 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 ) )
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 ) ::_thesis: for j being Element of I st j <> i holds
p1 . j = q1 . j
proof
reconsider LI = L . (indx L) as Block of (A . (indx L)) by A7;
let a, b be Point of (A . i); ::_thesis: ( a = p1 . i & b = q1 . i implies ( a <> b & a,b are_collinear ) )
A9: ex p0 being Function st
( p0 = p1 & dom p0 = dom L & ( for o being set 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 set 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 ) ; ::_thesis: ( a <> b & a,b are_collinear )
now__::_thesis:_not_a_=_b
assume A12: a = b ; ::_thesis: contradiction
A13: now__::_thesis:_for_o_being_set_st_o_in_dom_p1_holds_
p1_._o_=_q1_._o
let o be set ; ::_thesis: ( o in dom p1 implies p1 . b1 = q1 . b1 )
assume A14: o in dom p1 ; ::_thesis: p1 . b1 = q1 . b1
then reconsider o1 = o as Element of I ;
percases ( o1 = i or o1 <> i ) ;
suppose o1 = i ; ::_thesis: p1 . b1 = q1 . b1
hence p1 . o = q1 . o by A11, A12; ::_thesis: verum
end;
suppose o1 <> i ; ::_thesis: p1 . b1 = q1 . b1
then L . o1 is 1 -element by PENCIL_1:12;
then consider s being set 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; ::_thesis: verum
end;
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; ::_thesis: verum
end;
hence a <> b ; ::_thesis: a,b are_collinear
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 a,b are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
let j be Element of I; ::_thesis: ( j <> i implies p1 . j = q1 . j )
assume j <> i ; ::_thesis: p1 . j = q1 . j
hence p1 . j = q1 . j by A6, A8, A5, PENCIL_1:23; ::_thesis: verum
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 holds
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 ) ) ; ::_thesis: p,q are_collinear
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;
percases ( a = b or ex l being Block of (A . i) st {a,b} c= l ) by A21, PENCIL_1:def_1;
suppose a = b ; ::_thesis: p,q are_collinear
hence p,q are_collinear by A19; ::_thesis: verum
end;
suppose ex l being Block of (A . i) st {a,b} c= l ; ::_thesis: p,q are_collinear
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 set st o in dom ({p1} +* (i,l)) holds
q1 . o in ({p1} +* (i,l)) . o
proof
let o be set ; ::_thesis: ( o in dom ({p1} +* (i,l)) implies q1 . o in ({p1} +* (i,l)) . o )
assume A26: o in dom ({p1} +* (i,l)) ; ::_thesis: q1 . o in ({p1} +* (i,l)) . o
then reconsider o1 = o as Element of I ;
percases ( o1 = i or o1 <> i ) ;
supposeA27: o1 = i ; ::_thesis: q1 . o in ({p1} +* (i,l)) . o
then ({p1} +* (i,l)) . o = l by A24, A26, FUNCT_7:31;
hence q1 . o in ({p1} +* (i,l)) . o by A22, A27, ZFMISC_1:32; ::_thesis: verum
end;
supposeA28: o1 <> i ; ::_thesis: q1 . o in ({p1} +* (i,l)) . o
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 q1 . o in ({p1} +* (i,l)) . o by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
A29: for o being set st o in dom ({p1} +* (i,l)) holds
p1 . o in ({p1} +* (i,l)) . o
proof
let o be set ; ::_thesis: ( o in dom ({p1} +* (i,l)) implies p1 . o in ({p1} +* (i,l)) . o )
assume A30: o in dom ({p1} +* (i,l)) ; ::_thesis: p1 . o in ({p1} +* (i,l)) . o
percases ( o = i or o <> i ) ;
supposeA31: o = i ; ::_thesis: p1 . o in ({p1} +* (i,l)) . o
then ({p1} +* (i,l)) . o = l by A24, A30, FUNCT_7:31;
hence p1 . o in ({p1} +* (i,l)) . o by A22, A31, ZFMISC_1:32; ::_thesis: verum
end;
suppose o <> i ; ::_thesis: p1 . o in ({p1} +* (i,l)) . o
then ({p1} +* (i,l)) . o = {p1} . o by FUNCT_7:32;
then ({p1} +* (i,l)) . o = {(p1 . o)} by A30, PZFMISC1:def_1;
hence p1 . o in ({p1} +* (i,l)) . o by TARSKI:def_1; ::_thesis: verum
end;
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 p,q are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
end;
end;
theorem Th18: :: PENCIL_3:18
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for b being non trivial-yielding Segre-like 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))} = product (b +* ((indx b),{x})) )
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for b being non trivial-yielding Segre-like 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))} = product (b +* ((indx b),{x})) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: for b being non trivial-yielding Segre-like 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))} = product (b +* ((indx b),{x})) )
let b1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: for x being Point of (A . (indx b1)) ex p being ManySortedSet of I st
( p in product b1 & {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) )
set i = indx b1;
let x be Point of (A . (indx b1)); ::_thesis: ex p being ManySortedSet of I st
( p in product b1 & {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) )
consider bb being set 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 set 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 = bb as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18;
take p = bb; ::_thesis: ( p in product b1 & {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) )
thus p in product b1 by A1; ::_thesis: {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x}))
set bbx = bb +* ((indx b1),x);
thus {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) ::_thesis: verum
proof
thus {(p +* ((indx b1),x))} c= product (b1 +* ((indx b1),{x})) :: according to XBOOLE_0:def_10 ::_thesis: product (b1 +* ((indx b1),{x})) c= {(p +* ((indx b1),x))}
proof
A4: now__::_thesis:_for_z_being_set_st_z_in_dom_(b1_+*_((indx_b1),{x}))_holds_
(bb_+*_((indx_b1),x))_._z_in_(b1_+*_((indx_b1),{x}))_._z
let z be set ; ::_thesis: ( z in dom (b1 +* ((indx b1),{x})) implies (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 )
assume z in dom (b1 +* ((indx b1),{x})) ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
then A5: z in I ;
then A6: z in dom bb by PARTFUN1:def_2;
percases ( z = indx b1 or z <> indx b1 ) ;
supposeA7: z = indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
then (bb +* ((indx b1),x)) . z = x by A6, FUNCT_7:31;
then (bb +* ((indx b1),x)) . z in {x} by TARSKI:def_1;
hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A3, A7, FUNCT_7:31; ::_thesis: verum
end;
supposeA8: z <> indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
then (bb +* ((indx b1),x)) . z = bb . z by FUNCT_7:32;
then (bb +* ((indx b1),x)) . z in b1 . z by A1, A3, A5, CARD_3:9;
hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A8, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in {(p +* ((indx b1),x))} or o in product (b1 +* ((indx b1),{x})) )
assume o in {(p +* ((indx b1),x))} ; ::_thesis: o in product (b1 +* ((indx b1),{x}))
then A9: o = bb +* ((indx b1),x) by TARSKI:def_1;
dom (bb +* ((indx b1),x)) = I by PARTFUN1:def_2
.= dom (b1 +* ((indx b1),{x})) by PARTFUN1:def_2 ;
hence o in product (b1 +* ((indx b1),{x})) by A9, A4, CARD_3:9; ::_thesis: verum
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in product (b1 +* ((indx b1),{x})) or o in {(p +* ((indx b1),x))} )
assume o in product (b1 +* ((indx b1),{x})) ; ::_thesis: o in {(p +* ((indx b1),x))}
then consider u being Function such that
A10: u = o and
A11: dom u = dom (b1 +* ((indx b1),{x})) and
A12: for z being set st z in dom (b1 +* ((indx b1),{x})) holds
u . z in (b1 +* ((indx b1),{x})) . z by CARD_3:def_5;
A13: now__::_thesis:_for_z_being_set_st_z_in_dom_u_holds_
u_._z_=_(bb_+*_((indx_b1),x))_._z
let z be set ; ::_thesis: ( z in dom u implies u . b1 = (bb +* ((indx b1),x)) . b1 )
assume A14: z in dom u ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1
then A15: z in I by A11;
reconsider zz = z as Element of I by A11, A14;
A16: u . z in (b1 +* ((indx b1),{x})) . z by A11, A12, A14;
percases ( zz = indx b1 or zz <> indx b1 ) ;
supposeA17: zz = indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1
then u . z in {x} by A3, A16, FUNCT_7:31;
then u . z = x by TARSKI:def_1;
hence u . z = (bb +* ((indx b1),x)) . z by A2, A3, A17, FUNCT_7:31; ::_thesis: verum
end;
supposeA18: zz <> indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1
then ( not b1 . zz is empty & b1 . zz is trivial ) by PENCIL_1:def_21;
then b1 . zz is 1 -element ;
then consider o being set 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;
(bb +* ((indx b1),x)) . z = bb . z by A18, FUNCT_7:32;
then (bb +* ((indx b1),x)) . z in {o} by A2, A3, A15, A19;
hence u . z = (bb +* ((indx b1),x)) . z by A20, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
dom u = I by A11, PARTFUN1:def_2
.= dom (bb +* ((indx b1),x)) by PARTFUN1:def_2 ;
then u = bb +* ((indx b1),x) by A13, FUNCT_1:2;
hence o in {(p +* ((indx b1),x))} by A10, TARSKI:def_1; ::_thesis: verum
end;
end;
definition
let I be non empty finite set ;
let b1, b2 be ManySortedSet of I;
func diff (b1,b2) -> Nat equals :: PENCIL_3:def 1
card { i where i is Element of I : b1 . i <> b2 . i } ;
correctness
coherence
card { i where i is Element of I : b1 . i <> b2 . i } is Nat;
proof
{ i where i is Element of I : b1 . i <> b2 . i } c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : b1 . i <> b2 . i } or a in I )
assume a in { i where i is Element of I : b1 . i <> b2 . i } ; ::_thesis: a in I
then ex i being Element of I st
( a = i & b1 . i <> b2 . i ) ;
hence a in I ; ::_thesis: verum
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 card { i where i is Element of I : b1 . i <> b2 . i } is Nat ; ::_thesis: verum
end;
end;
:: deftheorem defines diff PENCIL_3:def_1_:_
for I being non empty finite set
for b1, b2 being ManySortedSet of I holds diff (b1,b2) = card { i where i is Element of I : b1 . i <> b2 . i } ;
theorem Th19: :: PENCIL_3:19
for I being non empty finite 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 non empty finite set ; ::_thesis: 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
let b1, b2 be ManySortedSet of I; ::_thesis: for i being Element of I st b1 . i <> b2 . i holds
diff (b1,b2) = (diff (b1,(b2 +* (i,(b1 . i))))) + 1
let j be Element of I; ::_thesis: ( b1 . j <> b2 . j implies diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1 )
set b3 = b2 +* (j,(b1 . j));
{ i where i is Element of I : b1 . i <> b2 . i } c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : b1 . i <> b2 . i } or a in I )
assume a in { i where i is Element of I : b1 . i <> b2 . i } ; ::_thesis: a in I
then ex i being Element of I st
( a = i & b1 . i <> b2 . i ) ;
hence a in I ; ::_thesis: verum
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 <> (b2 +* (j,(b1 . j))) . i } c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } or a in I )
assume a in { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } ; ::_thesis: a in I
then ex i being Element of I st
( a = i & b1 . i <> (b2 +* (j,(b1 . j))) . i ) ;
hence a in I ; ::_thesis: verum
end;
then reconsider G = { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } as finite set by FINSET_1:1;
assume A1: b1 . j <> b2 . j ; ::_thesis: diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1
A2: F = G \/ {j}
proof
thus F c= G \/ {j} :: according to XBOOLE_0:def_10 ::_thesis: G \/ {j} c= F
proof
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in F or o in G \/ {j} )
assume o in F ; ::_thesis: o in G \/ {j}
then consider i being Element of I such that
A3: o = i and
A4: b1 . i <> b2 . i ;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: o in G \/ {j}
then o in {j} by A3, TARSKI:def_1;
hence o in G \/ {j} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: o in G \/ {j}
then (b2 +* (j,(b1 . j))) . i = b2 . i by FUNCT_7:32;
then i in G by A4;
hence o in G \/ {j} by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in G \/ {j} or o in F )
assume A5: o in G \/ {j} ; ::_thesis: o in F
percases ( o in G or o in {j} ) by A5, XBOOLE_0:def_3;
suppose o in G ; ::_thesis: o in F
then consider i being Element of I such that
A6: o = i and
A7: b1 . i <> (b2 +* (j,(b1 . j))) . i ;
now__::_thesis:_not_b1_._i_=_b2_._i
assume A8: b1 . i = b2 . i ; ::_thesis: contradiction
then i = j by A7, FUNCT_7:32;
hence contradiction by A1, A8; ::_thesis: verum
end;
hence o in F by A6; ::_thesis: verum
end;
suppose o in {j} ; ::_thesis: o in F
then o = j by TARSKI:def_1;
hence o in F by A1; ::_thesis: verum
end;
end;
end;
now__::_thesis:_not_j_in_G
assume j in G ; ::_thesis: contradiction
then A9: ex jj being Element of I st
( jj = j & b1 . jj <> (b2 +* (j,(b1 . j))) . jj ) ;
dom b2 = I by PARTFUN1:def_2;
hence contradiction by A9, FUNCT_7:31; ::_thesis: verum
end;
hence diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1 by A2, CARD_2:41; ::_thesis: verum
end;
begin
definition
let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
let B1, B2 be Segre-Coset of A;
predB1 '||' B2 means :Def2: :: PENCIL_3:def 2
for x being Point of (Segre_Product A) st x in B1 holds
ex y being Point of (Segre_Product A) st
( y in B2 & x,y are_collinear );
end;
:: deftheorem Def2 defines '||' PENCIL_3:def_2_:_
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A holds
( B1 '||' B2 iff for x being Point of (Segre_Product A) st x in B1 holds
ex y being Point of (Segre_Product A) st
( y in B2 & x,y are_collinear ) );
theorem Th20: :: PENCIL_3:20
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 holds
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 ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st B1 '||' B2 holds
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
let A be PLS-yielding ManySortedSet of I; ::_thesis: for B1, B2 being Segre-Coset of A st B1 '||' B2 holds
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
let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 '||' B2 implies 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 )
assume A1: B1 '||' B2 ; ::_thesis: 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
let f be Collineation of (Segre_Product A); ::_thesis: for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds
C1 '||' C2
let C1, C2 be Segre-Coset of A; ::_thesis: ( C1 = f .: B1 & C2 = f .: B2 implies C1 '||' C2 )
assume that
A2: C1 = f .: B1 and
A3: C2 = f .: B2 ; ::_thesis: C1 '||' C2
let x be Point of (Segre_Product A); :: according to PENCIL_3:def_2 ::_thesis: ( x in C1 implies ex y being Point of (Segre_Product A) st
( y in C2 & x,y are_collinear ) )
assume x in C1 ; ::_thesis: ex y being Point of (Segre_Product A) st
( y in C2 & x,y are_collinear )
then consider a being set 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 = 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, Def2;
take y = f . b; ::_thesis: ( y in C2 & x,y are_collinear )
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; ::_thesis: x,y are_collinear
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: x,y are_collinear
hence x,y are_collinear by A6, PENCIL_1:def_1; ::_thesis: verum
end;
suppose a <> b ; ::_thesis: x,y are_collinear
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 x,y are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
end;
end;
theorem Th21: :: PENCIL_3:21
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 non trivial-yielding Segre-like 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 be non empty set ; ::_thesis: 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 non trivial-yielding Segre-like 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 ) ) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 holds
( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like 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 ) ) ) )
let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 misses B2 implies ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like 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 ) ) ) ) )
consider L1 being non trivial-yielding Segre-like 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 ; ::_thesis: ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like 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 ) ) ) )
thus ( B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like 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 ) ) ) ) ::_thesis: ( ( for b1, b2 being non trivial-yielding Segre-like 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 ) ) ) ) implies B1 '||' B2 )
proof
assume A3: B1 '||' B2 ; ::_thesis: for b1, b2 being non trivial-yielding Segre-like 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 ) ) )
consider L2 being non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & B2 = product b2 implies ( 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 ) ) ) )
assume that
A8: B1 = product b1 and
A9: B2 = product b2 ; ::_thesis: ( 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 ) ) )
A10: b1 = L1 by A8, A6, PUA2MSS1:2;
thus A11: indx b1 = indx b2 ::_thesis: 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 indx b1 <> indx b2 ; ::_thesis: contradiction
then b2 . (indx b1) is 1 -element by PENCIL_1:12;
then consider c2 being set such that
A12: b2 . (indx b1) = {c2} by ZFMISC_1:131;
set bl = the Block of (A . (indx b1));
consider p0 being set such that
A13: p0 in B1 by A8, XBOOLE_0:def_1;
reconsider p0 = p0 as Point of (Segre_Product A) by A13;
reconsider p = p0 as Element of Carrier A by Th6;
the Block of (A . (indx b1)) in the topology of (A . (indx b1)) ;
then ( 2 c= card the Block of (A . (indx b1)) & card the Block of (A . (indx b1)) c= card the carrier of (A . (indx b1)) ) by CARD_1:11, PENCIL_1:def_6;
then consider a being set such that
A14: a in the carrier of (A . (indx b1)) and
A15: a <> c2 by PENCIL_1:3, XBOOLE_1:1;
reconsider a = 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__::_thesis:_for_i_being_set_st_i_in_dom_x1_holds_
x1_._i_in_b1_._i
let i be set ; ::_thesis: ( i in dom x1 implies x1 . b1 in b1 . b1 )
assume A17: i in dom x1 ; ::_thesis: x1 . b1 in b1 . b1
then i in I ;
then A18: i in dom p by PARTFUN1:def_2;
percases ( i = indx b1 or i <> indx b1 ) ;
supposeA19: i = indx b1 ; ::_thesis: x1 . b1 in b1 . b1
then x1 . i = a by A18, FUNCT_7:31;
hence x1 . i in b1 . i by A7, A10, A19; ::_thesis: verum
end;
suppose i <> indx b1 ; ::_thesis: x1 . b1 in b1 . 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 set 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; ::_thesis: verum
end;
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, Def2;
reconsider y1 = y as Element of Carrier A by Th6;
percases ( y = x or y <> x ) ;
suppose y = x ; ::_thesis: contradiction
then y in B1 /\ B2 by A21, A22, XBOOLE_0:def_4;
hence contradiction by A2, XBOOLE_0:def_7; ::_thesis: verum
end;
suppose y <> x ; ::_thesis: contradiction
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__::_thesis:_for_i_being_set_st_i_in_dom_y1_holds_
y1_._i_in_b1_._i
let i be set ; ::_thesis: ( i in dom y1 implies y1 . b1 in b1 . b1 )
assume A26: i in dom y1 ; ::_thesis: y1 . b1 in b1 . b1
then reconsider i5 = i as Element of I ;
percases ( i = indx b1 or i <> indx b1 ) ;
supposeA27: i = indx b1 ; ::_thesis: y1 . b1 in b1 . 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; ::_thesis: verum
end;
supposeA28: i <> indx b1 ; ::_thesis: y1 . b1 in b1 . b1
( ex g being Function st
( g = y1 & dom g = dom b2 & ( for a being set 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 set 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; ::_thesis: verum
end;
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, XBOOLE_0:def_7; ::_thesis: verum
end;
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 ) ) ::_thesis: verum
proof
consider x being set such that
A33: x in B1 by A8, XBOOLE_0:def_1;
reconsider x = 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, Def2;
reconsider y1 = y as Element of Carrier A by Th6;
reconsider x1 = x as Element of Carrier A by Th6;
now__::_thesis:_not_x_=_y
assume x = y ; ::_thesis: contradiction
then B1 /\ B2 <> {} by A33, A34, XBOOLE_0:def_4;
hence contradiction by A2, XBOOLE_0:def_7; ::_thesis: verum
end;
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 ; ::_thesis: ( 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 ) )
now__::_thesis:_not_r_=_indx_b1
assume A38: r = indx b1 ; ::_thesis: contradiction
A39: now__::_thesis:_for_o_being_set_st_o_in_dom_b1_holds_
y1_._o_in_b1_._o
let o be set ; ::_thesis: ( o in dom b1 implies y1 . b1 in b1 . b1 )
assume A40: o in dom b1 ; ::_thesis: y1 . b1 in b1 . b1
then reconsider o1 = o as Element of I ;
percases ( o1 = r or o1 <> r ) ;
supposeA41: o1 = r ; ::_thesis: y1 . b1 in b1 . b1
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; ::_thesis: verum
end;
supposeA42: o1 <> r ; ::_thesis: y1 . b1 in b1 . b1
then b1 . o1 is 1 -element by A38, PENCIL_1:12;
then consider c being set 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; ::_thesis: verum
end;
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, XBOOLE_0:def_7; ::_thesis: verum
end;
hence r <> indx b1 ; ::_thesis: ( ( 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 ) )
thus for i being Element of I st i <> r holds
b1 . i = b2 . i ::_thesis: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear
proof
let i be Element of I; ::_thesis: ( i <> r implies b1 . i = b2 . i )
assume A44: i <> r ; ::_thesis: b1 . i = b2 . i
percases ( i = indx b1 or i <> indx b1 ) ;
suppose i = indx b1 ; ::_thesis: b1 . i = b2 . i
hence b1 . i = b2 . i by A7, A5, A10, A32, A11; ::_thesis: verum
end;
supposeA45: i <> indx b1 ; ::_thesis: b1 . i = b2 . i
then b2 . i is 1 -element by A11, PENCIL_1:12;
then A46: ex d being set 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 set 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 b1 . i = b2 . i by A48, A46, A47, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
let c1, c2 be Point of (A . r); ::_thesis: ( b1 . r = {c1} & b2 . r = {c2} implies c1,c2 are_collinear )
assume that
A49: b1 . r = {c1} and
A50: b2 . r = {c2} ; ::_thesis: c1,c2 are_collinear
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 c1,c2 are_collinear by A36, A51; ::_thesis: verum
end;
end;
consider L2 being non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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 ) ) ) ; ::_thesis: B1 '||' B2
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 set 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 by PBOOLE:def_2;
then {c2} c= [#] (A . r) by A57, Th7;
then reconsider c2 = c2 as Point of (A . r) by ZFMISC_1:31;
L1 . r is 1 -element by A54, PENCIL_1:12;
then consider c1 being set 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 by PBOOLE:def_2;
then {c1} c= [#] (A . r) by A58, Th7;
then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;
A59: now__::_thesis:_not_c1_=_c2
assume A60: c1 = c2 ; ::_thesis: contradiction
A61: now__::_thesis:_for_s_being_set_st_s_in_dom_L1_holds_
L1_._s_=_L2_._s
let s be set ; ::_thesis: ( s in dom L1 implies L1 . b1 = L2 . b1 )
assume s in dom L1 ; ::_thesis: L1 . b1 = L2 . b1
then reconsider s1 = s as Element of I ;
percases ( s1 = r or s1 <> r ) ;
suppose s1 = r ; ::_thesis: L1 . b1 = L2 . b1
hence L1 . s = L2 . s by A58, A57, A60; ::_thesis: verum
end;
suppose s1 <> r ; ::_thesis: L1 . b1 = L2 . b1
hence L1 . s = L2 . s by A55; ::_thesis: verum
end;
end;
end;
dom L1 = I by PARTFUN1:def_2
.= dom L2 by PARTFUN1:def_2 ;
then L1 = L2 by A61, FUNCT_1:2;
then B1 /\ B1 = {} by A2, A1, A52, XBOOLE_0:def_7;
hence contradiction by A1; ::_thesis: verum
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 be Point of (Segre_Product A); :: according to PENCIL_3:def_2 ::_thesis: ( x in B1 implies ex y being Point of (Segre_Product A) st
( y in B2 & x,y are_collinear ) )
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 ; ::_thesis: ex y being Point of (Segre_Product A) st
( y in B2 & x,y are_collinear )
then A63: ex x2 being Function st
( x2 = x & dom x2 = dom L1 & ( for o being set st o in dom L1 holds
x2 . o in L1 . o ) ) by A1, CARD_3:def_5;
A64: now__::_thesis:_for_a_being_set_st_a_in_dom_L2_holds_
y1_._a_in_L2_._a
let a be set ; ::_thesis: ( a in dom L2 implies y1 . b1 in L2 . b1 )
assume a in dom L2 ; ::_thesis: y1 . b1 in L2 . b1
then reconsider a1 = a as Element of I ;
percases ( a1 = r or a1 <> r ) ;
supposeA65: a1 = r ; ::_thesis: y1 . b1 in L2 . b1
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; ::_thesis: verum
end;
supposeA66: a1 <> r ; ::_thesis: y1 . b1 in L2 . b1
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; ::_thesis: verum
end;
end;
end;
take y ; ::_thesis: ( y in B2 & x,y are_collinear )
dom y1 = I by PARTFUN1:def_2
.= dom L2 by PARTFUN1:def_2 ;
hence y in B2 by A52, A64, CARD_3:def_5; ::_thesis: x,y are_collinear
reconsider B = product ({x1} +* (r,bb)) as Block of (Segre_Product A) by Th16;
A67: now__::_thesis:_for_s_being_set_st_s_in_dom_y1_holds_
y1_._s_in_({x1}_+*_(r,bb))_._s
let s be set ; ::_thesis: ( s in dom y1 implies y1 . b1 in ({x1} +* (r,bb)) . b1 )
assume s in dom y1 ; ::_thesis: y1 . b1 in ({x1} +* (r,bb)) . b1
then A68: s in I ;
then A69: ( s in dom {x1} & s in dom x1 ) by PARTFUN1:def_2;
percases ( s = r or s <> r ) ;
suppose s = r ; ::_thesis: y1 . b1 in ({x1} +* (r,bb)) . b1
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; ::_thesis: verum
end;
supposeA70: s <> r ; ::_thesis: y1 . b1 in ({x1} +* (r,bb)) . b1
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; ::_thesis: verum
end;
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__::_thesis:_for_s_being_set_st_s_in_dom_x1_holds_
x1_._s_in_({x1}_+*_(r,bb))_._s
let s be set ; ::_thesis: ( s in dom x1 implies x1 . b1 in ({x1} +* (r,bb)) . b1 )
assume A74: s in dom x1 ; ::_thesis: x1 . b1 in ({x1} +* (r,bb)) . b1
then A75: s in I ;
then A76: s in dom {x1} by PARTFUN1:def_2;
percases ( s = r or s <> r ) ;
supposeA77: s = r ; ::_thesis: x1 . b1 in ({x1} +* (r,bb)) . b1
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; ::_thesis: verum
end;
suppose s <> r ; ::_thesis: x1 . b1 in ({x1} +* (r,bb)) . b1
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; ::_thesis: verum
end;
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 x,y are_collinear by PENCIL_1:def_1; ::_thesis: verum
end;
theorem Th22: :: PENCIL_3:22
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds
for i being Element of I
for p being Point of (A . i)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds
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 holds
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 non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds
for i being Element of I
for p being Point of (A . i)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is connected ) implies for i being Element of I
for p being Point of (A . i)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
assume A1: for i being Element of I holds A . i is connected ; ::_thesis: for i being Element of I
for p being Point of (A . i)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
let i be Element of I; ::_thesis: for p being Point of (A . i)
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
let p be Point of (A . i); ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i implies 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
assume that
A2: product b2 is Segre-Coset of A and
A3: b1 = b2 +* (i,{p}) and
A4: not p in b2 . i ; ::_thesis: 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
defpred S1[ set , set ] means for a, b being Point of (A . i) st $1 = a & $2 = b holds
a,b are_collinear ;
A5: now__::_thesis:_not_i_=_indx_b2
assume i = indx b2 ; ::_thesis: contradiction
then b2 . i = [#] (A . i) by A2, Th10;
hence contradiction by A4; ::_thesis: verum
end;
then b2 . i is 1 -element by PENCIL_1:12;
then consider q being set 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 by PBOOLE:def_2;
then {q} c= [#] (A . i) by A6, Th7;
then reconsider q = 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 holds
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
for x, y being set st 1 <= j & j < len f & x = f . j & y = f . (j + 1) holds
S1[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
S1[F . j,F . (j + 1)] ) ) from PENCIL_2:sch_1(A7, A9);
A11: now__::_thesis:_not_F_=_{}
assume F = {} ; ::_thesis: contradiction
then dom F = {} ;
then ( F . 1 = {} & F . (len F) = {} ) by FUNCT_1:def_2;
hence contradiction by A4, A6, A10, TARSKI:def_1; ::_thesis: verum
end;
deffunc H1( set ) -> 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 = H1(j) ) ) from FINSEQ_1:sch_2();
rng G c= bool the carrier of (Segre_Product A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng G or a in bool the carrier of (Segre_Product A) )
assume a in rng G ; ::_thesis: a in bool the carrier of (Segre_Product A)
then consider o being set such that
A13: o in dom G and
A14: G . o = a by FUNCT_1:def_3;
reconsider o = 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 a in bool the carrier of (Segre_Product A) by A14, A15; ::_thesis: verum
end;
then reconsider D = G as FinSequence of bool the carrier of (Segre_Product A) by FINSEQ_1:def_4;
take D ; ::_thesis: ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
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; ::_thesis: ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
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; ::_thesis: ( ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
thus for j being Nat st j in dom D holds
D . j is Segre-Coset of A ::_thesis: for i being Nat st 1 <= i & i < len D holds
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; ::_thesis: ( j in dom D implies D . j is Segre-Coset of A )
assume A17: j in dom D ; ::_thesis: D . j is Segre-Coset of A
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 non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;
BB . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;
then not BB . (indx b2) is 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 D . j is Segre-Coset of A by A20, A19, PENCIL_2:def_2; ::_thesis: verum
end;
A21: dom b2 = I by PARTFUN1:def_2;
thus for i being Nat st 1 <= i & i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ::_thesis: verum
proof
let j be Nat; ::_thesis: ( 1 <= j & j < len D implies for Di, Di1 being Segre-Coset of A st Di = D . j & Di1 = D . (j + 1) holds
( Di misses Di1 & Di '||' Di1 ) )
assume A22: ( 1 <= j & j < len D ) ; ::_thesis: for Di, Di1 being Segre-Coset of A st Di = D . j & Di1 = D . (j + 1) holds
( Di misses Di1 & Di '||' Di1 )
let Di, Di1 be Segre-Coset of A; ::_thesis: ( Di = D . j & Di1 = D . (j + 1) implies ( Di misses Di1 & Di '||' Di1 ) )
assume that
A23: Di = D . j and
A24: Di1 = D . (j + 1) ; ::_thesis: ( Di misses Di1 & Di '||' Di1 )
reconsider j = 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 non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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 ::_thesis: Di '||' Di1
proof
A32: j <> j + 1 ;
assume Di /\ Di1 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being set 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 set 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 set 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; ::_thesis: verum
end;
now__::_thesis:_for_c1,_c2_being_non_trivial-yielding_Segre-like_ManySortedSubset_of_Carrier_A_st_Di_=_product_c1_&_Di1_=_product_c2_holds_
(_indx_c1_=_indx_c2_&_ex_r_being_Element_of_I_st_
(_r_<>_indx_c1_&_(_for_j_being_Element_of_I_st_j_<>_r_holds_
c1_._j_=_c2_._j_)_&_(_for_p1,_p2_being_Point_of_(A_._r)_st_c1_._r_=_{p1}_&_c2_._r_=_{p2}_holds_
p1,p2_are_collinear_)_)_)
let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( Di = product c1 & Di1 = product c2 implies ( indx c1 = indx c2 & ex r being Element of I st
( r <> indx c1 & ( for j being Element of I st j <> r holds
c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear ) ) ) )
assume that
A40: Di = product c1 and
A41: Di1 = product c2 ; ::_thesis: ( indx c1 = indx c2 & ex r being Element of I st
( r <> indx c1 & ( for j being Element of I st j <> r holds
c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear ) ) )
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: not c2 . (indx b2) is 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: not c1 . (indx b2) is 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; ::_thesis: ex r being Element of I st
( r <> indx c1 & ( for j being Element of I st j <> r holds
c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear ) )
take r = i; ::_thesis: ( r <> indx c1 & ( for j being Element of I st j <> r holds
c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear ) )
thus r <> indx c1 by A5, A45, PENCIL_1:def_21; ::_thesis: ( ( for j being Element of I st j <> r holds
c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear ) )
thus for j being Element of I st j <> r holds
c1 . j = c2 . j ::_thesis: for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear
proof
let j be Element of I; ::_thesis: ( j <> r implies c1 . j = c2 . j )
assume A46: j <> r ; ::_thesis: c1 . j = c2 . j
hence c1 . j = b2 . j by A44, FUNCT_7:32
.= c2 . j by A42, A46, FUNCT_7:32 ;
::_thesis: verum
end;
thus for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear ::_thesis: verum
proof
let p1, p2 be Point of (A . r); ::_thesis: ( c1 . r = {p1} & c2 . r = {p2} implies p1,p2 are_collinear )
assume that
A47: c1 . r = {p1} and
A48: c2 . r = {p2} ; ::_thesis: p1,p2 are_collinear
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 p1,p2 are_collinear by A10, A12, A22, A49; ::_thesis: verum
end;
end;
hence Di '||' Di1 by A31, Th21; ::_thesis: verum
end;
end;
theorem Th23: :: PENCIL_3:23
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds
for B1, B2 being Segre-Coset of A st B1 misses B2 holds
for b1, b2 being non trivial-yielding Segre-like 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 holds
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 non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds
for B1, B2 being Segre-Coset of A st B1 misses B2 holds
for b1, b2 being non trivial-yielding Segre-like 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is connected ) implies for B1, B2 being Segre-Coset of A st B1 misses B2 holds
for b1, b2 being non trivial-yielding Segre-like 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) ) )
assume A1: for i being Element of I holds A . i is connected ; ::_thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 holds
for b1, b2 being non trivial-yielding Segre-like 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 misses B2 implies for b1, b2 being non trivial-yielding Segre-like 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) ) )
assume A2: B1 misses B2 ; ::_thesis: for b1, b2 being non trivial-yielding Segre-like 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & B2 = product b2 implies ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) ) )
assume that
A3: B1 = product b1 and
A4: B2 = product b2 ; ::_thesis: ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) ) ::_thesis: ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) implies indx b1 = indx b2 )
proof
defpred S1[ Nat] means for c1, c2 being non trivial-yielding Segre-like 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 holds
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) );
A5: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( 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) = k + 1 implies 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
assume 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 ; ::_thesis: 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
{ i where i is Element of I : c1 . i <> c2 . i } <> {} by A10;
then consider j0 being set 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 set 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, PBOOLE:def_2;
then p in (Carrier A) . j by ZFMISC_1:31;
then p in [#] (A . j) by Th7;
then reconsider p = p as Point of (A . j) ;
reconsider c3 = c2 +* (j,{p}) as non trivial-yielding Segre-like 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 set st c2 . j = {r} by ZFMISC_1:131;
not A . (indx c1) is 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;
percases ( product c1 misses product c3 or product c1 meets product c3 ) ;
supposeA20: product c1 misses product c3 ; ::_thesis: 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
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 holds
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 holds
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__::_thesis:_not_len_F_=_1
dom c2 = I by PARTFUN1:def_2;
then A30: c3 . j = {p} by FUNCT_7:31;
assume len F = 1 ; ::_thesis: contradiction
hence contradiction by A12, A15, A25, A26, A30, PUA2MSS1:2; ::_thesis: verum
end;
reconsider D = E ^' F as FinSequence of bool the carrier of (Segre_Product A) ;
take D ; ::_thesis: ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
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, GRAPH_2:14; ::_thesis: ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
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, GRAPH_2:16; ::_thesis: ( ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
thus for i being Nat st i in dom D holds
D . i is Segre-Coset of A ::_thesis: for i being Nat st 1 <= i & i < len D holds
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; ::_thesis: ( i in dom D implies D . i is Segre-Coset of A )
A33: rng D c= (rng E) \/ (rng F) by GRAPH_2:17;
assume i in dom D ; ::_thesis: D . i is Segre-Coset of A
then A34: D . i in rng D by FUNCT_1:3;
percases ( D . i in rng E or D . i in rng F ) by A34, A33, XBOOLE_0:def_3;
suppose D . i in rng E ; ::_thesis: D . i is Segre-Coset of A
then consider i0 being set such that
A35: i0 in dom E and
A36: D . i = E . i0 by FUNCT_1:def_3;
thus D . i is Segre-Coset of A by A23, A35, A36; ::_thesis: verum
end;
suppose D . i in rng F ; ::_thesis: D . i is Segre-Coset of A
then consider i0 being set such that
A37: i0 in dom F and
A38: D . i = F . i0 by FUNCT_1:def_3;
thus D . i is Segre-Coset of A by A27, A37, A38; ::_thesis: verum
end;
end;
end;
thus for i being Nat st 1 <= i & i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ::_thesis: verum
proof
let i be Nat; ::_thesis: ( 1 <= i & i < len D implies for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) )
assume that
A39: 1 <= i and
A40: i < len D ; ::_thesis: for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 )
let Di, Di1 be Segre-Coset of A; ::_thesis: ( Di = D . i & Di1 = D . (i + 1) implies ( Di misses Di1 & Di '||' Di1 ) )
assume that
A41: Di = D . i and
A42: Di1 = D . (i + 1) ; ::_thesis: ( Di misses Di1 & Di '||' Di1 )
reconsider i = i as Element of NAT by ORDINAL1:def_12;
percases ( i < len E or i >= len E ) ;
supposeA43: i < len E ; ::_thesis: ( Di misses Di1 & Di '||' Di1 )
then i + 1 <= len E by NAT_1:13;
then A44: Di1 = E . (i + 1) by A42, GRAPH_2:14, NAT_1:11;
Di = E . i by A39, A41, A43, GRAPH_2:14;
hence ( Di misses Di1 & Di '||' Di1 ) by A24, A39, A43, A44; ::_thesis: verum
end;
suppose i >= len E ; ::_thesis: ( Di misses Di1 & Di '||' Di1 )
then consider k being Nat such that
A45: i = (len E) + k by NAT_1:10;
A46: F <> {} by A31;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
percases ( k > 0 or k = 0 ) ;
supposeA47: k > 0 ; ::_thesis: ( Di misses Di1 & Di '||' Di1 )
((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, GRAPH_2:13;
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, GRAPH_2:15, NAT_1:11;
0 + 1 <= k by A47, NAT_1:13;
then A52: Di = F . (k + 1) by A41, A45, A50, GRAPH_2:15;
( 1 <= k + 1 & k + 1 < len F ) by A48, NAT_1:11, XREAL_1:6;
hence ( Di misses Di1 & Di '||' Di1 ) by A28, A52, A51; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: ( Di misses Di1 & Di '||' Di1 )
then ( Di = F . 1 & Di1 = F . (1 + 1) ) by A22, A25, A32, A39, A41, A42, A45, GRAPH_2:14, GRAPH_2:15;
hence ( Di misses Di1 & Di '||' Di1 ) by A28, A32; ::_thesis: verum
end;
end;
end;
end;
end;
end;
supposeA53: product c1 meets product c3 ; ::_thesis: 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
not p in c2 . j by A12, A15, A17, TARSKI:def_1;
hence 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) by A1, A8, A9, A18, A19, A53, Th11, Th22; ::_thesis: verum
end;
end;
end;
end;
A54: S1[ 0 ]
proof
let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( 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) = 0 implies 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) )
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 ; ::_thesis: 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
A57: now__::_thesis:_for_a_being_set_st_a_in_dom_c1_holds_
not_c1_._a_<>_c2_._a
let a be set ; ::_thesis: ( a in dom c1 implies not c1 . a <> c2 . a )
assume a in dom c1 ; ::_thesis: not c1 . a <> c2 . a
then reconsider j = a as Element of I ;
assume c1 . a <> c2 . a ; ::_thesis: contradiction
then j in { i where i is Element of I : c1 . i <> c2 . i } ;
hence contradiction by A56; ::_thesis: verum
end;
dom c1 = I by PARTFUN1:def_2
.= dom c2 by PARTFUN1:def_2 ;
hence 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) by A55, A57, FUNCT_1:2; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A54, A5);
then A58: S1[ diff (b1,b2)] ;
assume indx b1 = indx b2 ; ::_thesis: 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
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 holds
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 ; ::_thesis: ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
thus ( D . 1 = B1 & D . (len D) = B2 ) by A3, A4, A59; ::_thesis: ( ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) )
thus ( ( 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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ) ) by A60; ::_thesis: verum
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 holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) ; ::_thesis: indx b1 = indx b2
defpred S1[ Nat] means for bb being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product bb = D . $1 holds
indx b1 = indx bb;
A65: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A66: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product bb = D . (k + 1) implies indx b1 = indx bb )
assume A67: product bb = D . (k + 1) ; ::_thesis: indx b1 = indx bb
A68: k + 1 in dom D by A67, FUNCT_1:def_2;
then A69: k + 1 <= len D by FINSEQ_3:25;
percases ( k = 0 or 0 < k ) ;
suppose k = 0 ; ::_thesis: indx b1 = indx bb
hence indx b1 = indx bb by A3, A61, A67, PUA2MSS1:2; ::_thesis: verum
end;
suppose 0 < k ; ::_thesis: indx b1 = indx bb
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 non trivial-yielding Segre-like 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 indx b1 = indx bb by A67, A71, A72, Th21; ::_thesis: verum
end;
end;
end;
end;
A73: S1[ 0 ]
proof
A74: not 0 in dom D by FINSEQ_3:24;
let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product bb = D . 0 implies indx b1 = indx bb )
assume product bb = D . 0 ; ::_thesis: indx b1 = indx bb
hence indx b1 = indx bb by A74, FUNCT_1:def_2; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A73, A65);
hence indx b1 = indx b2 by A4, A62; ::_thesis: verum
end;
theorem Th24: :: PENCIL_3:24
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
proof
let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4 )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
A2: now__::_thesis:_for_i_being_Element_of_I_holds_A_._i_is_connected
let i be Element of I; ::_thesis: A . i is connected
A . i is strongly_connected by A1;
hence A . i is connected by Th4; ::_thesis: verum
end;
let f be Collineation of (Segre_Product A); ::_thesis: for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let B1, B2 be Segre-Coset of A; ::_thesis: for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4
let b1, b2, b3, b4 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 implies indx b3 = indx b4 )
assume that
A3: B1 = product b1 and
A4: B2 = product b2 and
A5: ( f .: B1 = product b3 & f .: B2 = product b4 ) ; ::_thesis: ( not indx b1 = indx b2 or indx b3 = indx b4 )
assume A6: indx b1 = indx b2 ; ::_thesis: indx b3 = indx b4
percases ( B1 misses B2 or B1 meets B2 ) ;
supposeA7: B1 misses B2 ; ::_thesis: indx b3 = indx b4
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 holds
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 H1( Nat) -> Element of bool the carrier of (Segre_Product A) = 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 = H1(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 holds
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; ::_thesis: ( 1 <= i & i < len E implies for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 ) )
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 ) ; ::_thesis: for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 )
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; ::_thesis: ( Ei = E . i & Ei1 = E . (i + 1) implies ( Ei misses Ei1 & Ei '||' Ei1 ) )
assume that
A18: Ei = E . i and
A19: Ei1 = E . (i + 1) ; ::_thesis: ( Ei misses Ei1 & Ei '||' Ei1 )
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; ::_thesis: Ei '||' Ei1
Di '||' Di1 by A12, A13, A17;
hence Ei '||' Ei1 by A20, A21, Th20; ::_thesis: verum
end;
A22: for i being Nat st i in dom E holds
E . i is Segre-Coset of A
proof
let i be Nat; ::_thesis: ( i in dom E implies E . i is Segre-Coset of A )
assume A23: i in dom E ; ::_thesis: E . i is Segre-Coset of A
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 E . i is Segre-Coset of A by A1, PENCIL_2:24; ::_thesis: verum
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 indx b3 = indx b4 by A2, A5, A24, A22, A15, A8, Th23; ::_thesis: verum
end;
suppose B1 meets B2 ; ::_thesis: indx b3 = indx b4
then B1 = B2 by A3, A4, A6, Th11;
hence indx b3 = indx b4 by A5, PUA2MSS1:2; ::_thesis: verum
end;
end;
end;
theorem Th25: :: PENCIL_3:25
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
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 non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
proof
let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
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 non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies 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 non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: 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 non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
let f be Collineation of (Segre_Product A); ::_thesis: 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 non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j )
defpred S1[ set , set ] means for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = $1 holds
indx b2 = $2;
A2: for x, y, x9 being Element of I st S1[x,y] & S1[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; ::_thesis: ( S1[x,y] & S1[x9,y] implies x = x9 )
assume that
A3: for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds
indx b2 = y and
A4: for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x9 holds
indx b2 = y ; ::_thesis: x = x9
consider b1 being non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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 " 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, XBOOLE_0:def_10;
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, XBOOLE_0:def_10;
indx L1 = y by A3, A5, A7;
hence x = x9 by A1, A5, A7, A8, A10, A11, A19, A17, Th24; ::_thesis: verum
end;
A20: for y being Element of I ex x being Element of I st S1[x,y]
proof
set p0 = the Point of (Segre_Product A);
reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;
let x be Element of I; ::_thesis: ex x being Element of I st S1[x,x]
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 not A . x is trivial by PENCIL_1:def_18;
then reconsider C = [#] (A . x) as non trivial set ;
reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1: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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) )
assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A)
then consider f being Function such that
A23: a = f and
A24: dom f = dom b and
A25: for x being set 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__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_
f_._i_in_(Carrier_A)_._i
let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 )
assume A28: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1
then reconsider i1 = i as Element of I ;
A29: f . i in b . i by A24, A25, A26, A28;
percases ( i1 = x or i1 <> x ) ;
suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1
hence f . i in (Carrier A) . i by A21, A29, Th7; ::_thesis: verum
end;
suppose i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1
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;
not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A30; ::_thesis: verum
end;
end;
end;
Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23;
hence a in the carrier of (Segre_Product A) by A23, A26, A27, CARD_3:def_5; ::_thesis: verum
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 non trivial-yielding Segre-like 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; ::_thesis: S1[y,x]
let B1 be Segre-Coset of A; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = y holds
indx b2 = x
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y implies indx b2 = x )
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 ) ; ::_thesis: indx b2 = x
hence indx b2 = x by A1, A22, A31, A32, Th24; ::_thesis: verum
end;
A33: for x being Element of I ex y being Element of I st S1[x,y]
proof
set p0 = the Point of (Segre_Product A);
reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;
let x be Element of I; ::_thesis: ex y being Element of I st S1[x,y]
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 not A . x is trivial by PENCIL_1:def_18;
then reconsider C = [#] (A . x) as non trivial set ;
reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1: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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) )
assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A)
then consider f being Function such that
A36: a = f and
A37: dom f = dom b and
A38: for x being set 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__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_
f_._i_in_(Carrier_A)_._i
let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 )
assume A41: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1
then reconsider i1 = i as Element of I ;
A42: f . i in b . i by A37, A38, A39, A41;
percases ( i1 = x or i1 <> x ) ;
suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1
hence f . i in (Carrier A) . i by A34, A42, Th7; ::_thesis: verum
end;
suppose i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1
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;
not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A43; ::_thesis: verum
end;
end;
end;
Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23;
hence a in the carrier of (Segre_Product A) by A36, A39, A40, CARD_3:def_5; ::_thesis: verum
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 non trivial-yielding Segre-like 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 ; ::_thesis: S1[x, indx b0]
let B1 be Segre-Coset of A; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds
indx b2 = indx b0
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x implies indx b2 = indx b0 )
assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x ) ; ::_thesis: indx b2 = indx b0
hence indx b2 = indx b0 by A1, A35, A44, Th24; ::_thesis: verum
end;
A45: for x, y, y9 being Element of I st S1[x,y] & S1[x,y9] holds
y = y9
proof
let x, y, y9 be Element of I; ::_thesis: ( S1[x,y] & S1[x,y9] implies y = y9 )
assume that
A46: for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds
indx b2 = y and
A47: for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds
indx b2 = y9 ; ::_thesis: y = y9
consider b1 being non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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 y = y9 by A47, A48, A50; ::_thesis: verum
end;
thus ex f being Permutation of I st
for x, y being Element of I holds
( f . x = y iff S1[x,y] ) from TRANSGEO:sch_1(A33, A20, A2, A45); ::_thesis: verum
end;
definition
let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume B1: 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: :: PENCIL_3:def 3
for i, j being Element of I holds
( it . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j );
existence
ex b1 being Permutation of I st
for i, j being Element of I holds
( b1 . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) by B1, Th25;
uniqueness
for b1, b2 being Permutation of I st ( for i, j being Element of I holds
( b1 . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) & ( for i, j being Element of I holds
( b2 . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) holds
b1 = b2
proof
let s, t be Permutation of I; ::_thesis: ( ( for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) & ( for i, j being Element of I holds
( t . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) implies s = t )
assume that
A1: for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) and
A2: for i, j being Element of I holds
( t . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ; ::_thesis: s = t
A3: now__::_thesis:_for_a_being_set_st_a_in_I_holds_
s_._a_=_t_._a
let a be set ; ::_thesis: ( a in I implies s . a = t . a )
assume a in I ; ::_thesis: s . a = t . a
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 non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A4: indx b1 = i and
A5: product b1 is Segre-Coset of A by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A5;
reconsider fB = f .: B1 as Segre-Coset of A by B1, PENCIL_2:24;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A6: fB = product b2 and
b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def_2;
j1 = indx b2 by A1, A4, A6
.= j2 by A2, A4, A6 ;
hence s . a = t . a ; ::_thesis: verum
end;
( dom s = I & dom t = I ) by FUNCT_2:def_1;
hence s = t by A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines permutation_of_indices PENCIL_3:def_3_:_
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for b4 being Permutation of I holds
( b4 = permutation_of_indices f iff for i, j being Element of I holds
( b4 . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) );
begin
definition
let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume B1: for i being Element of I holds A . i is strongly_connected ;
let f be Collineation of (Segre_Product A);
let b1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A;
assume B2: 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: :: PENCIL_3:def 4
( it is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = it . (a . (indx b1)) ) );
existence
ex b1 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st
( b1 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = b1 . (a . (indx b1)) ) )
proof
reconsider B1 = product b1 as Segre-Coset of A by B2;
set s = permutation_of_indices f;
set i = indx b1;
defpred S1[ set , set ] means for J being ManySortedSet of I st J in f .: (product (b1 +* ((indx b1),{$1}))) holds
$2 = J . ((permutation_of_indices f) . (indx b1));
set B = the carrier of (A . (indx b1));
set t = permutation_of_indices f;
reconsider B2 = f .: B1 as Segre-Coset of A by B1, PENCIL_2:24;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A1: product b2 = B2 and
A2: b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def_2;
set j = indx b2;
A3: f is bijective by PENCIL_2:def_4;
then A4: f " B2 c= B1 by FUNCT_1:82;
A5: Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23;
A6: for x being set st x in the carrier of (A . (indx b1)) holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of (A . (indx b1)) implies ex y being set st S1[x,y] )
consider bb being set such that
A7: bb in B1 by XBOOLE_0:def_1;
A8: ex bf being Function st
( bf = bb & dom bf = dom b1 & ( for o being set st o in dom b1 holds
bf . o in b1 . o ) ) by A7, CARD_3:def_5;
A9: dom b1 = I by PARTFUN1:def_2;
then reconsider bb = bb as ManySortedSet of I by A8, PARTFUN1:def_2, RELAT_1:def_18;
set bbx = bb +* ((indx b1),x);
A10: {(bb +* ((indx b1),x))} = product (b1 +* ((indx b1),{x}))
proof
thus {(bb +* ((indx b1),x))} c= product (b1 +* ((indx b1),{x})) :: according to XBOOLE_0:def_10 ::_thesis: product (b1 +* ((indx b1),{x})) c= {(bb +* ((indx b1),x))}
proof
A11: now__::_thesis:_for_z_being_set_st_z_in_dom_(b1_+*_((indx_b1),{x}))_holds_
(bb_+*_((indx_b1),x))_._z_in_(b1_+*_((indx_b1),{x}))_._z
let z be set ; ::_thesis: ( z in dom (b1 +* ((indx b1),{x})) implies (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 )
assume z in dom (b1 +* ((indx b1),{x})) ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
then A12: z in I ;
then A13: z in dom bb by PARTFUN1:def_2;
percases ( z = indx b1 or z <> indx b1 ) ;
supposeA14: z = indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
then (bb +* ((indx b1),x)) . z = x by A13, FUNCT_7:31;
then (bb +* ((indx b1),x)) . z in {x} by TARSKI:def_1;
hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A9, A14, FUNCT_7:31; ::_thesis: verum
end;
supposeA15: z <> indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1
then (bb +* ((indx b1),x)) . z = bb . z by FUNCT_7:32;
then (bb +* ((indx b1),x)) . z in b1 . z by A7, A9, A12, CARD_3:9;
hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A15, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in {(bb +* ((indx b1),x))} or o in product (b1 +* ((indx b1),{x})) )
assume o in {(bb +* ((indx b1),x))} ; ::_thesis: o in product (b1 +* ((indx b1),{x}))
then A16: o = bb +* ((indx b1),x) by TARSKI:def_1;
dom (bb +* ((indx b1),x)) = I by PARTFUN1:def_2
.= dom (b1 +* ((indx b1),{x})) by PARTFUN1:def_2 ;
hence o in product (b1 +* ((indx b1),{x})) by A16, A11, CARD_3:9; ::_thesis: verum
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in product (b1 +* ((indx b1),{x})) or o in {(bb +* ((indx b1),x))} )
assume o in product (b1 +* ((indx b1),{x})) ; ::_thesis: o in {(bb +* ((indx b1),x))}
then consider u being Function such that
A17: u = o and
A18: dom u = dom (b1 +* ((indx b1),{x})) and
A19: for z being set st z in dom (b1 +* ((indx b1),{x})) holds
u . z in (b1 +* ((indx b1),{x})) . z by CARD_3:def_5;
A20: now__::_thesis:_for_z_being_set_st_z_in_dom_u_holds_
u_._z_=_(bb_+*_((indx_b1),x))_._z
let z be set ; ::_thesis: ( z in dom u implies u . b1 = (bb +* ((indx b1),x)) . b1 )
assume A21: z in dom u ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1
then A22: z in I by A18;
reconsider zz = z as Element of I by A18, A21;
A23: u . z in (b1 +* ((indx b1),{x})) . z by A18, A19, A21;
percases ( zz = indx b1 or zz <> indx b1 ) ;
supposeA24: zz = indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1
then u . z in {x} by A9, A23, FUNCT_7:31;
then u . z = x by TARSKI:def_1;
hence u . z = (bb +* ((indx b1),x)) . z by A8, A9, A24, FUNCT_7:31; ::_thesis: verum
end;
supposeA25: zz <> indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1
then ( not b1 . zz is empty & b1 . zz is trivial ) by PENCIL_1:def_21;
then b1 . zz is 1 -element ;
then consider o being set such that
A26: b1 . z = {o} by ZFMISC_1:131;
u . z in b1 . z by A23, A25, FUNCT_7:32;
then A27: u . z = o by A26, TARSKI:def_1;
(bb +* ((indx b1),x)) . z = bb . z by A25, FUNCT_7:32;
then (bb +* ((indx b1),x)) . z in {o} by A8, A9, A22, A26;
hence u . z = (bb +* ((indx b1),x)) . z by A27, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
dom u = I by A18, PARTFUN1:def_2
.= dom (bb +* ((indx b1),x)) by PARTFUN1:def_2 ;
then u = bb +* ((indx b1),x) by A20, FUNCT_1:2;
hence o in {(bb +* ((indx b1),x))} by A17, TARSKI:def_1; ::_thesis: verum
end;
assume A28: x in the carrier of (A . (indx b1)) ; ::_thesis: ex y being set st S1[x,y]
A29: now__::_thesis:_for_o_being_set_st_o_in_dom_(Carrier_A)_holds_
(bb_+*_((indx_b1),x))_._o_in_(Carrier_A)_._o
let o be set ; ::_thesis: ( o in dom (Carrier A) implies (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1 )
assume A30: o in dom (Carrier A) ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1
then reconsider u = o as Element of I ;
percases ( u = indx b1 or u <> indx b1 ) ;
supposeA31: u = indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1
then (bb +* ((indx b1),x)) . u in [#] (A . (indx b1)) by A28, A8, A9, FUNCT_7:31;
hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A31, Th7; ::_thesis: verum
end;
supposeA32: u <> indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1
b1 c= Carrier A by PBOOLE:def_18;
then A33: b1 . o c= (Carrier A) . o by A30, PBOOLE:def_2;
(bb +* ((indx b1),x)) . u = bb . u by A32, FUNCT_7:32;
then (bb +* ((indx b1),x)) . u in b1 . u by A7, A9, CARD_3:9;
hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A33; ::_thesis: verum
end;
end;
end;
dom (bb +* ((indx b1),x)) = I by PARTFUN1:def_2
.= dom (Carrier A) by PARTFUN1:def_2 ;
then reconsider bbx1 = bb +* ((indx b1),x) as Point of (Segre_Product A) by A5, A29, CARD_3:9;
reconsider fbbx = f . bbx1 as ManySortedSet of I by PENCIL_1:14;
take fbbx . ((permutation_of_indices f) . (indx b1)) ; ::_thesis: S1[x,fbbx . ((permutation_of_indices f) . (indx b1))]
dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1;
then bbx1 in dom f ;
then A34: Im (f,(bb +* ((indx b1),x))) = {(f . (bb +* ((indx b1),x)))} by FUNCT_1:59;
let J be ManySortedSet of I; ::_thesis: ( J in f .: (product (b1 +* ((indx b1),{x}))) implies fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1)) )
assume J in f .: (product (b1 +* ((indx b1),{x}))) ; ::_thesis: fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1))
hence fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1)) by A10, A34, TARSKI:def_1; ::_thesis: verum
end;
consider M being Function such that
A35: ( dom M = the carrier of (A . (indx b1)) & ( for x being set st x in the carrier of (A . (indx b1)) holds
S1[x,M . x] ) ) from CLASSES1:sch_1(A6);
A36: dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1;
then B1 c= f " B2 by FUNCT_1:76;
then A37: f " B2 = B1 by A4, XBOOLE_0:def_10;
rng M c= the carrier of (A . ((permutation_of_indices f) . (indx b1)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng M or x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) )
assume x in rng M ; ::_thesis: x in the carrier of (A . ((permutation_of_indices f) . (indx b1)))
then consider o being set such that
A38: o in dom M and
A39: x = M . o by FUNCT_1:def_3;
reconsider o = o as Point of (A . (indx b1)) by A35, A38;
consider p being ManySortedSet of I such that
A40: p in product b1 and
A41: {(p +* ((indx b1),o))} = product (b1 +* ((indx b1),{o})) by Th18;
reconsider pio = p +* ((indx b1),o) as Point of (Segre_Product A) by B2, A40, PENCIL_1:25;
reconsider J = f . pio as ManySortedSet of I by PENCIL_1:14;
Im (f,(p +* ((indx b1),o))) = {(f . pio)} by A36, FUNCT_1:59;
then A42: J in f .: (product (b1 +* ((indx b1),{o}))) by A41, TARSKI:def_1;
(permutation_of_indices f) . (indx b1) in I ;
then (permutation_of_indices f) . (indx b1) in dom (Carrier A) by PARTFUN1:def_2;
then J . ((permutation_of_indices f) . (indx b1)) in (Carrier A) . ((permutation_of_indices f) . (indx b1)) by A5, CARD_3:9;
then J . ((permutation_of_indices f) . (indx b1)) in [#] (A . ((permutation_of_indices f) . (indx b1))) by Th7;
hence x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) by A35, A39, A42; ::_thesis: verum
end;
then reconsider M = M as Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) by A35, FUNCT_2:def_1, RELSET_1:4;
set m = M;
A43: indx b2 = (permutation_of_indices f) . (indx b1) by B1, A1, Def3;
A44: M is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom M or not x2 in dom M or not M . x1 = M . x2 or x1 = x2 )
assume that
A45: ( x1 in dom M & x2 in dom M ) and
A46: M . x1 = M . x2 ; ::_thesis: x1 = x2
reconsider o1 = x1, o2 = x2 as Point of (A . (indx b1)) by A45;
consider p1 being ManySortedSet of I such that
A47: p1 in product b1 and
A48: {(p1 +* ((indx b1),o1))} = product (b1 +* ((indx b1),{o1})) by Th18;
reconsider p1io = p1 +* ((indx b1),o1) as Point of (Segre_Product A) by B2, A47, PENCIL_1:25;
reconsider J1 = f . p1io as ManySortedSet of I by PENCIL_1:14;
consider p2 being ManySortedSet of I such that
A49: p2 in product b1 and
A50: {(p2 +* ((indx b1),o2))} = product (b1 +* ((indx b1),{o2})) by Th18;
A51: dom b1 = I by PARTFUN1:def_2;
A52: dom p1 = I by PARTFUN1:def_2;
A53: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
(p1_+*_((indx_b1),o1))_._o_in_b1_._o
let o be set ; ::_thesis: ( o in I implies (p1 +* ((indx b1),o1)) . b1 in b1 . b1 )
assume A54: o in I ; ::_thesis: (p1 +* ((indx b1),o1)) . b1 in b1 . b1
percases ( o = indx b1 or o <> indx b1 ) ;
supposeA55: o = indx b1 ; ::_thesis: (p1 +* ((indx b1),o1)) . b1 in b1 . b1
then (p1 +* ((indx b1),o1)) . o = o1 by A52, FUNCT_7:31;
then (p1 +* ((indx b1),o1)) . o in [#] (A . (indx b1)) ;
hence (p1 +* ((indx b1),o1)) . o in b1 . o by B2, A55, Th10; ::_thesis: verum
end;
suppose o <> indx b1 ; ::_thesis: (p1 +* ((indx b1),o1)) . b1 in b1 . b1
then (p1 +* ((indx b1),o1)) . o = p1 . o by FUNCT_7:32;
hence (p1 +* ((indx b1),o1)) . o in b1 . o by A47, A51, A54, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom (p1 +* ((indx b1),o1)) = I by PARTFUN1:def_2;
then p1io in product b1 by A51, A53, CARD_3:9;
then A56: J1 in B2 by A36, FUNCT_1:def_6;
reconsider p2io = p2 +* ((indx b1),o2) as Point of (Segre_Product A) by B2, A49, PENCIL_1:25;
reconsider J2 = f . p2io as ManySortedSet of I by PENCIL_1:14;
Im (f,(p2 +* ((indx b1),o2))) = {(f . p2io)} by A36, FUNCT_1:59;
then J2 in f .: (product (b1 +* ((indx b1),{o2}))) by A50, TARSKI:def_1;
then A57: M . o2 = J2 . ((permutation_of_indices f) . (indx b1)) by A35;
dom p1 = I by PARTFUN1:def_2;
then A58: (p1 +* ((indx b1),o1)) . (indx b1) = o1 by FUNCT_7:31;
A59: dom b1 = I by PARTFUN1:def_2;
A60: dom p2 = I by PARTFUN1:def_2;
A61: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
(p2_+*_((indx_b1),o2))_._o_in_b1_._o
let o be set ; ::_thesis: ( o in I implies (p2 +* ((indx b1),o2)) . b1 in b1 . b1 )
assume A62: o in I ; ::_thesis: (p2 +* ((indx b1),o2)) . b1 in b1 . b1
percases ( o = indx b1 or o <> indx b1 ) ;
supposeA63: o = indx b1 ; ::_thesis: (p2 +* ((indx b1),o2)) . b1 in b1 . b1
then (p2 +* ((indx b1),o2)) . o = o2 by A60, FUNCT_7:31;
then (p2 +* ((indx b1),o2)) . o in [#] (A . (indx b1)) ;
hence (p2 +* ((indx b1),o2)) . o in b1 . o by B2, A63, Th10; ::_thesis: verum
end;
suppose o <> indx b1 ; ::_thesis: (p2 +* ((indx b1),o2)) . b1 in b1 . b1
then (p2 +* ((indx b1),o2)) . o = p2 . o by FUNCT_7:32;
hence (p2 +* ((indx b1),o2)) . o in b1 . o by A49, A59, A62, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom (p2 +* ((indx b1),o2)) = I by PARTFUN1:def_2;
then p2io in product b1 by A59, A61, CARD_3:9;
then A64: J2 in B2 by A36, FUNCT_1:def_6;
Im (f,(p1 +* ((indx b1),o1))) = {(f . p1io)} by A36, FUNCT_1:59;
then A65: J1 in f .: (product (b1 +* ((indx b1),{o1}))) by A48, TARSKI:def_1;
A66: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
J1_._o_=_J2_._o
let o be set ; ::_thesis: ( o in I implies J1 . b1 = J2 . b1 )
assume o in I ; ::_thesis: J1 . b1 = J2 . b1
then reconsider l = o as Element of I ;
percases ( l = indx b2 or l <> indx b2 ) ;
suppose l = indx b2 ; ::_thesis: J1 . b1 = J2 . b1
hence J1 . o = J2 . o by A43, A35, A46, A65, A57; ::_thesis: verum
end;
suppose l <> indx b2 ; ::_thesis: J1 . b1 = J2 . b1
hence J1 . o = J2 . o by A1, A56, A64, PENCIL_1:23; ::_thesis: verum
end;
end;
end;
dom p2 = I by PARTFUN1:def_2;
then A67: (p2 +* ((indx b1),o2)) . (indx b1) = o2 by FUNCT_7:31;
( dom J1 = I & dom J2 = I ) by PARTFUN1:def_2;
then J1 = J2 by A66, FUNCT_1:2;
hence x1 = x2 by A36, A3, A58, A67, FUNCT_1:def_4; ::_thesis: verum
end;
f is bijective by PENCIL_2:def_4;
then A68: rng f = the carrier of (Segre_Product A) by FUNCT_2:def_3;
A69: f " = f " by A3, TOPS_2:def_4;
the carrier of (A . ((permutation_of_indices f) . (indx b1))) c= rng M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) or x in rng M )
assume x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ; ::_thesis: x in rng M
then reconsider x1 = x as Point of (A . ((permutation_of_indices f) . (indx b1))) ;
consider p0 being ManySortedSet of I such that
A70: p0 in product b2 and
{(p0 +* ((indx b2),x1))} = product (b2 +* ((indx b2),{x1})) by A43, Th18;
reconsider p = p0 +* ((indx b2),x1) as Point of (Segre_Product A) by A1, A43, A70, PENCIL_1:25;
reconsider p1 = p as ManySortedSet of I ;
reconsider q = (f ") . p as ManySortedSet of I by PENCIL_1:14;
A71: p = f . ((f ") . p) by A68, A3, A69, FUNCT_1:35;
A72: dom b1 = I by PARTFUN1:def_2;
A73: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
q_._o_in_(b1_+*_((indx_b1),{(q_._(indx_b1))}))_._o
let o be set ; ::_thesis: ( o in I implies q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1 )
assume o in I ; ::_thesis: q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1
then reconsider l = o as Element of I ;
percases ( l = indx b1 or l <> indx b1 ) ;
suppose l = indx b1 ; ::_thesis: q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1
then (b1 +* ((indx b1),{(q . (indx b1))})) . l = {(q . o)} by A72, FUNCT_7:31;
hence q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o by TARSKI:def_1; ::_thesis: verum
end;
suppose l <> indx b1 ; ::_thesis: q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1
then A74: (b1 +* ((indx b1),{(q . (indx b1))})) . l = b1 . l by FUNCT_7:32;
A75: dom b2 = I by PARTFUN1:def_2;
A76: dom p0 = I by PARTFUN1:def_2;
A77: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
p1_._o_in_b2_._o
let o be set ; ::_thesis: ( o in I implies p1 . b1 in b2 . b1 )
assume A78: o in I ; ::_thesis: p1 . b1 in b2 . b1
percases ( o = indx b2 or o <> indx b2 ) ;
supposeA79: o = indx b2 ; ::_thesis: p1 . b1 in b2 . b1
then p1 . o = x1 by A76, FUNCT_7:31;
then p1 . o in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ;
hence p1 . o in b2 . o by B1, A1, A2, A79, Def3; ::_thesis: verum
end;
suppose o <> indx b2 ; ::_thesis: p1 . b1 in b2 . b1
then p1 . o = p0 . o by FUNCT_7:32;
hence p1 . o in b2 . o by A70, A75, A78, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom p1 = I by PARTFUN1:def_2;
then p in product b2 by A75, A77, CARD_3:9;
then consider q0 being set such that
A80: q0 in dom f and
A81: q0 in B1 and
A82: p = f . q0 by A1, FUNCT_1:def_6;
q = q0 by A36, A3, A71, A80, A82, FUNCT_1:def_4;
hence q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o by A72, A74, A81, CARD_3:9; ::_thesis: verum
end;
end;
end;
I = dom (Carrier A) by PARTFUN1:def_2;
then q . (indx b1) in (Carrier A) . (indx b1) by A5, CARD_3:9;
then A83: q . (indx b1) in [#] (A . (indx b1)) by Th7;
( dom q = I & dom (b1 +* ((indx b1),{(q . (indx b1))})) = I ) by PARTFUN1:def_2;
then q in product (b1 +* ((indx b1),{(q . (indx b1))})) by A73, CARD_3:9;
then p0 +* ((indx b2),x1) in f .: (product (b1 +* ((indx b1),{(q . (indx b1))}))) by A36, A71, FUNCT_1:def_6;
then ( dom p0 = I & M . (q . (indx b1)) = (p0 +* ((indx b2),x1)) . ((permutation_of_indices f) . (indx b1)) ) by A35, A83, PARTFUN1:def_2;
then ( dom M = the carrier of (A . (indx b1)) & M . (q . (indx b1)) = x ) by A43, FUNCT_2:def_1, FUNCT_7:31;
hence x in rng M by A83, FUNCT_1:3; ::_thesis: verum
end;
then A84: rng M = the carrier of (A . ((permutation_of_indices f) . (indx b1))) by XBOOLE_0:def_10;
then M is onto by FUNCT_2:def_3;
then A85: M " = M " by A44, TOPS_2:def_4;
A86: M " is open
proof
let S0 be Subset of (A . ((permutation_of_indices f) . (indx b1))); :: according to T_0TOPSP:def_2 ::_thesis: ( not S0 is open or (M ") .: S0 is open )
assume S0 is open ; ::_thesis: (M ") .: S0 is open
then reconsider S = S0 as Block of (A . ((permutation_of_indices f) . (indx b1))) by PRE_TOPC:def_2;
reconsider L = product (b2 +* ((indx b2),S)) as Block of (Segre_Product A) by A43, Th12;
reconsider K = f " L as Block of (Segre_Product A) ;
consider k being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A87: K = product k and
A88: k . (indx k) is Block of (A . (indx k)) by PENCIL_1:24;
A89: dom b2 = I by PARTFUN1:def_2;
A90: now__::_thesis:_for_x_being_set_st_x_in_I_holds_
(b2_+*_((indx_b2),S))_._x_c=_b2_._x
let x be set ; ::_thesis: ( x in I implies (b2 +* ((indx b2),S)) . b1 c= b2 . b1 )
assume x in I ; ::_thesis: (b2 +* ((indx b2),S)) . b1 c= b2 . b1
percases ( x = indx b2 or x <> indx b2 ) ;
supposeA91: x = indx b2 ; ::_thesis: (b2 +* ((indx b2),S)) . b1 c= b2 . b1
then (b2 +* ((indx b2),S)) . x = S by A89, FUNCT_7:31;
then (b2 +* ((indx b2),S)) . x c= the carrier of (A . ((permutation_of_indices f) . (indx b1))) ;
hence (b2 +* ((indx b2),S)) . x c= b2 . x by B1, A1, A2, A91, Def3; ::_thesis: verum
end;
suppose x <> indx b2 ; ::_thesis: (b2 +* ((indx b2),S)) . b1 c= b2 . b1
hence (b2 +* ((indx b2),S)) . x c= b2 . x by FUNCT_7:32; ::_thesis: verum
end;
end;
end;
dom (b2 +* ((indx b2),S)) = I by PARTFUN1:def_2;
then L c= product b2 by A89, A90, CARD_3:27;
then (product b1) /\ (product k) = K by A1, A37, A87, RELAT_1:143, XBOOLE_1:28;
then A92: 2 c= card ((product b1) /\ (product k)) by PENCIL_1:def_6;
then A93: indx k = indx b1 by PENCIL_1:26;
M " S = k . (indx k)
proof
thus M " S c= k . (indx k) :: according to XBOOLE_0:def_10 ::_thesis: k . (indx k) c= M " S
proof
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in M " S or o in k . (indx k) )
A94: dom b2 = I by PARTFUN1:def_2;
assume A95: o in M " S ; ::_thesis: o in k . (indx k)
then reconsider u = o as Point of (A . (indx b1)) ;
consider p being ManySortedSet of I such that
A96: p in product b1 and
A97: {(p +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18;
reconsider q = p +* ((indx b1),u) as Point of (Segre_Product A) by B2, A96, PENCIL_1:25;
reconsider fq = f . q as ManySortedSet of I by PENCIL_1:14;
Im (f,(p +* ((indx b1),u))) = {(f . q)} by A36, FUNCT_1:59;
then A98: fq in f .: (product (b1 +* ((indx b1),{u}))) by A97, TARSKI:def_1;
product (b1 +* ((indx b1),{u})) c= product b1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product (b1 +* ((indx b1),{u})) or a in product b1 )
A99: dom b1 = I by PARTFUN1:def_2;
assume a in product (b1 +* ((indx b1),{u})) ; ::_thesis: a in product b1
then consider g being Function such that
A100: a = g and
A101: dom g = dom (b1 +* ((indx b1),{u})) and
A102: for o being set st o in dom (b1 +* ((indx b1),{u})) holds
g . o in (b1 +* ((indx b1),{u})) . o by CARD_3:def_5;
A103: dom g = I by A101, PARTFUN1:def_2;
now__::_thesis:_for_o_being_set_st_o_in_I_holds_
g_._o_in_b1_._o
let o be set ; ::_thesis: ( o in I implies g . b1 in b1 . b1 )
assume o in I ; ::_thesis: g . b1 in b1 . b1
then A104: g . o in (b1 +* ((indx b1),{u})) . o by A101, A102, A103;
percases ( o = indx b1 or o <> indx b1 ) ;
supposeA105: o = indx b1 ; ::_thesis: g . b1 in b1 . b1
then g . o in {u} by A99, A104, FUNCT_7:31;
then g . o in [#] (A . (indx b1)) ;
hence g . o in b1 . o by B2, A105, Th10; ::_thesis: verum
end;
suppose o <> indx b1 ; ::_thesis: g . b1 in b1 . b1
hence g . o in b1 . o by A104, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
hence a in product b1 by A100, A103, A99, CARD_3:9; ::_thesis: verum
end;
then A106: f .: (product (b1 +* ((indx b1),{u}))) c= product b2 by A1, RELAT_1:123;
M . o in S by A95, FUNCT_1:def_7;
then A107: fq . ((permutation_of_indices f) . (indx b1)) in S by A35, A98;
A108: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
fq_._o_in_(b2_+*_((indx_b2),S))_._o
let o be set ; ::_thesis: ( o in I implies fq . b1 in (b2 +* ((indx b2),S)) . b1 )
assume A109: o in I ; ::_thesis: fq . b1 in (b2 +* ((indx b2),S)) . b1
percases ( o = indx b2 or o <> indx b2 ) ;
suppose o = indx b2 ; ::_thesis: fq . b1 in (b2 +* ((indx b2),S)) . b1
hence fq . o in (b2 +* ((indx b2),S)) . o by A43, A107, A94, FUNCT_7:31; ::_thesis: verum
end;
suppose o <> indx b2 ; ::_thesis: fq . b1 in (b2 +* ((indx b2),S)) . b1
then (b2 +* ((indx b2),S)) . o = b2 . o by FUNCT_7:32;
hence fq . o in (b2 +* ((indx b2),S)) . o by A98, A106, A94, A109, CARD_3:9; ::_thesis: verum
end;
end;
end;
( dom fq = I & dom (b2 +* ((indx b2),S)) = I ) by PARTFUN1:def_2;
then fq in L by A108, CARD_3:9;
then ( dom k = I & q in K ) by A36, FUNCT_1:def_7, PARTFUN1:def_2;
then ( dom p = I & (p +* ((indx b1),u)) . (indx b1) in k . (indx b1) ) by A87, CARD_3:9, PARTFUN1:def_2;
hence o in k . (indx k) by A93, FUNCT_7:31; ::_thesis: verum
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in k . (indx k) or o in M " S )
assume A110: o in k . (indx k) ; ::_thesis: o in M " S
k . (indx k) in the topology of (A . (indx b1)) by A88, A93;
then reconsider u = o as Point of (A . (indx b1)) by A110;
consider p0 being ManySortedSet of I such that
A111: p0 in product b1 and
A112: {(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18;
reconsider p = p0 +* ((indx b1),u) as Point of (Segre_Product A) by B2, A111, PENCIL_1:25;
reconsider fp = f . p as ManySortedSet of I by PENCIL_1:14;
A113: dom b1 = I by PARTFUN1:def_2;
A114: dom p0 = I by PARTFUN1:def_2;
A115: now__::_thesis:_for_a_being_set_st_a_in_I_holds_
(p0_+*_((indx_b1),u))_._a_in_k_._a
let a be set ; ::_thesis: ( a in I implies (p0 +* ((indx b1),u)) . b1 in k . b1 )
assume A116: a in I ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in k . b1
percases ( a = indx b1 or a <> indx b1 ) ;
suppose a = indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in k . b1
hence (p0 +* ((indx b1),u)) . a in k . a by A93, A110, A114, FUNCT_7:31; ::_thesis: verum
end;
supposeA117: a <> indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in k . b1
then (p0 +* ((indx b1),u)) . a = p0 . a by FUNCT_7:32;
then (p0 +* ((indx b1),u)) . a in b1 . a by A111, A113, A116, CARD_3:9;
hence (p0 +* ((indx b1),u)) . a in k . a by A92, A117, PENCIL_1:26; ::_thesis: verum
end;
end;
end;
( dom (p0 +* ((indx b1),u)) = I & dom k = I ) by PARTFUN1:def_2;
then p in K by A87, A115, CARD_3:9;
then ( dom (b2 +* ((indx b2),S)) = I & fp in L ) by FUNCT_1:def_7, PARTFUN1:def_2;
then ( dom b2 = I & fp . (indx b2) in (b2 +* ((indx b2),S)) . (indx b2) ) by CARD_3:9, PARTFUN1:def_2;
then A118: fp . ((permutation_of_indices f) . (indx b1)) in S by A43, FUNCT_7:31;
Im (f,(p0 +* ((indx b1),u))) = {(f . p)} by A36, FUNCT_1:59;
then fp in f .: (product (b1 +* ((indx b1),{u}))) by A112, TARSKI:def_1;
then M . u = fp . ((permutation_of_indices f) . (indx b1)) by A35;
hence o in M " S by A35, A118, FUNCT_1:def_7; ::_thesis: verum
end;
then (M ") .: S is Block of (A . (indx b1)) by A44, A85, A88, A93, FUNCT_1:85;
hence (M ") .: S0 is open by PRE_TOPC:def_2; ::_thesis: verum
end;
A119: M is open
proof
let S0 be Subset of (A . (indx b1)); :: according to T_0TOPSP:def_2 ::_thesis: ( not S0 is open or M .: S0 is open )
assume S0 is open ; ::_thesis: M .: S0 is open
then reconsider S = S0 as Block of (A . (indx b1)) by PRE_TOPC:def_2;
reconsider L = product (b1 +* ((indx b1),S)) as Block of (Segre_Product A) by Th12;
reconsider K = f .: L as Block of (Segre_Product A) ;
consider k being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A120: K = product k and
A121: k . (indx k) is Block of (A . (indx k)) by PENCIL_1:24;
A122: dom b1 = I by PARTFUN1:def_2;
A123: now__::_thesis:_for_x_being_set_st_x_in_I_holds_
(b1_+*_((indx_b1),S))_._x_c=_b1_._x
let x be set ; ::_thesis: ( x in I implies (b1 +* ((indx b1),S)) . b1 c= b1 . b1 )
assume x in I ; ::_thesis: (b1 +* ((indx b1),S)) . b1 c= b1 . b1
percases ( x = indx b1 or x <> indx b1 ) ;
supposeA124: x = indx b1 ; ::_thesis: (b1 +* ((indx b1),S)) . b1 c= b1 . b1
then (b1 +* ((indx b1),S)) . x = S by A122, FUNCT_7:31;
then (b1 +* ((indx b1),S)) . x c= [#] (A . (indx b1)) ;
hence (b1 +* ((indx b1),S)) . x c= b1 . x by B2, A124, Th10; ::_thesis: verum
end;
suppose x <> indx b1 ; ::_thesis: (b1 +* ((indx b1),S)) . b1 c= b1 . b1
hence (b1 +* ((indx b1),S)) . x c= b1 . x by FUNCT_7:32; ::_thesis: verum
end;
end;
end;
dom (b1 +* ((indx b1),S)) = I by PARTFUN1:def_2;
then A125: L c= product b1 by A122, A123, CARD_3:27;
then (product b2) /\ (product k) = K by A1, A120, RELAT_1:123, XBOOLE_1:28;
then 2 c= card ((product b2) /\ (product k)) by PENCIL_1:def_6;
then A126: indx k = (permutation_of_indices f) . (indx b1) by A43, PENCIL_1:26;
A127: dom k = I by PARTFUN1:def_2;
M .: S = k . (indx k)
proof
thus M .: S c= k . (indx k) :: according to XBOOLE_0:def_10 ::_thesis: k . (indx k) c= M .: S
proof
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in M .: S or o in k . (indx k) )
A128: dom b1 = I by PARTFUN1:def_2;
assume o in M .: S ; ::_thesis: o in k . (indx k)
then consider u being set such that
A129: u in dom M and
A130: u in S and
A131: o = M . u by FUNCT_1:def_6;
reconsider u = u as Point of (A . (indx b1)) by A129;
consider p0 being ManySortedSet of I such that
A132: p0 in product b1 and
A133: {(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18;
reconsider p = p0 +* ((indx b1),u) as Point of (Segre_Product A) by B2, A132, PENCIL_1:25;
reconsider q = f . p as ManySortedSet of I by PENCIL_1:14;
Im (f,(p0 +* ((indx b1),u))) = {(f . p)} by A36, FUNCT_1:59;
then q in f .: (product (b1 +* ((indx b1),{u}))) by A133, TARSKI:def_1;
then A134: M . u = q . ((permutation_of_indices f) . (indx b1)) by A35;
A135: dom p0 = I by PARTFUN1:def_2;
A136: now__::_thesis:_for_a_being_set_st_a_in_I_holds_
(p0_+*_((indx_b1),u))_._a_in_(b1_+*_((indx_b1),S))_._a
let a be set ; ::_thesis: ( a in I implies (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1 )
assume A137: a in I ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1
percases ( a = indx b1 or a <> indx b1 ) ;
supposeA138: a = indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1
then (p0 +* ((indx b1),u)) . a = u by A135, FUNCT_7:31;
hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A130, A128, A138, FUNCT_7:31; ::_thesis: verum
end;
supposeA139: a <> indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1
then (p0 +* ((indx b1),u)) . a = p0 . a by FUNCT_7:32;
then (p0 +* ((indx b1),u)) . a in b1 . a by A132, A128, A137, CARD_3:9;
hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A139, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
( dom (p0 +* ((indx b1),u)) = I & dom (b1 +* ((indx b1),S)) = I ) by PARTFUN1:def_2;
then p in L by A136, CARD_3:9;
then q in product k by A36, A120, FUNCT_1:def_6;
hence o in k . (indx k) by A127, A126, A131, A134, CARD_3:9; ::_thesis: verum
end;
let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in k . (indx k) or o in M .: S )
assume A140: o in k . (indx k) ; ::_thesis: o in M .: S
k . (indx k) in the topology of (A . ((permutation_of_indices f) . (indx b1))) by A121, A126;
then reconsider u = o as Point of (A . ((permutation_of_indices f) . (indx b1))) by A140;
consider p0 being ManySortedSet of I such that
A141: p0 in product k and
{(p0 +* (((permutation_of_indices f) . (indx b1)),u))} = product (k +* (((permutation_of_indices f) . (indx b1)),{u})) by A126, Th18;
K in the topology of (Segre_Product A) ;
then reconsider p = p0 +* (((permutation_of_indices f) . (indx b1)),u) as Point of (Segre_Product A) by A120, A141, PENCIL_1:25;
reconsider q = (f ") . p as ManySortedSet of I by PENCIL_1:14;
A142: dom k = I by PARTFUN1:def_2;
A143: dom p0 = I by PARTFUN1:def_2;
A144: now__::_thesis:_for_z_being_set_st_z_in_I_holds_
(p0_+*_(((permutation_of_indices_f)_._(indx_b1)),u))_._z_in_k_._z
let z be set ; ::_thesis: ( z in I implies (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1 )
assume A145: z in I ; ::_thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1
percases ( z = (permutation_of_indices f) . (indx b1) or z <> (permutation_of_indices f) . (indx b1) ) ;
suppose z = (permutation_of_indices f) . (indx b1) ; ::_thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1
hence (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z by A126, A140, A143, FUNCT_7:31; ::_thesis: verum
end;
suppose z <> (permutation_of_indices f) . (indx b1) ; ::_thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1
then (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z = p0 . z by FUNCT_7:32;
hence (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z by A141, A142, A145, CARD_3:9; ::_thesis: verum
end;
end;
end;
A146: p = f . q by A68, A3, A69, FUNCT_1:35;
dom (p0 +* (((permutation_of_indices f) . (indx b1)),u)) = I by PARTFUN1:def_2;
then p in f .: L by A120, A142, A144, CARD_3:9;
then ex qq being set st
( qq in dom f & qq in L & p = f . qq ) by FUNCT_1:def_6;
then A147: q in L by A36, A3, A146, FUNCT_1:def_4;
dom (b1 +* ((indx b1),S)) = I by PARTFUN1:def_2;
then q . (indx b1) in (b1 +* ((indx b1),S)) . (indx b1) by A147, CARD_3:9;
then A148: q . (indx b1) in S by A122, FUNCT_7:31;
then reconsider qi = q . (indx b1) as Point of (A . (indx b1)) ;
consider q0 being ManySortedSet of I such that
A149: q0 in product b1 and
A150: {(q0 +* ((indx b1),qi))} = product (b1 +* ((indx b1),{qi})) by Th18;
A151: dom q0 = I by PARTFUN1:def_2;
A152: now__::_thesis:_for_a_being_set_st_a_in_I_holds_
(q0_+*_((indx_b1),qi))_._a_=_q_._a
let a be set ; ::_thesis: ( a in I implies (q0 +* ((indx b1),qi)) . b1 = q . b1 )
assume a in I ; ::_thesis: (q0 +* ((indx b1),qi)) . b1 = q . b1
percases ( a = indx b1 or a <> indx b1 ) ;
suppose a = indx b1 ; ::_thesis: (q0 +* ((indx b1),qi)) . b1 = q . b1
hence (q0 +* ((indx b1),qi)) . a = q . a by A151, FUNCT_7:31; ::_thesis: verum
end;
supposeA153: a <> indx b1 ; ::_thesis: (q0 +* ((indx b1),qi)) . b1 = q . b1
then (q0 +* ((indx b1),qi)) . a = q0 . a by FUNCT_7:32;
hence (q0 +* ((indx b1),qi)) . a = q . a by A125, A147, A149, A153, PENCIL_1:23; ::_thesis: verum
end;
end;
end;
( dom q = I & dom (q0 +* ((indx b1),qi)) = I ) by PARTFUN1:def_2;
then q0 +* ((indx b1),qi) = q by A152, FUNCT_1:2;
then Im (f,(q0 +* ((indx b1),qi))) = {(f . q)} by A36, FUNCT_1:59;
then p in f .: (product (b1 +* ((indx b1),{qi}))) by A146, A150, TARSKI:def_1;
then M . (q . (indx b1)) = (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . ((permutation_of_indices f) . (indx b1)) by A35;
then M . (q . (indx b1)) = o by A143, FUNCT_7:31;
hence o in M .: S by A35, A148, FUNCT_1:def_6; ::_thesis: verum
end;
hence M .: S0 is open by A121, A126, PRE_TOPC:def_2; ::_thesis: verum
end;
take M ; ::_thesis: ( M is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) ) )
A154: M is onto by A84, FUNCT_2:def_3;
then M " is bijective by A44, PENCIL_2:12;
hence M is isomorphic by A44, A154, A119, A86, PENCIL_2:def_4; ::_thesis: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
let a be ManySortedSet of I; ::_thesis: ( a is Point of (Segre_Product A) & a in product b1 implies for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) )
assume that
A155: a is Point of (Segre_Product A) and
A156: a in product b1 ; ::_thesis: for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
dom (Carrier A) = I by PARTFUN1:def_2;
then a . (indx b1) in (Carrier A) . (indx b1) by A5, A155, CARD_3:9;
then a . (indx b1) in [#] (A . (indx b1)) by Th7;
then reconsider ai = a . (indx b1) as Point of (A . (indx b1)) ;
A157: dom b1 = I by PARTFUN1:def_2;
A158: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
a_._o_in_(b1_+*_((indx_b1),{ai}))_._o
let o be set ; ::_thesis: ( o in I implies a . b1 in (b1 +* ((indx b1),{ai})) . b1 )
assume A159: o in I ; ::_thesis: a . b1 in (b1 +* ((indx b1),{ai})) . b1
percases ( o = indx b1 or o <> indx b1 ) ;
supposeA160: o = indx b1 ; ::_thesis: a . b1 in (b1 +* ((indx b1),{ai})) . b1
then (b1 +* ((indx b1),{ai})) . o = {ai} by A157, FUNCT_7:31;
hence a . o in (b1 +* ((indx b1),{ai})) . o by A160, TARSKI:def_1; ::_thesis: verum
end;
suppose o <> indx b1 ; ::_thesis: a . b1 in (b1 +* ((indx b1),{ai})) . b1
then (b1 +* ((indx b1),{ai})) . o = b1 . o by FUNCT_7:32;
hence a . o in (b1 +* ((indx b1),{ai})) . o by A156, A157, A159, CARD_3:9; ::_thesis: verum
end;
end;
end;
( dom a = I & dom (b1 +* ((indx b1),{ai})) = I ) by PARTFUN1:def_2;
then A161: a in product (b1 +* ((indx b1),{ai})) by A158, CARD_3:9;
let b be ManySortedSet of I; ::_thesis: ( b = f . a implies b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) )
assume b = f . a ; ::_thesis: b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
then b in f .: (product (b1 +* ((indx b1),{ai}))) by A36, A155, A161, FUNCT_1:def_6;
hence b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) by A35; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st b1 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = b1 . (a . (indx b1)) ) & b2 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = b2 . (a . (indx b1)) ) holds
b1 = b2
proof
set i = indx b1;
set s = permutation_of_indices f;
let f1, f2 be Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))); ::_thesis: ( f1 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) ) & f2 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ) implies f1 = f2 )
assume that
f1 is isomorphic and
A162: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) and
f2 is isomorphic and
A163: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ; ::_thesis: f1 = f2
A164: now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
consider p being set such that
A165: p in product b1 by XBOOLE_0:def_1;
assume x in dom f1 ; ::_thesis: f1 . x = f2 . x
then reconsider x0 = x as Point of (A . (indx b1)) ;
reconsider p = p as Point of (Segre_Product A) by B2, A165;
reconsider P = p as ManySortedSet of I by PENCIL_1:14;
set a = P +* ((indx b1),x0);
reconsider a1 = P +* ((indx b1),x0) as Point of (Segre_Product A) by PENCIL_1:25;
A166: dom b1 = I by PARTFUN1:def_2;
A167: dom P = I by PARTFUN1:def_2;
A168: now__::_thesis:_for_e_being_set_st_e_in_I_holds_
(P_+*_((indx_b1),x0))_._e_in_b1_._e
let e be set ; ::_thesis: ( e in I implies (P +* ((indx b1),x0)) . b1 in b1 . b1 )
assume A169: e in I ; ::_thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1
percases ( e = indx b1 or e <> indx b1 ) ;
supposeA170: e = indx b1 ; ::_thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1
then (P +* ((indx b1),x0)) . e = x0 by A167, FUNCT_7:31;
then (P +* ((indx b1),x0)) . e in [#] (A . (indx b1)) ;
hence (P +* ((indx b1),x0)) . e in b1 . e by B2, A170, Th10; ::_thesis: verum
end;
suppose e <> indx b1 ; ::_thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1
then (P +* ((indx b1),x0)) . e = P . e by FUNCT_7:32;
hence (P +* ((indx b1),x0)) . e in b1 . e by A165, A166, A169, CARD_3:9; ::_thesis: verum
end;
end;
end;
reconsider b = f . a1 as ManySortedSet of I by PENCIL_1:14;
dom P = I by PARTFUN1:def_2;
then A171: (P +* ((indx b1),x0)) . (indx b1) = x by FUNCT_7:31;
dom (P +* ((indx b1),x0)) = I by PARTFUN1:def_2;
then A172: P +* ((indx b1),x0) in product b1 by A166, A168, CARD_3:9;
then f2 . ((P +* ((indx b1),x0)) . (indx b1)) = b . ((permutation_of_indices f) . (indx b1)) by A163;
hence f1 . x = f2 . x by A162, A172, A171; ::_thesis: verum
end;
dom f1 = the carrier of (A . (indx b1)) by FUNCT_2:def_1
.= dom f2 by FUNCT_2:def_1 ;
hence f1 = f2 by A164, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines canonical_embedding PENCIL_3:def_4_:_
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A holds
for b5 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) holds
( b5 = canonical_embedding (f,b1) iff ( b5 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = b5 . (a . (indx b1)) ) ) );
theorem Th26: :: PENCIL_3:26
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)
proof
let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2) )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A)
for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)
let f be Collineation of (Segre_Product A); ::_thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)
let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 misses B2 & B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2) )
assume that
A2: B1 misses B2 and
A3: B1 '||' B2 ; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
canonical_embedding (f,b1) = canonical_embedding (f,b2)
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b1 = B1 & product b2 = B2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) )
assume that
A4: product b1 = B1 and
A5: product b2 = B2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,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 non trivial-yielding Segre-like 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 non trivial-yielding Segre-like 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__::_thesis:_for_o_being_set_st_o_in_the_carrier_of_(A_._(indx_b1))_holds_
(canonical_embedding_(f,b1))_._o_=_(canonical_embedding_(f,b2))_._o
b2 . r is trivial by A6, A9, PENCIL_1:def_21;
then consider c2 being set 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 by PBOOLE:def_2;
then A21: {c2} c= [#] (A . r) by A20, Th7;
let o be set ; ::_thesis: ( o in the carrier of (A . (indx b1)) implies (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1 )
consider p0 being set such that
A22: p0 in product b1 by XBOOLE_0:def_1;
assume o in the carrier of (A . (indx b1)) ; ::_thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1
then reconsider u = o as Point of (A . (indx b1)) ;
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 +* ((indx b1),u);
reconsider q1 = p +* ((indx b1),u) as Point of (Segre_Product A) by PENCIL_1:25;
b1 . r is trivial by A9, PENCIL_1:def_21;
then consider c1 being set 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 by PBOOLE:def_2;
then {c1} c= [#] (A . r) by A23, Th7;
then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;
reconsider c2 = c2 as Point of (A . r) by A21, ZFMISC_1:31;
set t = (p +* ((indx b1),u)) +* (r,c2);
p +* ((indx b1),u) is Point of (Segre_Product A) by PENCIL_1:25;
then reconsider t1 = (p +* ((indx b1),u)) +* (r,c2) as Point of (Segre_Product A) by PENCIL_1:25;
percases ( c1 <> c2 or c1 = c2 ) ;
supposeA24: c1 <> c2 ; ::_thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1
(p +* ((indx b1),u)) . r = p . r by A9, FUNCT_7:32;
then (p +* ((indx b1),u)) . r in b1 . r by A18, A22, CARD_3:9;
then A25: (p +* ((indx b1),u)) . r = c1 by A23, TARSKI:def_1;
dom (p +* ((indx b1),u)) = I by PARTFUN1:def_2;
then A26: ((p +* ((indx b1),u)) +* (r,c2)) . r = c2 by FUNCT_7:31;
now__::_thesis:_for_q3,_t3_being_ManySortedSet_of_I_st_q3_=_q1_&_t3_=_t1_holds_
ex_r_being_Element_of_I_st_
(_(_for_a,_b_being_Point_of_(A_._r)_st_a_=_q3_._r_&_b_=_t3_._r_holds_
(_a_<>_b_&_a,b_are_collinear_)_)_&_(_for_j_being_Element_of_I_st_j_<>_r_holds_
q3_._j_=_t3_._j_)_)
let q3, t3 be ManySortedSet of I; ::_thesis: ( q3 = q1 & t3 = t1 implies ex r being Element of I st
( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
q3 . j = t3 . j ) ) )
assume A27: ( q3 = q1 & t3 = t1 ) ; ::_thesis: ex r being Element of I st
( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
q3 . j = t3 . j ) )
take r = r; ::_thesis: ( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
q3 . j = t3 . j ) )
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; ::_thesis: for j being Element of I st j <> r holds
q3 . j = t3 . j
let j be Element of I; ::_thesis: ( j <> r implies q3 . j = t3 . j )
assume j <> r ; ::_thesis: q3 . j = t3 . j
hence q3 . j = t3 . j by A27, FUNCT_7:32; ::_thesis: verum
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__::_thesis:_for_a_being_set_st_a_in_I_holds_
(p_+*_((indx_b1),u))_._a_in_b1_._a
let a be set ; ::_thesis: ( a in I implies (p +* ((indx b1),u)) . b1 in b1 . b1 )
assume A32: a in I ; ::_thesis: (p +* ((indx b1),u)) . b1 in b1 . b1
percases ( a = indx b1 or a <> indx b1 ) ;
suppose a = indx b1 ; ::_thesis: (p +* ((indx b1),u)) . b1 in b1 . b1
then ( (p +* ((indx b1),u)) . a = u & b1 . a = [#] (A . (indx b1)) ) by A4, A30, Th10, FUNCT_7:31;
hence (p +* ((indx b1),u)) . a in b1 . a ; ::_thesis: verum
end;
suppose a <> indx b1 ; ::_thesis: (p +* ((indx b1),u)) . b1 in b1 . b1
then (p +* ((indx b1),u)) . a = p . a by FUNCT_7:32;
hence (p +* ((indx b1),u)) . a in b1 . a by A22, A29, A32, CARD_3:9; ::_thesis: verum
end;
end;
end;
A33: dom (p +* ((indx b1),u)) = I by PARTFUN1:def_2;
then A34: p +* ((indx b1),u) in product b1 by A29, A31, CARD_3:9;
A35: now__::_thesis:_for_a_being_set_st_a_in_I_holds_
((p_+*_((indx_b1),u))_+*_(r,c2))_._a_in_b2_._a
let a be set ; ::_thesis: ( a in I implies ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1 )
assume A36: a in I ; ::_thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1
percases ( a = r or a <> r ) ;
supposeA37: a = r ; ::_thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1
then ((p +* ((indx b1),u)) +* (r,c2)) . a = c2 by A33, FUNCT_7:31;
hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A20, A37, TARSKI:def_1; ::_thesis: verum
end;
supposeA38: a <> r ; ::_thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1
then ((p +* ((indx b1),u)) +* (r,c2)) . a = (p +* ((indx b1),u)) . a by FUNCT_7:32;
then ((p +* ((indx b1),u)) +* (r,c2)) . a in b1 . a by A31, A36;
hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A10, A36, A38; ::_thesis: verum
end;
end;
end;
( dom ((p +* ((indx b1),u)) +* (r,c2)) = I & dom b2 = I ) by PARTFUN1:def_2;
then A39: (p +* ((indx b1),u)) +* (r,c2) in product b2 by A35, CARD_3:9;
then A40: (canonical_embedding (f,b2)) . (((p +* ((indx b1),u)) +* (r,c2)) . (indx b1)) = ft . ((permutation_of_indices f) . (indx b1)) by A1, A5, A6, Def4;
A41: f . q1 <> f . t1 by A17, A7, A24, A25, A26, FUNCT_1:def_4;
A42: now__::_thesis:_not_fq_._(indx_b3)_<>_ft_._(indx_b3)
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 . (indx b3) <> ft . (indx b3) ; ::_thesis: contradiction
then A44: indx b3 = 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__::_thesis:_for_o_being_set_st_o_in_I_holds_
fq_._o_in_b4_._o
let o be set ; ::_thesis: ( o in I implies fq . b1 in b4 . b1 )
assume o in I ; ::_thesis: fq . b1 in b4 . b1
then reconsider o1 = o as Element of I ;
percases ( o1 = indx b3 or o1 <> indx b3 ) ;
suppose o1 = indx b3 ; ::_thesis: fq . b1 in b4 . b1
hence fq . o in b4 . o by A14, A15, A13, A16, A46, A47, CARD_3:9; ::_thesis: verum
end;
suppose o1 <> indx b3 ; ::_thesis: fq . b1 in b4 . b1
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; ::_thesis: verum
end;
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, XBOOLE_0:def_7; ::_thesis: verum
end;
A50: indx b3 = (permutation_of_indices f) . (indx b1) by A1, A4, A14, Def3;
dom p = I by PARTFUN1:def_2;
then A51: (p +* ((indx b1),u)) . (indx b1) = o by FUNCT_7:31;
then ((p +* ((indx b1),u)) +* (r,c2)) . (indx b1) = 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; ::_thesis: verum
end;
supposeA52: c1 = c2 ; ::_thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1
A53: now__::_thesis:_for_o_being_set_st_o_in_I_holds_
b1_._o_=_b2_._o
let o be set ; ::_thesis: ( o in I implies b1 . b1 = b2 . b1 )
assume o in I ; ::_thesis: b1 . b1 = b2 . b1
then reconsider o1 = o as Element of I ;
percases ( r = o1 or r <> o1 ) ;
suppose r = o1 ; ::_thesis: b1 . b1 = b2 . b1
hence b1 . o = b2 . o by A23, A20, A52; ::_thesis: verum
end;
suppose r <> o1 ; ::_thesis: b1 . b1 = b2 . b1
hence b1 . o = b2 . o by A10; ::_thesis: verum
end;
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; ::_thesis: verum
end;
end;
end;
( dom (canonical_embedding (f,b1)) = the carrier of (A . (indx b1)) & dom (canonical_embedding (f,b2)) = the carrier of (A . (indx b1)) ) by A6, FUNCT_2:def_1;
hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A19, FUNCT_1:2; ::_thesis: verum
end;
theorem Th27: :: PENCIL_3:27
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for b1, b2 being non trivial-yielding Segre-like 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 non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for b1, b2 being non trivial-yielding Segre-like 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)
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A)
for b1, b2 being non trivial-yielding Segre-like 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) )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A)
for b1, b2 being non trivial-yielding Segre-like 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)
A2: now__::_thesis:_for_o_being_Element_of_I_holds_A_._o_is_connected
let o be Element of I; ::_thesis: A . o is connected
A . o is strongly_connected by A1;
hence A . o is connected by Th4; ::_thesis: verum
end;
let f be Collineation of (Segre_Product A); ::_thesis: for b1, b2 being non trivial-yielding Segre-like 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)
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) )
assume that
A3: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A ) and
A4: indx b1 = indx b2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)
reconsider B1 = product b1, B2 = product b2 as Segre-Coset of A by A3;
percases ( B1 misses B2 or B1 meets B2 ) ;
suppose B1 misses B2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,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 holds
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 S1[ Nat] means ( $1 in dom D implies for D1 being Segre-Coset of A st D1 = D . $1 holds
for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D1 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1) );
A9: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
assume k + 1 in dom D ; ::_thesis: for D1 being Segre-Coset of A st D1 = D . (k + 1) holds
for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D1 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1)
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; ::_thesis: ( D2 = D . (k + 1) implies for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D2 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1) )
assume A12: D2 = D . (k + 1) ; ::_thesis: for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D2 = product d1 holds
canonical_embedding (f,b1) = canonical_embedding (f,d1)
let d2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( D2 = product d2 implies canonical_embedding (f,b1) = canonical_embedding (f,d2) )
assume A13: D2 = product d2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2)
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2)
hence canonical_embedding (f,b1) = canonical_embedding (f,d2) by A5, A12, A13, PUA2MSS1:2; ::_thesis: verum
end;
supposeA14: 1 <= k ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2)
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 non trivial-yielding Segre-like 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 canonical_embedding (f,b1) = canonical_embedding (f,d2) by A10, A11, A14, A15, FINSEQ_3:25; ::_thesis: verum
end;
end;
end;
end;
A16: S1[ 0 ] by FINSEQ_3:24;
for n being Nat holds S1[n] from NAT_1:sch_2(A16, A9);
then A17: S1[ len D] ;
1 in dom D by A5, FUNCT_1:def_2;
then 1 <= len D by FINSEQ_3:25;
hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A6, A17, FINSEQ_3:25; ::_thesis: verum
end;
suppose B1 meets B2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)
hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A4, Th11; ::_thesis: verum
end;
end;
end;
definition
let I be non empty finite set ;
let A be PLS-yielding ManySortedSet of I;
assume B1: 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: :: PENCIL_3:def 5
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
it = canonical_embedding (f,b);
existence
ex b1 being Function of (A . i),(A . ((permutation_of_indices f) . i)) st
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b1 = canonical_embedding (f,b)
proof
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A1: indx L = i and
A2: 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 A1;
take n ; ::_thesis: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
n = canonical_embedding (f,b)
let b be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b is Segre-Coset of A & indx b = i implies n = canonical_embedding (f,b) )
assume ( product b is Segre-Coset of A & indx b = i ) ; ::_thesis: n = canonical_embedding (f,b)
hence n = canonical_embedding (f,b) by B1, A1, A2, Th27; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (A . i),(A . ((permutation_of_indices f) . i)) st ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b1 = canonical_embedding (f,b) ) & ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b2 = canonical_embedding (f,b) ) holds
b1 = b2
proof
let n1, n2 be Function of (A . i),(A . ((permutation_of_indices f) . i)); ::_thesis: ( ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
n1 = canonical_embedding (f,b) ) & ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
n2 = canonical_embedding (f,b) ) implies n1 = n2 )
assume that
A3: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
n1 = canonical_embedding (f,b) and
A4: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
n2 = canonical_embedding (f,b) ; ::_thesis: n1 = n2
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A5: ( indx L = i & product L is Segre-Coset of A ) by Th8;
thus n1 = canonical_embedding (f,L) by A3, A5
.= n2 by A4, A5 ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines canonical_embedding PENCIL_3:def_5_:_
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for i being Element of I
for b5 being Function of (A . i),(A . ((permutation_of_indices f) . i)) holds
( b5 = canonical_embedding (f,i) iff for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b5 = canonical_embedding (f,b) );
theorem :: PENCIL_3:28
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A) ex s being Permutation of I ex 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 holds
for b being ManySortedSet of I st b = f . p holds
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 non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A) ex s being Permutation of I ex 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 holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) ex s being Permutation of I ex 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 holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) ) )
assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A) ex s being Permutation of I ex 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 holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) )
let f be Collineation of (Segre_Product A); ::_thesis: ex s being Permutation of I ex 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 holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) )
set s = permutation_of_indices f;
take permutation_of_indices f ; ::_thesis: ex B being Function-yielding ManySortedSet of I st
for i being Element of I holds
( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . 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 holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) ) )
defpred S1[ set , set ] means for i being Element of I st i = $1 holds
$2 = canonical_embedding (f,i);
A2: for i being set st i in I holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] )
assume i in I ; ::_thesis: ex j being set st S1[i,j]
then reconsider i1 = i as Element of I ;
S1[i1, canonical_embedding (f,i1)] ;
hence ex j being set st S1[i,j] ; ::_thesis: verum
end;
consider B being ManySortedSet of I such that
A3: for i being set st i in I holds
S1[i,B . i] from PBOOLE:sch_3(A2);
now__::_thesis:_for_x_being_set_st_x_in_dom_B_holds_
B_._x_is_Function
let x be set ; ::_thesis: ( x in dom B implies B . x is Function )
assume x in dom B ; ::_thesis: B . x is Function
then reconsider y = x as Element of I ;
B . y = canonical_embedding (f,y) by A3;
hence B . x is Function ; ::_thesis: verum
end;
then reconsider B = B as Function-yielding ManySortedSet of I by FUNCOP_1:def_6;
take B ; ::_thesis: for i being Element of I holds
( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . 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 holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) ) )
let i be Element of I; ::_thesis: ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . 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 holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) ) )
A4: B . i = canonical_embedding (f,i) by A3;
thus ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
m is isomorphic ) ) ::_thesis: for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)
proof
thus B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) by A4; ::_thesis: for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
m is isomorphic
let m be Function of (A . i),(A . ((permutation_of_indices f) . i)); ::_thesis: ( m = B . i implies m is isomorphic )
assume A5: m = B . i ; ::_thesis: m is isomorphic
consider L being non trivial-yielding Segre-like 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 m is isomorphic by A1, A5, A6, Def4; ::_thesis: verum
end;
let p be Point of (Segre_Product A); ::_thesis: for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)
let a be ManySortedSet of I; ::_thesis: ( a = p implies for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) )
assume A7: a = p ; ::_thesis: for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)
consider b1 being non trivial-yielding Segre-like 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; ::_thesis: ( b = f . p implies for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) )
assume A10: b = f . p ; ::_thesis: for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)
let m be Function of (A . i),(A . ((permutation_of_indices f) . i)); ::_thesis: ( m = B . i implies b . ((permutation_of_indices f) . i) = m . (a . i) )
assume m = B . i ; ::_thesis: b . ((permutation_of_indices f) . i) = m . (a . i)
then m = canonical_embedding (f,b1) by A1, A4, A8, Def5;
hence b . ((permutation_of_indices f) . i) = m . (a . i) by A1, A7, A10, A8, A9, Def4; ::_thesis: verum
end;