The abstract of the Mizar article:

On Segre's Product of Partial Line Spaces

by

Adam Naumowicz

Received May 29, 2000

MML identifier: PENCIL_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, CARD_3, ZF_REFLE, RELAT_1, BOOLE, CARD_1, REALSET1,
      PRE_TOPC, AMI_1, VECTSP_1, RELAT_2, FINSEQ_1, FINSET_1, SETFAM_1,
      PRALG_1, PBOOLE, FUNCOP_1, WAYBEL_3, FUNCT_4, RLVECT_2, MSUALG_2,
      INTEGRA1, SUBSET_1, ARYTM_1, PENCIL_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0,
      SETFAM_1, NAT_1, FINSET_1, RELAT_1, STRUCT_0, FUNCT_1, REALSET1,
      WAYBEL_3, CARD_1, FINSEQ_1, CARD_3, PRE_TOPC, PBOOLE, MSUALG_1, MSUALG_2,
      PZFMISC1, PRE_CIRC, PRALG_1, POLYNOM1;
 constructors PRE_CIRC, WAYBEL_3, ENUMSET1, MSUALG_2, POLYNOM1, PZFMISC1,
      CQC_LANG;
 clusters STRUCT_0, RELSET_1, SUBSET_1, FINSET_1, YELLOW_6, PRALG_1, TEX_1,
      TEX_2, YELLOW13, REALSET1, PZFMISC1, XREAL_0, ARYTM_3, XBOOLE_0;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;


begin

theorem :: PENCIL_1:1
for f,g being Function st product f = product g holds
f is non-empty implies g is non-empty;

theorem :: 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;

theorem :: PENCIL_1:3
for X being set st 2 c= Card X
for x being set ex y being set st y in X & x<>y;

theorem :: PENCIL_1:4
for X being set holds 2 c= Card X iff X is non trivial;

theorem :: 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;

theorem :: PENCIL_1:6
for X being set st 3 c= Card X
for x,y being set ex z being set st z in X & x<>z & y<>z;

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

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;

definition
let S be TopStruct;
attr S is void means
:: 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
:: PENCIL_1:def 6
 for k being Block of S holds 2 c= Card k;
attr S is identifying_close_blocks means
:: 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
 ex x,y being Point of S st not x,y are_collinear;
attr S is without_isolated_points means
:: 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
 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 strong
 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 strong) &
 for i being Nat st 1 <= i & i < len f holds
 2 c= Card((f.i) /\ (f.(i+1)));
end;

theorem :: PENCIL_1:7
for X being non empty set st 3 c= Card X
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
S is non empty non void
non degenerated non truly-partial with_non_trivial_blocks
identifying_close_blocks without_isolated_points;

theorem :: PENCIL_1:8
for X being non empty set st 3 c= Card X
for K being Subset of X st Card K = 2
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
S is non empty non void
non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks
without_isolated_points;

definition
cluster strict non empty non void non degenerated non truly-partial
        with_non_trivial_blocks identifying_close_blocks
        without_isolated_points TopStruct;
cluster strict non empty non void non degenerated truly-partial
        with_non_trivial_blocks identifying_close_blocks
        without_isolated_points TopStruct;
end;

definition
let S be non void TopStruct;
cluster the topology of S -> non empty;
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;
end;

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
:: PENCIL_1:def 13
 for x being set st x in rng F holds x is TopStruct;
end;

definition
 cluster TopStruct-yielding -> 1-sorted-yielding Function;
end;

definition let I be set;
 cluster TopStruct-yielding ManySortedSet of I;
end;

definition
cluster TopStruct-yielding Function;
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 S is non void;
end;

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

definition
let F be Relation;
attr F is trivial-yielding means
:: PENCIL_1:def 16
for S being set st S in rng F holds S is trivial;
end;

definition
let F be Relation;
attr F is non-Trivial-yielding means
:: PENCIL_1:def 17
for S being 1-sorted st S in rng F holds S is non trivial;
end;

definition
cluster non-Trivial-yielding -> non-Empty Relation;
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;
end;

definition let I be non empty set;
           let A be TopStruct-yielding ManySortedSet of I;
           let j be Element of I;
 redefine func A.j -> TopStruct;
end;

definition let F be Relation;
attr F is PLS-yielding means
:: PENCIL_1:def 19
 for x being set st x in rng F holds x is PLS;
end;

definition
 cluster PLS-yielding -> non-Empty TopStruct-yielding Function;
 cluster PLS-yielding -> non-void-yielding (TopStruct-yielding Function);
 cluster PLS-yielding -> non-Trivial-yielding (TopStruct-yielding Function);
end;

