:: BCI-Algebras with Condition (S) and Their Properties
::  by Tao Sun , Junjie Zhao and Xiquan Liang
::
:: Received November 24, 2007
:: Copyright (c) 2007-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 BCIALG_1, STRUCT_0, BINOP_1, SUBSET_1, XBOOLE_0, RELAT_1,
      FUNCT_1, FUNCT_5, ZFMISC_1, NUMBERS, FINSEQ_1, XXREAL_0, SUPINF_2,
      VECTSP_1, ALGSTR_0, RLVECT_1, ARYTM_3, SETWISEO, GROUP_1, CARD_1, NAT_1,
      NEWTON, POWER, FINSOP_1, ORDINAL4, BCIALG_2, TARSKI, FILTER_0, BCIALG_4;
 notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, BINOP_1, FUNCT_5, STRUCT_0,
      ALGSTR_0, BCIALG_1, RELAT_1, ORDINAL1, NUMBERS, XXREAL_0, FINSEQ_1,
      FINSOP_1, SETWISEO, FUNCT_1, FUNCT_2, FINSEQ_4, XCMPLX_0, RLVECT_1,
      NAT_1, BCIALG_2, VECTSP_1;
 constructors BINOP_1, VECTSP_2, FINSOP_1, SETWISEO, FINSEQ_4, BCIALG_2,
      FUNCT_5, NAT_1;
 registrations BCIALG_1, RELAT_1, STRUCT_0, ORDINAL1, XXREAL_0, VECTSP_1,
      BCIALG_2, CARD_1;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM;


begin :: Definition and Elementary Properties of BCI-Algebras with Condition(S)

