:: by Tao Sun , Weibo Pan , Chenglong Wu and Xiquan Liang

::

:: Received May 13, 2008

:: Copyright (c) 2008-2019 Association of Mizar Users

definition

let X be BCI-algebra;

let x, y be Element of X;

let m, n be Nat;

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

end;
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;

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

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

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;

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;

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 )

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 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

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

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

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)

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)

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)

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)

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;

end;
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);

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);

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

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
end;

definition

let i, j, m, n be Nat;

ex b_{1} being BCI-algebra st

for x, y being Element of b_{1} holds Polynom (i,j,x,y) = Polynom (m,n,y,x)

end;
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 for x, y being Element of it holds Polynom (i,j,x,y) = Polynom (m,n,y,x);

ex b

for x, y being Element of b

proof end;

:: deftheorem Def3 defines BCI-algebra BCIALG_5:def 3 :

for i, j, m, n being Nat

for b_{5} being BCI-algebra holds

( b_{5} is BCI-algebra of i,j,m,n iff for x, y being Element of b_{5} holds Polynom (i,j,x,y) = Polynom (m,n,y,x) );

for i, j, m, n being Nat

for b

( b

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 )

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

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

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

let i, j, m, n be Nat;

existence

ex b_{1} being BCI-algebra of i,j,m,n st b_{1} is being_BCK-5

end;
existence

ex b

proof end;

definition
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 )

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

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

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)

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)

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;

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

definition

let i, j, m, n be Nat;

correctness

coherence

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

;

correctness

coherence

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

;

end;
correctness

coherence

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

;

correctness

coherence

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

;

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

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)));

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 )

( 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 )

( 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 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 )

( 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

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

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

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

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

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

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

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

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

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

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 )

( 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 )

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

proof 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)}

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)} )

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)} )

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

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 )

( 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

X is BCI-algebra of 0 ,1,1,1

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 )

( 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 )

( X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1, 0 , 0 , 0 )

proof end;

registration

for b_{1} being BCK-algebra st b_{1} is BCK-implicative holds

b_{1} is commutative
by BCIALG_3:34;

for b_{1} being BCK-algebra st b_{1} is BCK-implicative holds

b_{1} is BCK-positive-implicative
by BCIALG_3:34;

end;

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

coherence for b

b

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

b

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 ) )

( 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;

( 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) )

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

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

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

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

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

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;