:: On the Characterization of Collineations of the Segre Product of Strongly
:: Connected Partial Linear Spaces
::  by Adam Naumowicz
::
:: Received October 18, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, STRUCT_0, PRE_TOPC, PENCIL_2, PENCIL_1,
      FUNCT_1, RELAT_1, TARSKI, SUBSET_1, PRALG_1, PBOOLE, ZFMISC_1, RELAT_2,
      FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, WAYBEL_3, RLVECT_2,
      CARD_3, INTEGRA1, FUNCT_4, FINSET_1, FDIFF_1, PARSP_1, GRAPH_2, FUNCT_2,
      CAT_1, RCOMP_1, FUNCOP_1, PENCIL_3, WAYBEL18;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XCMPLX_0, XXREAL_0, ORDINAL1, NUMBERS,
      NAT_1, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1, CARD_1,
      FINSET_1, FINSEQ_1, CARD_3, DOMAIN_1, STRUCT_0, PRE_TOPC, PBOOLE,
      PZFMISC1, T_0TOPSP, PRALG_1, WAYBEL_3, WAYBEL18, PENCIL_1, FUNCT_7,
      PENCIL_2, TOPS_2, FINSEQ_6, GRAPH_2;
 constructors PZFMISC1, TOPS_2, REALSET2, T_0TOPSP, GRAPH_2, PENCIL_2,
      RELSET_1, PBOOLE, FUNCT_7, PRE_POLY, FINSEQ_6;
 registrations SUBSET_1, RELSET_1, FUNCT_2, XREAL_0, NAT_1, CARD_1, PBOOLE,
      STRUCT_0, PENCIL_1, ORDINAL1, FUNCT_1, RELAT_1, FINSEQ_1, PRE_POLY,
      WAYBEL18;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;


begin :: Preliminaries

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

theorem :: PENCIL_3:2
  for I being non empty set for i be Element of I for A being
  non-Trivial-yielding 1-sorted-yielding ManySortedSet of I holds A.i is non
  trivial;

theorem :: PENCIL_3:3
  for S being non void identifying_close_blocks TopStruct st S is
  strongly_connected holds S is without_isolated_points;

theorem :: PENCIL_3:4
  for S being non empty non void identifying_close_blocks TopStruct
  holds S is strongly_connected implies S is connected;

theorem :: PENCIL_3:5
  for S being non void non degenerated TopStruct for L being Block of S
  ex x being Point of S st not x in L;

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

theorem :: PENCIL_3:7
  for I being non empty set for A be 1-sorted-yielding
  ManySortedSet of I for x being Element of I holds (Carrier A).x = [#](A.x);

theorem :: PENCIL_3:8
  for I being non empty set for i being Element of I for A be
  non-Trivial-yielding TopStruct-yielding ManySortedSet of I ex L being
  Segre-like non trivial-yielding ManySortedSubset of Carrier A st indx(L)=i &
  product L is Segre-Coset of A;

theorem :: PENCIL_3:9
  for I being non empty set for i being Element of I for A be
non-Trivial-yielding TopStruct-yielding ManySortedSet of I for p being Point
of Segre_Product A ex L being Segre-like non trivial-yielding ManySortedSubset
  of Carrier A st indx(L)=i & product L is Segre-Coset of A & p in product L;

theorem :: PENCIL_3:10
  for I being non empty set for A being non-Trivial-yielding
  TopStruct-yielding ManySortedSet of I for b being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b is Segre-Coset of A
  holds b.indx(b) = [#](A.indx(b));

theorem :: PENCIL_3:11
  for I being non empty set for A be non-Trivial-yielding
  TopStruct-yielding ManySortedSet of I for L1,L2 being Segre-like non
trivial-yielding 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;

theorem :: PENCIL_3:12
  for I being non empty set for A be PLS-yielding ManySortedSet of
I for L being Segre-like non trivial-yielding ManySortedSubset of Carrier A for
  B being Block of A.indx(L) holds product(L+*(indx(L),B)) is Block of
  Segre_Product A;

theorem :: PENCIL_3:13
  for I being non empty set for A be PLS-yielding ManySortedSet of
I for i being Element of I for p being Point of A.i for L being Segre-like non
  trivial-yielding ManySortedSubset of Carrier A st i<>indx(L) holds L+*(i,{p})
  is Segre-like non trivial-yielding ManySortedSubset of Carrier A;

theorem :: 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 Segre-like
non trivial-yielding ManySortedSubset of Carrier A holds product (L+*(i,S)) is
  Subset of Segre_Product A;

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

theorem :: PENCIL_3:16
  for I being non empty set for i being Element of I for A be
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;

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

theorem :: PENCIL_3:18
  for I being non empty set for A being PLS-yielding ManySortedSet
of I for b being Segre-like non trivial-yielding 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) qua set} = product(b+*(indx(b),{x}));

