:: General Theory of Quasi-Commutative BCI-algebras
:: by Tao Sun , Weibo Pan , Chenglong Wu and Xiquan Liang
::
:: Received May 13, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users

definition

let X be BCI-algebra;
let x, y be Element of X;
let m, n be Nat;

func Polynom (m,n,x,y) -> Element of X equals :: BCIALG_5:def 1
(((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n;

coherence
(((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n is Element of X ;

end;

:: deftheorem defines Polynom BCIALG_5:def 1 :
for X being BCI-algebra
for x, y being Element of X
for m, n being Nat holds Polynom (m,n,x,y) = (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n;

theorem Th1: :: BCIALG_5:1

for X being BCI-algebra
for x, y, z being Element of X st x <= y & y <= z holds
x <= z by BCIALG_1:3;

theorem Th2: :: BCIALG_5:2

for X being BCI-algebra
for x, y being Element of X st x <= y & y <= x holds
x = y by BCIALG_1:def 7;

theorem Th3: :: BCIALG_5:3

for n being Nat
for X being BCK-algebra
for x, y being Element of X holds
( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n )

proof end;

theorem Th4: :: BCIALG_5:4

for n being Nat
for X being BCK-algebra
for x being Element of X holds ((0. X),x) to_power n = 0. X

proof end;

theorem Th5: :: BCIALG_5:5

for m, n being Nat
for X being BCK-algebra
for x, y being Element of X st m >= n holds
(x,y) to_power m <= (x,y) to_power n

proof end;

theorem Th6: :: BCIALG_5:6

for m, n being Nat
for X being BCK-algebra
for x, y being Element of X st m > n & (x,y) to_power n = (x,y) to_power m holds
for k being Nat st k >= n holds
(x,y) to_power n = (x,y) to_power k

proof end;

theorem Th7: :: BCIALG_5:7

for X being BCI-algebra
for x, y being Element of X holds Polynom (0,0,x,y) = x \ (x \ y)

proof end;

theorem :: BCIALG_5:8

for X being BCI-algebra
for x, y being Element of X
for m, n being Nat holds Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n

proof end;

theorem Th9: :: BCIALG_5:9

for X being BCI-algebra
for x, y being Element of X
for m, n being Nat holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y)

proof end;

theorem Th10: :: BCIALG_5:10

for X being BCI-algebra
for x, y being Element of X
for m, n being Nat holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x)

proof end;

theorem :: BCIALG_5:11

for X being BCI-algebra
for x, y being Element of X
for n being Nat holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y)

proof end;

theorem :: BCIALG_5:12

for X being BCI-algebra
for x, y being Element of X
for n being Nat holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x)

proof end;

definition

let X be BCI-algebra;

attr X is quasi-commutative means :: BCIALG_5:def 2
ex i, j, m, n being Element of NAT st
for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (m,n,y,x);

end;

:: deftheorem defines quasi-commutative BCIALG_5:def 2 :
for X being BCI-algebra holds
( X is quasi-commutative iff ex i, j, m, n being Element of NAT st
for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (m,n,y,x) );

registration

cluster BCI-EXAMPLE -> quasi-commutative ;

coherence
BCI-EXAMPLE is quasi-commutative

proof end;

end;

registration

cluster non empty being_B being_C being_I being_BCI-4 quasi-commutative for BCIStr_0 ;

existence
ex b₁ being BCI-algebra st b₁ is quasi-commutative

proof end;

end;

definition

let i, j, m, n be Nat;

mode BCI-algebra of i,j,m,n -> BCI-algebra means :Def3: :: BCIALG_5:def 3
for x, y being Element of it holds Polynom (i,j,x,y) = Polynom (m,n,y,x);

existence
ex b₁ being BCI-algebra st
for x, y being Element of b₁ holds Polynom (i,j,x,y) = Polynom (m,n,y,x)

proof end;

end;

:: deftheorem Def3 defines BCI-algebra BCIALG_5:def 3 :
for i, j, m, n being Nat
for b₅ being BCI-algebra holds
( b₅ is BCI-algebra of i,j,m,n iff for x, y being Element of b₅ holds Polynom (i,j,x,y) = Polynom (m,n,y,x) );

theorem Th13: :: BCIALG_5:13

for X being BCI-algebra
for i, j, m, n being Nat holds
( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j )

proof end;

theorem Th14: :: BCIALG_5:14

for i, j, m, n being Nat
for X being BCI-algebra of i,j,m,n
for k being Element of NAT holds X is BCI-algebra of i + k,j,m,n + k

proof end;

theorem :: BCIALG_5:15

for i, j, m, n being Nat
for X being BCI-algebra of i,j,m,n
for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n

proof end;

registration

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 quasi-commutative for BCIStr_0 ;

existence
ex b₁ being BCK-algebra st b₁ is quasi-commutative

proof end;

end;

registration

let i, j, m, n be Nat;

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 for BCI-algebra of i,j,m,n;

existence
ex b₁ being BCI-algebra of i,j,m,n st b₁ is being_BCK-5

proof end;

end;

definition

let i, j, m, n be Nat;
mode BCK-algebra of i,j,m,n is being_BCK-5 BCI-algebra of i,j,m,n;

end;

theorem :: BCIALG_5:16

for X being BCI-algebra
for i, j, m, n being Nat holds
( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j )

proof end;

theorem Th17: :: BCIALG_5:17

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n
for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k

proof end;

theorem Th18: :: BCIALG_5:18

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n
for k being Element of NAT holds X is BCK-algebra of i,j + k,m + k,n

proof end;

theorem Th19: :: BCIALG_5:19

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n
for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1)

proof end;

theorem Th20: :: BCIALG_5:20

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n
for x, y being Element of X holds (x,y) to_power (j + 1) = (x,y) to_power (m + 1)

proof end;

theorem Th21: :: BCIALG_5:21

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j,j,n

proof end;

theorem Th22: :: BCIALG_5:22

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n

proof end;

:: The Reduction of the Type of Quasi-Commutative BCK-algebra

definition

let i, j, m, n be Nat;

func min (i,j,m,n) -> ExtReal equals :: BCIALG_5:def 4
min ((min (i,j)),(min (m,n)));

correctness
coherence
min ((min (i,j)),(min (m,n))) is ExtReal;
;

func max (i,j,m,n) -> ExtReal equals :: BCIALG_5:def 5
max ((max (i,j)),(max (m,n)));

correctness
coherence
max ((max (i,j)),(max (m,n))) is ExtReal;
;

end;

:: deftheorem defines min BCIALG_5:def 4 :
for i, j, m, n being Nat holds min (i,j,m,n) = min ((min (i,j)),(min (m,n)));

:: deftheorem defines max BCIALG_5:def 5 :
for i, j, m, n being Nat holds max (i,j,m,n) = max ((max (i,j)),(max (m,n)));

theorem :: BCIALG_5:23

for i, j, m, n being Nat holds
( min (i,j,m,n) = i or min (i,j,m,n) = j or min (i,j,m,n) = m or min (i,j,m,n) = n )

proof end;

theorem :: BCIALG_5:24

for i, j, m, n being Nat holds
( max (i,j,m,n) = i or max (i,j,m,n) = j or max (i,j,m,n) = m or max (i,j,m,n) = n )

proof end;

theorem Th25: :: BCIALG_5:25

for i, j, m, n being Nat st i = min (i,j,m,n) holds
( i <= j & i <= m & i <= n )

proof end;

theorem Th26: :: BCIALG_5:26

for i, j, m, n being Nat holds
( max (i,j,m,n) >= i & max (i,j,m,n) >= j & max (i,j,m,n) >= m & max (i,j,m,n) >= n )

proof end;

theorem Th27: :: BCIALG_5:27

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = j holds
X is BCK-algebra of i,i,i,i

proof end;

theorem :: BCIALG_5:28

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i < j & i < n holds
X is BCK-algebra of i,i + 1,i,i + 1

proof end;

theorem :: BCIALG_5:29

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = n & i = m holds
X is BCK-algebra of i,i,i,i

proof end;

theorem :: BCIALG_5:30

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i = n & m < j holds
X is BCK-algebra of i,m + 1,m,i

proof end;

theorem :: BCIALG_5:31

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i = n holds
X is BCK-algebra of i,j,j,i

proof end;

theorem :: BCIALG_5:32

for i, j, k, l, m, n being Nat
for X being BCK-algebra of i,j,m,n st l >= j & k >= n holds
X is BCK-algebra of k,l,l,k

proof end;

theorem :: BCIALG_5:33

for i, j, k, m, n being Nat
for X being BCK-algebra of i,j,m,n st k >= max (i,j,m,n) holds
X is BCK-algebra of k,k,k,k

proof end;

theorem :: BCIALG_5:34

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i <= m & j <= n holds
X is BCK-algebra of i,j,i,j

proof end;

theorem :: BCIALG_5:35

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i <= m & i < n holds
X is BCK-algebra of i,j,i,i + 1

proof end;

theorem Th36: :: BCIALG_5:36

for X being BCI-algebra
for i, j, k being Nat st X is BCI-algebra of i,j,j + k,i + k holds
X is BCK-algebra

proof end;

::Some Special Classes of Quasi-Commutative BCI-algebra

theorem Th37: :: BCIALG_5:37

for X being BCI-algebra holds
( X is BCI-algebra of 0 , 0 , 0 , 0 iff X is BCK-algebra of 0 , 0 , 0 , 0 )

proof end;

theorem Th38: :: BCIALG_5:38

for X being BCI-algebra holds
( X is commutative BCK-algebra iff X is BCI-algebra of 0 , 0 , 0 , 0 )

proof end;

notation

let X be BCI-algebra;
synonym p-Semisimple-part X for AtomSet X;

end;

theorem :: BCIALG_5:39

for X being BCI-algebra
for B, P being non empty Subset of X
for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds
B /\ P = {(0. X)}

proof end;

theorem :: BCIALG_5:40

for X being BCI-algebra
for P being non empty Subset of X
for X being BCI-algebra st P = p-Semisimple-part X holds
( X is BCK-algebra iff P = {(0. X)} )

proof end;

theorem :: BCIALG_5:41

for X being BCI-algebra
for B being non empty Subset of X
for X being BCI-algebra st B = BCK-part X holds
( X is p-Semisimple BCI-algebra iff B = {(0. X)} )

proof end;

theorem Th42: :: BCIALG_5:42

for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is BCI-algebra of 0 ,1, 0 , 0

proof end;

theorem :: BCIALG_5:43

for X being BCI-algebra
for j, m, n being Nat st X is p-Semisimple BCI-algebra holds
X is BCI-algebra of n + j,n,m,(m + j) + 1

proof end;

theorem :: BCIALG_5:44

for X being BCI-algebra st X is associative BCI-algebra holds
( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 )

proof end;

theorem :: BCIALG_5:45

for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds
X is BCI-algebra of 0 ,1,1,1

proof end;

theorem :: BCIALG_5:46

for X being BCI-algebra st X is positive-implicative BCI-algebra holds
X is BCI-algebra of 0 ,1,1,1

proof end;

theorem :: BCIALG_5:47

for X being BCI-algebra st X is implicative BCI-algebra holds
X is BCI-algebra of 0 ,1, 0 , 0

proof end;

theorem :: BCIALG_5:48

for X being BCI-algebra st X is alternative BCI-algebra holds
X is BCI-algebra of 0 ,1, 0 , 0

proof end;

theorem Th49: :: BCIALG_5:49

for X being BCI-algebra holds
( X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0 ,1, 0 ,1 )

proof end;

theorem Th50: :: BCIALG_5:50

for X being BCI-algebra holds
( X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1, 0 , 0 , 0 )

proof end;

registration

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative -> commutative for BCIStr_0 ;

coherence
for b₁ being BCK-algebra st b₁ is BCK-implicative holds
b₁ is commutative by BCIALG_3:34;

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative -> BCK-positive-implicative for BCIStr_0 ;

coherence
for b₁ being BCK-algebra st b₁ is BCK-implicative holds
b₁ is BCK-positive-implicative by BCIALG_3:34;

end;

theorem :: BCIALG_5:51

for X being BCI-algebra holds
( X is BCK-algebra of 1, 0 , 0 , 0 iff ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) )

proof end;

theorem :: BCIALG_5:52

for X being quasi-commutative BCK-algebra holds
( X is BCK-algebra of 0 ,1, 0 ,1 iff for x, y being Element of X holds x \ y = (x \ y) \ y ) by BCIALG_3:28, Th49;

theorem :: BCIALG_5:53

for n being Nat
for X being quasi-commutative BCK-algebra holds
( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) )

proof end;

theorem :: BCIALG_5:54

for X being BCI-algebra st X is BCI-algebra of 0 ,1, 0 , 0 holds
X is BCI-commutative BCI-algebra

proof end;

theorem :: BCIALG_5:55

for X being BCI-algebra
for m, n being Nat st X is BCI-algebra of n, 0 ,m,m holds
X is BCI-commutative BCI-algebra

proof end;

theorem :: BCIALG_5:56

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st j = 0 & m > 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0

proof end;

theorem :: BCIALG_5:57

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st m = 0 & j > 0 holds
X is BCK-algebra of 0 ,1, 0 ,1

proof end;

theorem :: BCIALG_5:58

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st n = 0 & i <> 0 holds
X is BCK-algebra of 0 , 0 , 0 , 0

proof end;

theorem :: BCIALG_5:59

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i = 0 & n <> 0 holds
X is BCK-algebra of 0 ,1, 0 ,1

proof end;