:: Several Classes of {BCI}-algebras and Their Properties
:: by Yuzhong Ding
::
:: Received February 23, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem defines \ BCIALG_1:def 1 :
:: deftheorem defines ` BCIALG_1:def 2 :
:: deftheorem Def3 defines being_B BCIALG_1:def 3 :
:: deftheorem Def4 defines being_C BCIALG_1:def 4 :
:: deftheorem Def5 defines being_I BCIALG_1:def 5 :
:: deftheorem Def6 defines being_K BCIALG_1:def 6 :
:: deftheorem Def7 defines being_BCI-4 BCIALG_1:def 7 :
:: deftheorem Def8 defines being_BCK-5 BCIALG_1:def 8 :
:: deftheorem defines BCI-EXAMPLE BCIALG_1:def 9 :
:: deftheorem Def10 defines SubAlgebra BCIALG_1:def 10 :
theorem Th1: :: BCIALG_1:1
:: deftheorem Def11 defines <= BCIALG_1:def 11 :
Lm1:
for X being BCI-algebra
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X
theorem Th2: :: BCIALG_1:2
theorem Th3: :: BCIALG_1:3
theorem Th4: :: BCIALG_1:4
theorem :: BCIALG_1:5
theorem :: BCIALG_1:6
theorem Th7: :: BCIALG_1:7
theorem Th8: :: BCIALG_1:8
theorem Th9: :: BCIALG_1:9
theorem Th10: :: BCIALG_1:10
theorem :: BCIALG_1:11
theorem :: BCIALG_1:12
theorem :: BCIALG_1:13
theorem :: BCIALG_1:14
theorem :: BCIALG_1:15
theorem :: BCIALG_1:16
theorem :: BCIALG_1:17
theorem :: BCIALG_1:18
:: deftheorem defines BCK-part BCIALG_1:def 12 :
theorem Th19: :: BCIALG_1:19
theorem :: BCIALG_1:20
theorem :: BCIALG_1:21
theorem Th22: :: BCIALG_1:22
:: deftheorem Def13 defines proper BCIALG_1:def 13 :
:: deftheorem Def14 defines atom BCIALG_1:def 14 :
:: deftheorem defines AtomSet BCIALG_1:def 15 :
theorem Th23: :: BCIALG_1:23
theorem Th24: :: BCIALG_1:24
theorem :: BCIALG_1:25
theorem :: BCIALG_1:26
theorem :: BCIALG_1:27
theorem Th28: :: BCIALG_1:28
theorem Th29: :: BCIALG_1:29
theorem Th30: :: BCIALG_1:30
theorem Th31: :: BCIALG_1:31
theorem :: BCIALG_1:32
theorem Th33: :: BCIALG_1:33
theorem Th34: :: BCIALG_1:34
theorem Th35: :: BCIALG_1:35
:: deftheorem Def16 defines generated_by_atom BCIALG_1:def 16 :
:: deftheorem defines BranchV BCIALG_1:def 17 :
theorem :: BCIALG_1:36
theorem :: BCIALG_1:37
theorem Th38: :: BCIALG_1:38
Lm2:
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BranchV a holds a \ x = 0. X
theorem Th39: :: BCIALG_1:39
theorem :: BCIALG_1:40
theorem :: BCIALG_1:41
theorem :: BCIALG_1:42
:: deftheorem Def18 defines Ideal BCIALG_1:def 18 :
:: deftheorem Def19 defines closed BCIALG_1:def 19 :
Lm3:
for X being BCI-algebra holds {(0. X)} is Ideal of X
Lm4:
for X being BCI-algebra
for X1 being Ideal of X st X1 = {(0. X)} holds
for x being Element of X1 holds x ` in {(0. X)}
theorem :: BCIALG_1:43
theorem :: BCIALG_1:44
theorem :: BCIALG_1:45
Lm5:
for X being BCI-algebra
for IT being non empty Subset of X st IT is Ideal of X holds
for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT
theorem :: BCIALG_1:46
:: deftheorem Def20 defines associative BCIALG_1:def 20 :
:: deftheorem Def21 defines quasi-associative BCIALG_1:def 21 :
:: deftheorem Def22 defines positive-implicative BCIALG_1:def 22 :
:: deftheorem Def23 defines weakly-positive-implicative BCIALG_1:def 23 :
:: deftheorem Def24 defines implicative BCIALG_1:def 24 :
:: deftheorem defines weakly-implicative BCIALG_1:def 25 :
:: deftheorem Def26 defines p-Semisimple BCIALG_1:def 26 :
:: deftheorem Def27 defines alternative BCIALG_1:def 27 :
Lm6:
for X being BCI-algebra st ( for x, y being Element of X holds y \ x = x \ y ) holds
X is associative
Lm7:
for X being BCI-algebra st ( for x being Element of X holds x ` = x ) holds
for x, y being Element of X holds x \ y = y \ x
theorem Th47: :: BCIALG_1:47
theorem Th48: :: BCIALG_1:48
theorem Th49: :: BCIALG_1:49
theorem Th50: :: BCIALG_1:50
theorem :: BCIALG_1:51
theorem :: BCIALG_1:52
theorem :: BCIALG_1:53
Lm8:
for X being BCI-algebra holds
( ( for x being Element of X holds (x ` ) ` = x ) iff for x, y being Element of X holds y \ (y \ x) = x )
Lm9:
for X being BCI-algebra holds
( ( for x, y being Element of X holds y \ (y \ x) = x ) iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )
theorem Th54: :: BCIALG_1:54
theorem Th55: :: BCIALG_1:55
theorem Th56: :: BCIALG_1:56
theorem Th57: :: BCIALG_1:57
Lm10:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z, u being Element of X holds
( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )
Lm11:
for X being BCI-algebra st X is p-Semisimple holds
for x, y being Element of X holds (y ` ) \ ((0. X) \ x) = x \ y
Lm12:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z
Lm13:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st x \ y = x \ z holds
y = z
Lm14:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x ` )
Lm15:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st y \ x = z \ x holds
y = z
theorem :: BCIALG_1:58
theorem Th59: :: BCIALG_1:59
theorem :: BCIALG_1:60
theorem :: BCIALG_1:61
theorem Th62: :: BCIALG_1:62
theorem Th63: :: BCIALG_1:63
theorem :: BCIALG_1:64
theorem :: BCIALG_1:65
theorem :: BCIALG_1:66
theorem :: BCIALG_1:67
theorem :: BCIALG_1:68
theorem :: BCIALG_1:69
theorem :: BCIALG_1:70
Lm16:
for X being BCI-algebra st ( for x being Element of X holds x ` <= x ) holds
for x, y being Element of X holds (x \ y) ` = (y \ x) `
Lm17:
for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) holds
for x, y being Element of X holds (x ` ) \ y = (x \ y) `
Lm18:
for X being BCI-algebra st ( for x, y being Element of X holds (x ` ) \ y = (x \ y) ` ) holds
for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X
Lm19:
for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) holds
X is quasi-associative
Lm20:
for X being BCI-algebra holds
( ( for x being Element of X holds x ` <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )
theorem Th71: :: BCIALG_1:71
theorem Th72: :: BCIALG_1:72
theorem Th73: :: BCIALG_1:73
theorem :: BCIALG_1:74
theorem :: BCIALG_1:75
theorem Th76: :: BCIALG_1:76
theorem :: BCIALG_1:77
theorem :: BCIALG_1:78
theorem :: BCIALG_1:79
theorem :: BCIALG_1:80
Lm21:
for X being BCI-algebra holds
( X is alternative iff X is associative )
Lm22:
for X being BCI-algebra st X is alternative holds
X is implicative
theorem :: BCIALG_1:81
theorem :: BCIALG_1:82
Lm23:
for X being BCI-algebra st X is associative holds
X is weakly-positive-implicative
Lm24:
for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is weakly-positive-implicative BCI-algebra
theorem :: BCIALG_1:83
theorem Th84: :: BCIALG_1:84
Lm25:
for X being BCI-algebra
for x, y being Element of X st X is weakly-positive-implicative holds
(x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)
Lm26:
for X being BCI-algebra holds
( X is positive-implicative iff X is weakly-positive-implicative )
theorem :: BCIALG_1:85
theorem :: BCIALG_1:86