definition let I be set;
 cluster PLS-yielding ManySortedSet of I;
end;

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

definition
let I be set;
let A be ManySortedSet of I;
attr A is Segre-like means
:: PENCIL_1:def 20
ex i being Element of I st for j being Element of I st i<>j
holds A.j is non empty trivial;
end;

definition
let I be set;
let A be ManySortedSet of I;
cluster {A} -> trivial-yielding;
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
A+*(i,S) is non trivial-yielding;

definition
let I be non empty set;
let A be ManySortedSet of I;
cluster {A} -> Segre-like;
end;

theorem :: PENCIL_1:10
  for I being non empty set
for A being ManySortedSet of I
for i,S be set holds
{A}+*(i,S) is Segre-like;

theorem :: PENCIL_1:11
for I being non empty set
for A being non-Empty (1-sorted-yielding ManySortedSet of I)
for B being Element of Carrier A holds
{B} is ManySortedSubset of Carrier A;

definition
let I be non empty set;
let A be non-Empty (1-sorted-yielding ManySortedSet of I);
cluster Segre-like trivial-yielding non-empty ManySortedSubset of Carrier A;
end;

definition
let I be non empty set;
let A be non-Trivial-yielding (1-sorted-yielding ManySortedSet of I);
cluster Segre-like non trivial-yielding non-empty
ManySortedSubset of Carrier A;
end;

definition
let I be non empty set;
cluster Segre-like non trivial-yielding ManySortedSet of I;
end;

definition
let I be non empty set;
let B be Segre-like non trivial-yielding ManySortedSet of I;
func indx(B) -> Element of I means
:: PENCIL_1:def 21
B.it is non trivial;
end;

theorem :: PENCIL_1:12
for I being non empty set
for A being Segre-like non trivial-yielding ManySortedSet of I
for i being Element of I st i <> indx(A) holds A.i is non empty trivial;

definition
let I be non empty set;
cluster Segre-like non trivial-yielding -> non-empty ManySortedSet of I;
end;

theorem :: 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 non trivial-yielding;

definition
let I be non empty set;
let B be Segre-like non trivial-yielding ManySortedSet of I;
cluster product B -> non trivial;
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
:: 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;
end;

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

theorem :: PENCIL_1:14
for I being non empty set
for A be non-Empty (TopStruct-yielding ManySortedSet of I)
for x being Point of Segre_Product A holds x is ManySortedSet of I;

theorem :: PENCIL_1:15
for I being non empty set
for A being non-Empty (TopStruct-yielding ManySortedSet of I)
st ex i being Element of I st A.i is non void
holds Segre_Product A is non void;

theorem :: 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 A.i is non degenerated &
ex i being Element of I st A.i is non void
holds Segre_Product A is non degenerated;

theorem :: 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 &
ex i being Element of I st A.i is non void
holds Segre_Product A is with_non_trivial_blocks;

theorem :: 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 with_non_trivial_blocks &
ex i being Element of I st A.i is non void
holds Segre_Product A is identifying_close_blocks;

definition
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
redefine func Segre_Product A -> PLS;
end;

theorem :: PENCIL_1:19
  for T being TopStruct
for S being Subset of T holds
S is trivial implies S is strong closed_under_lines;

theorem :: PENCIL_1:20
 for S being identifying_close_blocks TopStruct, l being Block of S
 for L being Subset of S st L=l holds
 L is closed_under_lines;

theorem :: PENCIL_1:21
 for S being TopStruct, l being Block of S
 for L being Subset of S st L=l holds L is strong;

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

theorem :: PENCIL_1:23
for I being non empty set
for A being Segre-like non trivial-yielding ManySortedSet of I
for x,y being ManySortedSet of I st x in product A & y in product A
for i being set st i <> indx(A) holds x.i = y.i;

theorem :: 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 Segre-like non trivial-yielding ManySortedSubset of Carrier A st
x = product L & L.indx(L) is Block of A.indx(L);

theorem :: 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
for i being Element of I
for p being Point of A.i holds
P+*(i,p) is Point of Segre_Product A;

theorem :: PENCIL_1:26
for I being non empty set
for A,B being Segre-like non trivial-yielding 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;

theorem :: PENCIL_1:27
for I being non empty set
for A being Segre-like non trivial-yielding ManySortedSet of I
for N being non trivial set holds
A+*(indx(A),N) is Segre-like non trivial-yielding;

theorem :: PENCIL_1:28
  for S being non empty non void identifying_close_blocks
without_isolated_points
TopStruct holds S is strongly_connected implies S is connected;

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
S is non trivial strong closed_under_lines iff
ex B being Segre-like non trivial-yielding
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 closed_under_lines;