:: On Segre's Product of Partial Line Spaces
:: by Adam Naumowicz
::
:: Received May 29, 2000
:: Copyright (c) 2000-2011 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

proof end;

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 ) )

proof end;

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 )

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 set 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 set ex z being set st
( z in X & x <> z & y <> z )

proof end;

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;
pred x,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;
attr T 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;
attr T 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 ;
attr S is void means :Def4: :: PENCIL_1:def 4
the topology of S is empty ;
attr S is degenerated means :Def5: :: 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 :Def8: :: 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 :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 )

proof end;

Lm1: ex S being TopStruct st
( S is strict & 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;

Lm2: ex S being TopStruct st
( S is strict & 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 TopStruct ;
existence
ex b₁ being TopStruct st
( b₁ is strict & not b₁ is empty & not b₁ is void & not b₁ is degenerated & not b₁ is truly-partial & b₁ is with_non_trivial_blocks & b₁ is identifying_close_blocks & b₁ is without_isolated_points ) by Lm1;
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points TopStruct ;
existence
ex b₁ being TopStruct st
( b₁ is strict & not b₁ is empty & not b₁ is void & not b₁ is degenerated & b₁ is truly-partial & b₁ is with_non_trivial_blocks & b₁ is identifying_close_blocks & b₁ is without_isolated_points ) by Lm2;

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 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 set ;
coherence
for b₁ being Function st b₁ is TopStruct-yielding holds
b₁ is 1-sorted-yielding

proof end;

end;

registration

let I be set ;
cluster Relation-like I -defined Function-like V17(I) TopStruct-yielding set ;
existence
ex b₁ being ManySortedSet of I st b₁ is TopStruct-yielding

proof end;

end;

registration

cluster Relation-like Function-like TopStruct-yielding set ;
existence
ex b₁ being Function st b₁ is TopStruct-yielding

proof end;

end;

definition

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

proof end;

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 set ;
coherence
for b₁ being Relation st b₁ is non-Trivial-yielding holds
b₁ is non-Empty

proof end;

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 )

proof end;

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 set ;
coherence
for b₁ being Function st b₁ is PLS-yielding holds
( b₁ is non-Empty & b₁ is TopStruct-yielding )

proof end;

cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-void-yielding set ;
coherence
for b₁ being TopStruct-yielding Function st b₁ is PLS-yielding holds
b₁ is non-void-yielding

proof end;

cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-Trivial-yielding set ;
coherence
for b₁ being TopStruct-yielding Function st b₁ is PLS-yielding holds
b₁ is non-Trivial-yielding

proof end;

end;

registration

let I be set ;
cluster Relation-like I -defined Function-like V17(I) PLS-yielding set ;
existence
ex b₁ being ManySortedSet of I st b₁ 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
( not A . j is empty & A . j is trivial );

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
( not A . j is empty & A . j is trivial ) );

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 V5() I -defined Function-like V17(I) trivial-yielding Segre-like ManySortedSubset of Carrier A;
existence
ex b₁ being ManySortedSubset of Carrier A st
( b₁ is Segre-like & b₁ is trivial-yielding & b₁ is non-empty )

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 V5() I -defined Function-like V17(I) non trivial-yielding Segre-like ManySortedSubset of Carrier A;
existence
ex b₁ being ManySortedSubset of Carrier A st
( b₁ is Segre-like & not b₁ is trivial-yielding & b₁ is non-empty )

proof end;

end;

registration

let I be non empty set ;
cluster Relation-like I -defined Function-like V17(I) non trivial-yielding Segre-like set ;
existence
ex b₁ being ManySortedSet of I st
( b₁ is Segre-like & not b₁ 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 b₁ being Element of I holds B . b₁ is trivial

proof end;

uniqueness
for b₁, b₂ being Element of I st not B . b₁ is trivial & not B . b₂ is trivial holds
b₁ = b₂

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 b₃ being Element of I holds
( b₃ = indx B iff not B . b₃ 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
( not A . i is empty & A . i is trivial )

proof end;

registration

let I be non empty set ;
cluster Relation-like I -defined Function-like V17(I) non trivial-yielding Segre-like -> V5() set ;
coherence
for b₁ being ManySortedSet of I st b₁ is Segre-like & not b₁ is trivial-yielding holds
b₁ is non-empty

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 non-empty & 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;

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 b₁ being Subset-Family of (product (Carrier A)) st
for x being set holds
( x in b₁ 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 b₁, b₂ being Subset-Family of (product (Carrier A)) st ( for x being set holds
( x in b₁ 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 b₂ 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
b₁ = b₂

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 b₃ being Subset-Family of (product (Carrier A)) holds
( b₃ = Segre_Blocks A iff for x being set holds
( x in b₃ 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

proof end;

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 set 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 set 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;