definition
  let I be finite non empty 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};
end;

theorem :: PENCIL_3:19
  for I being finite non empty 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;

begin :: The adherence of Segre cosets

definition
  let I be non empty set;
  let A be PLS-yielding ManySortedSet of I;
  let B1,B2 be Segre-Coset of A;
  pred B1 '||' B2 means
:: PENCIL_3:def 2

  for x being Point of Segre_Product A st x in B1
  ex y being Point of Segre_Product A st y in B2 & x,y are_collinear;
end;

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

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

theorem :: PENCIL_3:22
  for I being finite non empty set for A being PLS-yielding
  ManySortedSet of I st for i being Element of I holds A.i is connected for i
  being Element of I for p being Point of A.i for b1,b2 being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st product b2 is Segre-Coset of
  A & b1=b2+*(i,{p}) & not p in b2.i 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 for Di,Di1 being Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1
  & Di '||' Di1;

theorem :: PENCIL_3:23
  for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is connected for B1,B2
  being Segre-Coset of A st B1 misses B2 for b1,b2 being Segre-like non
  trivial-yielding 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 for Di
  ,Di1 being Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di
  '||' Di1;

theorem :: PENCIL_3:24
  for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is strongly_connected
  for f being Collineation of Segre_Product A for B1,B2 being Segre-Coset of A
  for b1,b2,b3,b4 being Segre-like non trivial-yielding ManySortedSubset of
  Carrier A st B1 = product b1 & B2 = product b2 & f.:B1 = product b3 & f.:B2 =
  product b4 holds indx(b1)=indx(b2) implies indx(b3)=indx(b4);

theorem :: PENCIL_3:25
  for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is strongly_connected
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 Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 =
  product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j;

definition
  let I be finite non empty set;
  let A be PLS-yielding ManySortedSet of I such that
 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
:: 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 Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 =
  product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j;
end;

begin :: Canonical embeddings and automorphisms of Segre product

definition
  let I be finite non empty set;
  let A be PLS-yielding ManySortedSet of I such that
 for i being Element of I holds A.i is strongly_connected;
  let f be Collineation of Segre_Product A;
  let b1 be Segre-like non trivial-yielding ManySortedSubset of Carrier A such
  that
 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
:: 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 for b
being ManySortedSet of I st b=f.a holds b.(permutation_of_indices(f).indx(b1))=
  it.(a.indx(b1));
end;

theorem :: PENCIL_3:26
  for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is strongly_connected
for f being Collineation of Segre_Product A for B1,B2 being Segre-Coset of A st
  B1 misses B2 & B1 '||' B2 for b1,b2 being Segre-like non trivial-yielding
  ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds
  canonical_embedding(f,b1) = canonical_embedding(f,b2);

theorem :: PENCIL_3:27
  for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is strongly_connected
  for f being Collineation of Segre_Product A for b1,b2 being Segre-like non
trivial-yielding 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);

definition
  let I be finite non empty set;
  let A be PLS-yielding ManySortedSet of I such that
 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
:: PENCIL_3:def 5

  for b being Segre-like non trivial-yielding ManySortedSubset
  of Carrier A st product b is Segre-Coset of A & indx(b)=i holds it=
  canonical_embedding(f,b);
end;

theorem :: PENCIL_3:28
  for I being finite non empty set for A being PLS-yielding
ManySortedSet of I st for i being Element of I holds A.i is strongly_connected
  for f being Collineation of Segre_Product A ex s being Permutation of I, 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 for b being ManySortedSet of I st b=f.p for m being
  Function of A.i,A.(s.i) st m=B.i holds b.(s.i)=m.(a.i);