definition
  struct (BCIStr_0,ZeroStr) BCIStr_1 (# carrier -> set, ExternalDiff,
    InternalDiff -> BinOp of the carrier, ZeroF -> Element of the carrier #);
end;

registration
  cluster non empty strict for BCIStr_1;
end;

definition
  let A be BCIStr_1;
  let x,y be Element of A;
  func x * y -> Element of A equals
:: BCIALG_4:def 1
  (the ExternalDiff of A).(x,y);
end;

definition
  let IT be non empty BCIStr_1;
  attr IT is with_condition_S means
:: BCIALG_4:def 2

  for x,y,z being Element of IT holds (x\y)\z = x\(y*z);
end;

definition
  func BCI_S-EXAMPLE -> BCIStr_1 equals
:: BCIALG_4:def 3
  BCIStr_1 (# {0}, op2, op2, op0 #);
end;

registration
  cluster BCI_S-EXAMPLE -> strict 1-element;
end;

registration
  cluster BCI_S-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5
    with_condition_S;
end;

registration
  cluster strict being_B being_C being_I being_BCI-4 with_condition_S for non
    empty BCIStr_1;
end;

definition
  mode BCI-Algebra_with_Condition(S) is being_B being_C being_I being_BCI-4
    with_condition_S non empty BCIStr_1;
end;

reserve X for non empty BCIStr_1;
reserve d for Element of X;
reserve n,m,k for Nat;
reserve f for sequence of  the carrier of X;

definition
  let X be BCI-Algebra_with_Condition(S);
  let x,y be Element of X;
  func Condition_S(x,y) -> non empty Subset of X equals
:: BCIALG_4:def 4
  {t where t is Element
  of X: t\x <= y};
end;

theorem :: BCIALG_4:1
  for X be BCI-Algebra_with_Condition(S),x,y,u,v being Element of X st u
  in Condition_S(x,y) & v <= u holds v in Condition_S(x,y);

theorem :: BCIALG_4:2
  for X being BCI-Algebra_with_Condition(S) holds for x,y being Element
  of X holds ex a be Element of Condition_S(x,y) st for z being Element of
  Condition_S(x,y) holds z <= a;

theorem :: BCIALG_4:3
  X is BCI-algebra & (for x,y being Element of X holds ((x*y)\x <= y &
  for t being Element of X st t\x <= y holds t <= (x*y))) iff X is
  BCI-Algebra_with_Condition(S);

definition
  let X be p-Semisimple BCI-algebra;
  func Adjoint_pGroup X -> strict AbGroup means
:: BCIALG_4:def 5
  the carrier of it = the
carrier of X & (for x,y being Element of X holds (the addF of it).(x,y) = x\(0.
  X\y)) & 0.it = 0.X;
end;

::$CT

theorem :: BCIALG_4:5
  for X being BCI-algebra holds X is p-Semisimple iff for x,y being
  Element of X st x\y = 0.X holds x=y;

theorem :: BCIALG_4:6
  for X being BCI-Algebra_with_Condition(S) st X is p-Semisimple holds
  for x,y being Element of X holds x*y = x\(0.X\y);

theorem :: BCIALG_4:7  :: Commutativity
  for X being BCI-Algebra_with_Condition(S) holds for x,y being
  Element of X holds x*y = y*x;

theorem :: BCIALG_4:8  :: Isotonic Property
  for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds x <= y implies x*z <= y*z & z*x <= z*y;

theorem :: BCIALG_4:9  :: Unit Element
  for X being BCI-Algebra_with_Condition(S) holds for x being
  Element of X holds 0.X*x = x & x*0.X = x;

theorem :: BCIALG_4:10  :: Associativity
  for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds (x*y)*z = x*(y*z);

theorem :: BCIALG_4:11
  for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds (x*y)*z = (x*z)*y;

theorem :: BCIALG_4:12
  for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds (x\y)\z = x\(y*z);

theorem :: BCIALG_4:13
  for X being BCI-Algebra_with_Condition(S) holds for x,y being
  Element of X holds y <= x*(y\x);

theorem :: BCIALG_4:14
  for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds (x*z)\(y*z) <= x\y;

theorem :: BCIALG_4:15
  for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds x\y <= z iff x <= y*z;

theorem :: BCIALG_4:16
  for X being BCI-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds x\y <= (x\z)*(z\y);

registration
  let X be BCI-Algebra_with_Condition(S);
  cluster the ExternalDiff of X -> commutative associative;
end;

theorem :: BCIALG_4:17
  for X being BCI-Algebra_with_Condition(S) holds 0.X
  is_a_unity_wrt the ExternalDiff of X;

theorem :: BCIALG_4:18
  for X being BCI-Algebra_with_Condition(S) holds the_unity_wrt the
  ExternalDiff of X = 0.X;

theorem :: BCIALG_4:19
  for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff
  of X is having_a_unity;

definition
  let X be BCI-Algebra_with_Condition(S);
  func power X -> Function of [:the carrier of X,NAT:], the carrier of X means
:: BCIALG_4:def 6

  for h being Element of X holds it.(h,0) = 0.X &
    for n holds it.(h,n + 1) = it.(h,n) * h;
end;

definition
  let X be BCI-Algebra_with_Condition(S);
  let x be Element of X;
  let n be Nat;
  func x |^ n -> Element of X equals
:: BCIALG_4:def 7
  power(X).(x,n);
end;

theorem :: BCIALG_4:20
  for X being BCI-Algebra_with_Condition(S) holds for x being Element of
  X holds x |^ 0 = 0.X;

theorem :: BCIALG_4:21
  for X being BCI-Algebra_with_Condition(S) holds for x being Element of
  X holds x |^ (n + 1) = (x|^n) * x;

theorem :: BCIALG_4:22
  for X being BCI-Algebra_with_Condition(S) holds for x being
  Element of X holds x |^ 1 = x;

theorem :: BCIALG_4:23
  for X being BCI-Algebra_with_Condition(S) holds for x being
  Element of X holds x |^ 2 = x * x;

theorem :: BCIALG_4:24
  for X being BCI-Algebra_with_Condition(S) holds for x being Element of
  X holds x |^ 3 = x * x * x;

theorem :: BCIALG_4:25
  for X being BCI-Algebra_with_Condition(S) holds (0.X) |^ 2 = 0.X;

theorem :: BCIALG_4:26
  for X being BCI-Algebra_with_Condition(S) holds (0.X)|^n = 0.X;

theorem :: BCIALG_4:27
  for X being BCI-Algebra_with_Condition(S) holds for x,a being Element
  of X holds ((x\a)\a)\a = x\(a|^3);

theorem :: BCIALG_4:28
  for X being BCI-Algebra_with_Condition(S) holds for x,a being Element
  of X holds (x,a) to_power n = x\(a|^n);

definition
  let X be non empty BCIStr_1;
  let F be FinSequence of the carrier of X;
  func Product_S F -> Element of X equals
:: BCIALG_4:def 8
  (the ExternalDiff of X) "**" F;
end;

theorem :: BCIALG_4:29
  (the ExternalDiff of X) "**" <* d *> = d;

theorem :: BCIALG_4:30
  for X being BCI-Algebra_with_Condition(S), F1,F2 being FinSequence of
  the carrier of X holds Product_S(F1 ^ F2) = Product_S(F1) * Product_S(F2);

theorem :: BCIALG_4:31
  for X being BCI-Algebra_with_Condition(S), F being FinSequence of the
carrier of X, a being Element of X holds Product_S(F ^ <* a *>) = Product_S(F)
  * a;

theorem :: BCIALG_4:32
  for X being BCI-Algebra_with_Condition(S), F being FinSequence of the
carrier of X, a being Element of X holds Product_S(<* a *> ^ F) = a * Product_S
  (F);

theorem :: BCIALG_4:33
  for X being BCI-Algebra_with_Condition(S) holds for a1,a2 being
  Element of X holds Product_S<*a1,a2*> = a1 * a2;

theorem :: BCIALG_4:34
  for X being BCI-Algebra_with_Condition(S) holds for a1,a2,a3
  being Element of X holds Product_S<*a1,a2,a3*> = a1 * a2 * a3;

theorem :: BCIALG_4:35
  for X being BCI-Algebra_with_Condition(S) holds for x,a1,a2 being
  Element of X holds (x\a1)\a2 = x\Product_S<*a1,a2*>;

theorem :: BCIALG_4:36
  for X being BCI-Algebra_with_Condition(S) holds for x,a1,a2,a3 being
  Element of X holds ((x\a1)\a2)\a3 = x\Product_S<*a1,a2,a3*>;

theorem :: BCIALG_4:37
  for X being BCI-Algebra_with_Condition(S), a,b being Element of
AtomSet(X) holds for ma being Element of X st (for x being Element of BranchV(a
  ) holds x <= ma) holds ex mb being Element of X st for y being Element of
  BranchV(b) holds y <= mb;

:: Commutative BCK-Algebras with Condition(S)

registration
  cluster strict being_BCK-5 for BCI-Algebra_with_Condition(S);
end;

definition
  mode BCK-Algebra_with_Condition(S) is being_BCK-5
    BCI-Algebra_with_Condition(S);
end;

theorem :: BCIALG_4:38
  for X being BCK-Algebra_with_Condition(S) holds for x,y being
  Element of X holds x <= x*y & y <= x*y;

theorem :: BCIALG_4:39
  for X being BCK-Algebra_with_Condition(S) holds for x,y,z being
  Element of X holds ((x*y)\(y*z))\(z*x) = 0.X;

theorem :: BCIALG_4:40
  for X being BCK-Algebra_with_Condition(S) holds for x,y being Element
  of X holds (x\y)*(y\x) <= x*y;

theorem :: BCIALG_4:41
  for X being BCK-Algebra_with_Condition(S) holds for x being Element of
  X holds (x\0.X)*(0.X\x) = x;

definition
  let IT be BCK-Algebra_with_Condition(S);
  attr IT is commutative means
:: BCIALG_4:def 9

  for x,y being Element of IT holds x\(x\y ) = y\(y\x);
end;

registration
  cluster commutative for BCK-Algebra_with_Condition(S);
end;

theorem :: BCIALG_4:42
  for X being non empty BCIStr_1 holds (X is commutative
BCK-Algebra_with_Condition(S) iff for x,y,z being Element of X holds x\(0.X\y)
  = x & (x\z)\(x\y) = (y\z)\(y\x) & (x\y)\z = x\(y*z) );

theorem :: BCIALG_4:43
  for X being commutative BCK-Algebra_with_Condition(S), a being Element
of X st a is greatest holds for x,y being Element of X holds x*y = a\((a\x)\y);

definition
  let X be BCI-algebra;
  let a be Element of X;
  func Initial_section(a) -> non empty Subset of X equals
:: BCIALG_4:def 10
  {t where t is
  Element of X: t <= a};
end;

theorem :: BCIALG_4:44
  for X being commutative BCK-Algebra_with_Condition(S), a,b,c being
  Element of X st Condition_S(a,b) c= Initial_section(c) holds for x being
  Element of Condition_S(a,b) holds x <= c\((c\a)\b);

:: Positive-Implicative BCK-Algebras with Condition(S)

definition
  let IT be BCK-Algebra_with_Condition(S);
  attr IT is positive-implicative means
:: BCIALG_4:def 11

  for x,y being Element of IT holds (x\y)\y = x\y;
end;

registration
  cluster positive-implicative for BCK-Algebra_with_Condition(S);
end;

theorem :: BCIALG_4:45
  for X being BCK-Algebra_with_Condition(S) holds ( X is
  positive-implicative iff for x being Element of X holds x*x = x );

theorem :: BCIALG_4:46
  for X being BCK-Algebra_with_Condition(S) holds ( X is
positive-implicative iff for x,y being Element of X holds (x <= y implies x*y =
  y) );

theorem :: BCIALG_4:47
  for X being BCK-Algebra_with_Condition(S) holds ( X is
positive-implicative iff for x,y,z being Element of X holds (x*y)\z = (x\z)*(y\
  z) );

theorem :: BCIALG_4:48
  for X being BCK-Algebra_with_Condition(S) holds ( X is
  positive-implicative iff for x,y being Element of X holds x*y = x*(y\x) );

theorem :: BCIALG_4:49
  for X being positive-implicative BCK-Algebra_with_Condition(S)
  holds for x,y being Element of X holds x = (x\y)*(x\(x\y));

definition
  let IT be non empty BCIStr_1;
  attr IT is being_SB-1 means
:: BCIALG_4:def 12

  for x being Element of IT holds x * x = x;
  attr IT is being_SB-2 means
:: BCIALG_4:def 13

  for x,y being Element of IT holds x * y = y * x;
  attr IT is being_SB-4 means
:: BCIALG_4:def 14

  for x,y being Element of IT holds (x\y) * y = x * y;
end;

registration
  cluster BCI_S-EXAMPLE -> being_SB-1 being_SB-2 being_SB-4 being_I
    with_condition_S;
end;

registration
  cluster strict being_SB-1 being_SB-2 being_SB-4 being_I with_condition_S for

    non empty BCIStr_1;
end;

definition
  mode semi-Brouwerian-algebra is being_SB-1 being_SB-2 being_SB-4 being_I
    with_condition_S non empty BCIStr_1;
end;

theorem :: BCIALG_4:50
  for X being non empty BCIStr_1 holds (X is positive-implicative
  BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra);

:: Implicative BCK-Algebras with Condition(S)

definition
  let IT be BCK-Algebra_with_Condition(S);
  attr IT is implicative means
:: BCIALG_4:def 15

  for x,y being Element of IT holds x\(y\ x) = x;
end;

registration
  cluster implicative for BCK-Algebra_with_Condition(S);
end;

theorem :: BCIALG_4:51
  for X being BCK-Algebra_with_Condition(S) holds (X is
  implicative iff X is commutative & X is positive-implicative );

theorem :: BCIALG_4:52
  for X being BCK-Algebra_with_Condition(S) holds ( X is implicative iff
  for x,y,z being Element of X holds x\(y\z) = ((x\y)\z)*(z\(z\x)) );