:: On Segre's Product of Partial Line Spaces
:: by Adam Naumowicz
::
:: Received May 29, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


theorem Th1: :: PENCIL_1:1
for f, g being Function st product f = product g & f is non-empty holds
g is non-empty
proof end;

theorem Th2: :: PENCIL_1:2
for X being set holds
( 2 c= card X iff ex x, y being object st
( x in X & y in X & x <> y ) )
proof end;

theorem Th3: :: PENCIL_1:3
for X being set st 2 c= card X holds
for x being object ex y being object st
( y in X & x <> y )
proof end;

theorem Th4: :: PENCIL_1:4
for X being set holds
( 2 c= card X iff not X is trivial )
proof end;

theorem Th5: :: PENCIL_1:5
for X being set holds
( 3 c= card X iff ex x, y, z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )
proof end;

theorem Th6: :: PENCIL_1:6
for X being set st 3 c= card X holds
for x, y being object ex z being object st
( z in X & x <> z & y <> z )
proof end;

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;
pred x,y are_collinear means :: PENCIL_1:def 1
( x = y or ex l being Block of S st {x,y} c= l );
end;

:: deftheorem 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;
attr T is closed_under_lines means :: PENCIL_1:def 2
 for l being Block of S st 2 c= card (l /\ T) holds
l c= T;
attr T is strong means :: 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 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 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 ;
attr S is void means :Def4: :: PENCIL_1:def 4
 the topology of S is empty ;
attr S is degenerated means :: PENCIL_1:def 5
 the carrier of S is Block of S;
attr S is with_non_trivial_blocks means :Def6: :: PENCIL_1:def 6
 for k being Block of S holds 2 c= card k;
attr S 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;
attr S is truly-partial means :: PENCIL_1:def 8
 not for x, y being Point of S holds x,y are_collinear ;
attr S 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;
attr S 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 ) );
attr S is strongly_connected means :: 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 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 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 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 )
proof end;

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 )
proof end;

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 )
proof end;
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 )
proof end;
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 )
proof end;
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;
attr F is non-void-yielding means :: PENCIL_1:def 14
 for S being TopStruct st S in rng F holds
not S is void ;
end;

:: deftheorem PENCIL_1:def 13 :
canceled;

:: deftheorem 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 ) by WAYBEL18:def 1;
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;
attr F 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;
attr F 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 ;
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 ) by PRALG_1:def 11;
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 func A . j -> TopStruct ;
coherence
A . j is TopStruct
proof end;
end;

definition
let F be Relation;
attr F 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 ) ;
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 ;
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
proof end;
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
proof end;
end;

definition
let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
let j be Element of I;
:: original: .
redefine func A . j -> PLS;
coherence
A . j is PLS
proof end;
end;

definition
let I be set ;
let A be ManySortedSet of I;
attr A 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
proof end;
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
proof end;

registration
let I be non empty set ;
let A be ManySortedSet of I;
cluster {A} -> Segre-like ;
coherence
{A} is Segre-like
proof end;
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
proof end;

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
proof end;

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() )
proof end;
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() )
proof end;
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 )
proof end;
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
proof end;
uniqueness
for b1, b2 being Element of I st not B . b1 is trivial & not B . b2 is trivial holds
b1 = b2
proof end;
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
proof end;

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()
proof end;
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 ) )
proof end;

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
proof end;
end;

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) ) )
proof end;
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
proof end;
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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;
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 )
proof end;

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 by Def7;

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
proof end;

theorem :: PENCIL_1:22
for S being non void TopStruct holds [#] S is closed_under_lines
proof end;

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 object st i <> indx A holds
x . i = y . i
proof end;

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)) ) )
proof end;

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)
proof end;

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 object st i <> indx A holds
A . i = B . i ) )
proof end;

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 )
proof end;

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
proof end;

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 ) ) ) )
proof end;