:: 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
:: deftheorem defines Polynom BCIALG_5:def 1 :
theorem Th1: :: BCIALG_5:1
theorem Th2: :: BCIALG_5:2
theorem Th3: :: BCIALG_5:3
theorem Th4: :: BCIALG_5:4
theorem Th5: :: BCIALG_5:5
theorem Th6: :: BCIALG_5:6
theorem Th7: :: BCIALG_5:7
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
theorem Th9: :: BCIALG_5:9
theorem Th10: :: BCIALG_5:10
theorem :: BCIALG_5:11
theorem :: BCIALG_5:12
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 );
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 b1 being BCI-algebra st
for x, y being Element of b1 holds Polynom i,j,x,y = Polynom m,n,y,x
end;
:: deftheorem Def3 defines BCI-algebra BCIALG_5:def 3 :
for
i,
j,
m,
n being
Element of
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
theorem Th14: :: BCIALG_5:14
theorem :: BCIALG_5:15
theorem :: BCIALG_5:16
theorem Th17: :: BCIALG_5:17
theorem Th18: :: BCIALG_5:18
theorem Th19: :: BCIALG_5:19
theorem Th20: :: BCIALG_5:20
theorem Th21: :: BCIALG_5:21
theorem Th22: :: BCIALG_5:22
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 :
:: deftheorem defines max BCIALG_5:def 5 :
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 )
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 )
theorem Th25: :: BCIALG_5:25
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 )
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
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
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
theorem :: BCIALG_5:30
theorem :: BCIALG_5:31
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
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
theorem :: BCIALG_5:34
theorem :: BCIALG_5:35
theorem Th36: :: BCIALG_5:36
theorem Th37: :: BCIALG_5:37
theorem Th38: :: BCIALG_5:38
theorem :: BCIALG_5:39
theorem :: BCIALG_5:40
theorem :: BCIALG_5:41
theorem Th42: :: BCIALG_5:42
theorem :: BCIALG_5:43
theorem :: BCIALG_5:44
theorem :: BCIALG_5:45
theorem :: BCIALG_5:46
theorem :: BCIALG_5:47
theorem :: BCIALG_5:48
theorem Th49: :: BCIALG_5:49
theorem Th50: :: BCIALG_5:50
theorem :: BCIALG_5:51
theorem :: BCIALG_5:52
theorem :: BCIALG_5:53
theorem :: BCIALG_5:54
theorem :: BCIALG_5:55
theorem :: BCIALG_5:56
theorem :: BCIALG_5:57
theorem :: BCIALG_5:58
theorem :: BCIALG_5:59