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

begin

definition

let X be BCI-algebra;
let x, y be Element of X;
let m, n be Element of 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 Element of 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

proof end;

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

proof end;

theorem Th3: :: BCIALG_5:3

for n being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 y, x being Element of X
for n being Element of 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 Element of 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 :Def2: :: 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 Def2 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 BCIStr_0 ;
existence
ex b₁ being BCI-algebra st b₁ is quasi-commutative

proof end;

end;

definition

let i, j, m, n be Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 BCIStr_0 ;
existence
ex b₁ being BCK-algebra st b₁ is quasi-commutative

proof end;

end;

registration

let i, j, m, n be Element of NAT ;
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT
for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n

proof end;

definition

let i, j, m, n be Element of NAT ;
func min i,j,m,n -> ext-real number equals :: BCIALG_5:def 4
min (min i,j),(min m,n);
correctness
coherence
min (min i,j),(min m,n) is ext-real number ;
;
func max i,j,m,n -> ext-real number equals :: BCIALG_5:def 5
max (max i,j),(max m,n);
correctness
coherence
max (max i,j),(max m,n) is ext-real number ;
;

end;

:: deftheorem defines min BCIALG_5:def 4 :

for i, j, m, n being Element of 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 Element of NAT holds max i,j,m,n = max (max i,j),(max m,n);

theorem :: BCIALG_5:23

for i, j, m, n being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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, m, n, l, k being Element of 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, m, n, k being Element of 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 Element of 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 Element of 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 Element of NAT st X is BCI-algebra of i,j,j + k,i + k holds
X is BCK-algebra

proof end;

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 n, j, m being Element of 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 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 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 )

proof end;

theorem :: BCIALG_5:53

for n being Element of 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 n, m being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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;