:: On Segre's Product of Partial Line Spaces :: by Adam Naumowicz :: :: Received May 29, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin theorem Th1: :: PENCIL_1:1 for f, g being Function st product f = product g & f is non-empty holds g is non-empty proofend; theorem Th2: :: PENCIL_1:2 for X being set holds ( 2 c= card X iff ex x, y being set st ( x in X & y in X & x <> y ) ) proofend; theorem Th3: :: PENCIL_1:3 for X being set st 2 c= card X holds for x being set ex y being set st ( y in X & x <> y ) proofend; theorem Th4: :: PENCIL_1:4 for X being set holds ( 2 c= card X iff not X is trivial ) proofend; theorem Th5: :: PENCIL_1:5 for X being set holds ( 3 c= card X iff ex x, y, z being set st ( x in X & y in X & z in X & x <> y & x <> z & y <> z ) ) proofend; theorem Th6: :: PENCIL_1:6 for X being set st 3 c= card X holds for x, y being set ex z being set st ( z in X & x <> z & y <> z ) proofend; begin definition let S be TopStruct ; mode Block of S is Element of the topology of S; end; definition let S be TopStruct ; let x, y be Point of S; predx,y are_collinear means :Def1: :: PENCIL_1:def 1 ( x = y or ex l being Block of S st {x,y} c= l ); end; :: deftheorem Def1 defines are_collinear PENCIL_1:def_1_:_ for S being TopStruct for x, y being Point of S holds ( x,y are_collinear iff ( x = y or ex l being Block of S st {x,y} c= l ) ); definition let S be TopStruct ; let T be Subset of S; attrT is closed_under_lines means :Def2: :: PENCIL_1:def 2 for l being Block of S st 2 c= card (l /\ T) holds l c= T; attrT is strong means :Def3: :: PENCIL_1:def 3 for x, y being Point of S st x in T & y in T holds x,y are_collinear ; end; :: deftheorem Def2 defines closed_under_lines PENCIL_1:def_2_:_ for S being TopStruct for T being Subset of S holds ( T is closed_under_lines iff for l being Block of S st 2 c= card (l /\ T) holds l c= T ); :: deftheorem Def3 defines strong PENCIL_1:def_3_:_ for S being TopStruct for T being Subset of S holds ( T is strong iff for x, y being Point of S st x in T & y in T holds x,y are_collinear ); definition let S be TopStruct ; attrS is void means :Def4: :: PENCIL_1:def 4 the topology of S is empty ; attrS is degenerated means :Def5: :: PENCIL_1:def 5 the carrier of S is Block of S; attrS is with_non_trivial_blocks means :Def6: :: PENCIL_1:def 6 for k being Block of S holds 2 c= card k; attrS is identifying_close_blocks means :Def7: :: PENCIL_1:def 7 for k, l being Block of S st 2 c= card (k /\ l) holds k = l; attrS is truly-partial means :Def8: :: PENCIL_1:def 8 not for x, y being Point of S holds x,y are_collinear ; attrS is without_isolated_points means :Def9: :: PENCIL_1:def 9 for x being Point of S ex l being Block of S st x in l; attrS is connected means :: PENCIL_1:def 10 for x, y being Point of S ex f being FinSequence of the carrier of S st ( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds for a, b being Point of S st a = f . i & b = f . (i + 1) holds a,b are_collinear ) ); attrS is strongly_connected means :Def11: :: PENCIL_1:def 11 for x being Point of S for X being Subset of S st X is closed_under_lines & X is strong holds ex f being FinSequence of bool the carrier of S st ( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ); end; :: deftheorem Def4 defines void PENCIL_1:def_4_:_ for S being TopStruct holds ( S is void iff the topology of S is empty ); :: deftheorem Def5 defines degenerated PENCIL_1:def_5_:_ for S being TopStruct holds ( S is degenerated iff the carrier of S is Block of S ); :: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def_6_:_ for S being TopStruct holds ( S is with_non_trivial_blocks iff for k being Block of S holds 2 c= card k ); :: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def_7_:_ for S being TopStruct holds ( S is identifying_close_blocks iff for k, l being Block of S st 2 c= card (k /\ l) holds k = l ); :: deftheorem Def8 defines truly-partial PENCIL_1:def_8_:_ for S being TopStruct holds ( S is truly-partial iff not for x, y being Point of S holds x,y are_collinear ); :: deftheorem Def9 defines without_isolated_points PENCIL_1:def_9_:_ for S being TopStruct holds ( S is without_isolated_points iff for x being Point of S ex l being Block of S st x in l ); :: deftheorem defines connected PENCIL_1:def_10_:_ for S being TopStruct holds ( S is connected iff for x, y being Point of S ex f being FinSequence of the carrier of S st ( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds for a, b being Point of S st a = f . i & b = f . (i + 1) holds a,b are_collinear ) ) ); :: deftheorem Def11 defines strongly_connected PENCIL_1:def_11_:_ for S being TopStruct holds ( S is strongly_connected iff for x being Point of S for X being Subset of S st X is closed_under_lines & X is strong holds ex f being FinSequence of bool the carrier of S st ( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) ) ) ); theorem Th7: :: PENCIL_1:7 for X being non empty set st 3 c= card X holds for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } holds ( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) proofend; theorem Th8: :: PENCIL_1:8 for X being non empty set st 3 c= card X holds for K being Subset of X st card K = 2 holds for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } \ {K} holds ( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) proofend; registration cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks non truly-partial without_isolated_points for TopStruct ; existence ex b1 being TopStruct st ( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & not b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points ) proofend; cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points for TopStruct ; existence ex b1 being TopStruct st ( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points ) proofend; end; registration let S be non void TopStruct ; cluster the topology of S -> non empty ; coherence not the topology of S is empty by Def4; end; definition let S be without_isolated_points TopStruct ; let x, y be Point of S; redefine pred x,y are_collinear means :: PENCIL_1:def 12 ex l being Block of S st {x,y} c= l; compatibility ( x,y are_collinear iff ex l being Block of S st {x,y} c= l ) proofend; end; :: deftheorem defines are_collinear PENCIL_1:def_12_:_ for S being without_isolated_points TopStruct for x, y being Point of S holds ( x,y are_collinear iff ex l being Block of S st {x,y} c= l ); definition mode PLS is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct ; end; definition let F be Relation; attrF is TopStruct-yielding means :Def13: :: PENCIL_1:def 13 for x being set st x in rng F holds x is TopStruct ; end; :: deftheorem Def13 defines TopStruct-yielding PENCIL_1:def_13_:_ for F being Relation holds ( F is TopStruct-yielding iff for x being set st x in rng F holds x is TopStruct ); registration cluster Relation-like Function-like TopStruct-yielding -> 1-sorted-yielding for set ; coherence for b1 being Function st b1 is TopStruct-yielding holds b1 is 1-sorted-yielding proofend; end; registration let I be set ; cluster Relation-like I -defined Function-like V14(I) TopStruct-yielding for set ; existence ex b1 being ManySortedSet of I st b1 is TopStruct-yielding proofend; end; registration cluster Relation-like Function-like TopStruct-yielding for set ; existence ex b1 being Function st b1 is TopStruct-yielding proofend; end; definition let F be Relation; attrF is non-void-yielding means :Def14: :: PENCIL_1:def 14 for S being TopStruct st S in rng F holds not S is void ; end; :: deftheorem Def14 defines non-void-yielding PENCIL_1:def_14_:_ for F being Relation holds ( F is non-void-yielding iff for S being TopStruct st S in rng F holds not S is void ); definition let F be TopStruct-yielding Function; redefine attr F is non-void-yielding means :: PENCIL_1:def 15 for i being set st i in rng F holds i is non void TopStruct ; compatibility ( F is non-void-yielding iff for i being set st i in rng F holds i is non void TopStruct ) proofend; end; :: deftheorem defines non-void-yielding PENCIL_1:def_15_:_ for F being TopStruct-yielding Function holds ( F is non-void-yielding iff for i being set st i in rng F holds i is non void TopStruct ); definition let F be Relation; attrF is trivial-yielding means :Def16: :: PENCIL_1:def 16 for S being set st S in rng F holds S is trivial ; end; :: deftheorem Def16 defines trivial-yielding PENCIL_1:def_16_:_ for F being Relation holds ( F is trivial-yielding iff for S being set st S in rng F holds S is trivial ); definition let F be Relation; attrF is non-Trivial-yielding means :Def17: :: PENCIL_1:def 17 for S being 1-sorted st S in rng F holds not S is trivial ; end; :: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def_17_:_ for F being Relation holds ( F is non-Trivial-yielding iff for S being 1-sorted st S in rng F holds not S is trivial ); registration cluster Relation-like non-Trivial-yielding -> non-Empty for set ; coherence for b1 being Relation st b1 is non-Trivial-yielding holds b1 is non-Empty proofend; end; definition let F be 1-sorted-yielding Function; redefine attr F is non-Trivial-yielding means :: PENCIL_1:def 18 for i being set st i in rng F holds i is non trivial 1-sorted ; compatibility ( F is non-Trivial-yielding iff for i being set st i in rng F holds i is non trivial 1-sorted ) proofend; end; :: deftheorem defines non-Trivial-yielding PENCIL_1:def_18_:_ for F being 1-sorted-yielding Function holds ( F is non-Trivial-yielding iff for i being set st i in rng F holds i is non trivial 1-sorted ); definition let I be non empty set ; let A be TopStruct-yielding ManySortedSet of I; let j be Element of I; :: original:. redefine funcA . j -> TopStruct ; coherence A . j is TopStruct proofend; end; definition let F be Relation; attrF is PLS-yielding means :Def19: :: PENCIL_1:def 19 for x being set st x in rng F holds x is PLS; end; :: deftheorem Def19 defines PLS-yielding PENCIL_1:def_19_:_ for F being Relation holds ( F is PLS-yielding iff for x being set st x in rng F holds x is PLS ); registration cluster Relation-like Function-like PLS-yielding -> non-Empty TopStruct-yielding for set ; coherence for b1 being Function st b1 is PLS-yielding holds ( b1 is non-Empty & b1 is TopStruct-yielding ) proofend; cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-void-yielding for set ; coherence for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds b1 is non-void-yielding proofend; cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-Trivial-yielding for set ; coherence for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds b1 is non-Trivial-yielding proofend; end; registration let I be set ; cluster Relation-like I -defined Function-like V14(I) PLS-yielding for set ; existence ex b1 being ManySortedSet of I st b1 is PLS-yielding proofend; end; definition let I be non empty set ; let A be PLS-yielding ManySortedSet of I; let j be Element of I; :: original:. redefine funcA . j -> PLS; coherence A . j is PLS proofend; end; definition let I be set ; let A be ManySortedSet of I; attrA is Segre-like means :Def20: :: PENCIL_1:def 20 ex i being Element of I st for j being Element of I st i <> j holds A . j is 1 -element ; end; :: deftheorem Def20 defines Segre-like PENCIL_1:def_20_:_ for I being set for A being ManySortedSet of I holds ( A is Segre-like iff ex i being Element of I st for j being Element of I st i <> j holds A . j is 1 -element ); registration let I be set ; let A be ManySortedSet of I; cluster{A} -> trivial-yielding ; coherence {A} is trivial-yielding proofend; end; theorem :: PENCIL_1:9 for I being non empty set for A being ManySortedSet of I for i being Element of I for S being non trivial set holds not A +* (i,S) is trivial-yielding proofend; registration let I be non empty set ; let A be ManySortedSet of I; cluster{A} -> Segre-like ; coherence {A} is Segre-like proofend; end; theorem :: PENCIL_1:10 for I being non empty set for A being ManySortedSet of I for i, S being set holds {A} +* (i,S) is Segre-like proofend; theorem Th11: :: PENCIL_1:11 for I being non empty set for A being 1-sorted-yielding non-Empty ManySortedSet of I for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A proofend; registration let I be non empty set ; let A be 1-sorted-yielding non-Empty ManySortedSet of I; cluster Relation-like V2() I -defined Function-like V14(I) trivial-yielding Segre-like for ManySortedSubset of Carrier A; existence ex b1 being ManySortedSubset of Carrier A st ( b1 is Segre-like & b1 is trivial-yielding & b1 is V2() ) proofend; end; registration let I be non empty set ; let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I; cluster Relation-like V2() I -defined Function-like V14(I) non trivial-yielding Segre-like for ManySortedSubset of Carrier A; existence ex b1 being ManySortedSubset of Carrier A st ( b1 is Segre-like & not b1 is trivial-yielding & b1 is V2() ) proofend; end; registration let I be non empty set ; cluster Relation-like I -defined Function-like V14(I) non trivial-yielding Segre-like for set ; existence ex b1 being ManySortedSet of I st ( b1 is Segre-like & not b1 is trivial-yielding ) proofend; end; definition let I be non empty set ; let B be non trivial-yielding Segre-like ManySortedSet of I; func indx B -> Element of I means :Def21: :: PENCIL_1:def 21 not B . it is trivial ; existence not for b1 being Element of I holds B . b1 is trivial proofend; uniqueness for b1, b2 being Element of I st not B . b1 is trivial & not B . b2 is trivial holds b1 = b2 proofend; end; :: deftheorem Def21 defines indx PENCIL_1:def_21_:_ for I being non empty set for B being non trivial-yielding Segre-like ManySortedSet of I for b3 being Element of I holds ( b3 = indx B iff not B . b3 is trivial ); theorem Th12: :: PENCIL_1:12 for I being non empty set for A being non trivial-yielding Segre-like ManySortedSet of I for i being Element of I st i <> indx A holds A . i is 1 -element proofend; registration let I be non empty set ; cluster Relation-like I -defined Function-like V14(I) non trivial-yielding Segre-like -> V2() for set ; coherence for b1 being ManySortedSet of I st b1 is Segre-like & not b1 is trivial-yielding holds b1 is V2() proofend; end; theorem Th13: :: PENCIL_1:13 for I being non empty set for A being ManySortedSet of I holds ( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) ) proofend; registration let I be non empty set ; let B be non trivial-yielding Segre-like ManySortedSet of I; cluster product B -> non trivial ; coherence not product B is trivial proofend; end; begin definition let I be non empty set ; let A be non-Empty TopStruct-yielding ManySortedSet of I; func Segre_Blocks A -> Subset-Family of (product (Carrier A)) means :Def22: :: PENCIL_1:def 22 for x being set holds ( x in it iff ex B being Segre-like ManySortedSubset of Carrier A st ( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ); existence ex b1 being Subset-Family of (product (Carrier A)) st for x being set holds ( x in b1 iff ex B being Segre-like ManySortedSubset of Carrier A st ( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) proofend; uniqueness for b1, b2 being Subset-Family of (product (Carrier A)) st ( for x being set holds ( x in b1 iff ex B being Segre-like ManySortedSubset of Carrier A st ( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) & ( for x being set holds ( x in b2 iff ex B being Segre-like ManySortedSubset of Carrier A st ( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def22 defines Segre_Blocks PENCIL_1:def_22_:_ for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I for b3 being Subset-Family of (product (Carrier A)) holds ( b3 = Segre_Blocks A iff for x being set holds ( x in b3 iff ex B being Segre-like ManySortedSubset of Carrier A st ( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ); definition let I be non empty set ; let A be non-Empty TopStruct-yielding ManySortedSet of I; func Segre_Product A -> non empty TopStruct equals :: PENCIL_1:def 23 TopStruct(# (product (Carrier A)),(Segre_Blocks A) #); correctness coherence TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) is non empty TopStruct ; ; end; :: deftheorem defines Segre_Product PENCIL_1:def_23_:_ for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I holds Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #); theorem Th14: :: PENCIL_1:14 for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I for x being Point of (Segre_Product A) holds x is ManySortedSet of I proofend; theorem Th15: :: PENCIL_1:15 for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds not Segre_Product A is void proofend; theorem Th16: :: PENCIL_1:16 for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds ( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds not Segre_Product A is degenerated proofend; theorem Th17: :: PENCIL_1:17 for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds ( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds Segre_Product A is with_non_trivial_blocks proofend; theorem Th18: :: PENCIL_1:18 for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds ( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds Segre_Product A is identifying_close_blocks proofend; registration let I be non empty set ; let A be PLS-yielding ManySortedSet of I; cluster Segre_Product A -> non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ; coherence ( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks ) proofend; end; theorem :: PENCIL_1:19 for T being TopStruct for S being Subset of T st S is trivial holds ( S is strong & S is closed_under_lines ) proofend; theorem Th20: :: PENCIL_1:20 for S being identifying_close_blocks TopStruct for l being Block of S for L being Subset of S st L = l holds L is closed_under_lines proofend; theorem Th21: :: PENCIL_1:21 for S being TopStruct for l being Block of S for L being Subset of S st L = l holds L is strong proofend; theorem :: PENCIL_1:22 for S being non void TopStruct holds [#] S is closed_under_lines proofend; theorem Th23: :: PENCIL_1:23 for I being non empty set for A being non trivial-yielding Segre-like ManySortedSet of I for x, y being ManySortedSet of I st x in product A & y in product A holds for i being set st i <> indx A holds x . i = y . i proofend; theorem Th24: :: PENCIL_1:24 for I being non empty set for A being PLS-yielding ManySortedSet of I for x being set holds ( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( x = product L & L . (indx L) is Block of (A . (indx L)) ) ) proofend; theorem Th25: :: PENCIL_1:25 for I being non empty set for A being PLS-yielding ManySortedSet of I for P being ManySortedSet of I st P is Point of (Segre_Product A) holds for i being Element of I for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A) proofend; theorem Th26: :: PENCIL_1:26 for I being non empty set for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds ( indx A = indx B & ( for i being set st i <> indx A holds A . i = B . i ) ) proofend; theorem Th27: :: PENCIL_1:27 for I being non empty set for A being non trivial-yielding Segre-like ManySortedSet of I for N being non trivial set holds ( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding ) proofend; theorem :: PENCIL_1:28 for S being non empty non void identifying_close_blocks without_isolated_points TopStruct st S is strongly_connected holds S is connected proofend; theorem :: PENCIL_1:29 for I being non empty set for A being PLS-yielding ManySortedSet of I for S being Subset of (Segre_Product A) holds ( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds ( C is strong & C is closed_under_lines ) ) ) ) proofend;