:: General Theory of Quasi-Commutative BCI-algebras
:: by Tao Sun , Weibo Pan , Chenglong Wu and Xiquan Liang
::
:: 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
coherence
proof end;
end;

registration
existence
ex b1 being BCI-algebra st b1 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 b1 being BCI-algebra st
for x, y being Element of b1 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 b5 being BCI-algebra holds
( b5 is BCI-algebra of i,j,m,n iff for x, y being Element of b5 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
existence
ex b1 being BCK-algebra st b1 is quasi-commutative
proof end;
end;

registration
let i, j, m, n be Nat;
existence
ex b1 being BCI-algebra of i,j,m,n st b1 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
coherence
for b1 being BCK-algebra st b1 is BCK-implicative holds
b1 is commutative
by BCIALG_3:34;
coherence
for b1 being BCK-algebra st b1 is BCK-implicative holds
b1 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 ;

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;