:: BCI-Algebras with Condition (S) and Their Properties
:: by Tao Sun , Junjie Zhao and Xiquan Liang
::
:: Received November 24, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem defines * BCIALG_4:def 1 :
:: deftheorem Def2 defines with_condition_S BCIALG_4:def 2 :
:: deftheorem defines BCI_S-EXAMPLE BCIALG_4:def 3 :
Lm1:
( BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )
:: deftheorem defines Condition_S BCIALG_4:def 4 :
theorem :: BCIALG_4:1
theorem :: BCIALG_4:2
Lm2:
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) )
Lm3:
for X being non empty BCIStr_1 st X is BCI-algebra & ( for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) holds
X is BCI-Algebra_with_Condition(S)
theorem :: BCIALG_4:3
theorem :: BCIALG_4:4
:: deftheorem defines Adjoint_pGroup BCIALG_4:def 5 :
theorem Th5: :: BCIALG_4:5
theorem :: BCIALG_4:6
theorem Th7: :: BCIALG_4:7
theorem Th8: :: BCIALG_4:8
theorem Th9: :: BCIALG_4:9
theorem Th10: :: BCIALG_4:10
theorem Th11: :: BCIALG_4:11
theorem Th12: :: BCIALG_4:12
theorem Th13: :: BCIALG_4:13
theorem :: BCIALG_4:14
theorem :: BCIALG_4:15
theorem :: BCIALG_4:16
Lm4:
for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is commutative
Lm5:
for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is associative
theorem Th17: :: BCIALG_4:17
theorem :: BCIALG_4:18
theorem Th19: :: BCIALG_4:19
definition
let X be
BCI-Algebra_with_Condition(S);
func power X -> Function of
[:the carrier of X,NAT :],the
carrier of
X means :
Def6:
:: BCIALG_4:def 6
for
h being
Element of
X holds
(
it . h,
0 = 0. X & ( for
n being
Element of
NAT holds
it . h,
(n + 1) = (it . h,n) * h ) );
existence
ex b1 being Function of [:the carrier of X,NAT :],the carrier of X st
for h being Element of X holds
( b1 . h,0 = 0. X & ( for n being Element of NAT holds b1 . h,(n + 1) = (b1 . h,n) * h ) )
uniqueness
for b1, b2 being Function of [:the carrier of X,NAT :],the carrier of X st ( for h being Element of X holds
( b1 . h,0 = 0. X & ( for n being Element of NAT holds b1 . h,(n + 1) = (b1 . h,n) * h ) ) ) & ( for h being Element of X holds
( b2 . h,0 = 0. X & ( for n being Element of NAT holds b2 . h,(n + 1) = (b2 . h,n) * h ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines power BCIALG_4:def 6 :
:: deftheorem defines |^ BCIALG_4:def 7 :
theorem :: BCIALG_4:20
theorem :: BCIALG_4:21
theorem Th22: :: BCIALG_4:22
theorem Th23: :: BCIALG_4:23
theorem :: BCIALG_4:24
theorem Th25: :: BCIALG_4:25
Lm6:
for n being Element of NAT
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X
theorem :: BCIALG_4:26
theorem :: BCIALG_4:27
Lm7:
for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds x,a to_power 0 = x \ (a |^ 0 )
theorem :: BCIALG_4:28
:: deftheorem defines Product_S BCIALG_4:def 8 :
theorem :: BCIALG_4:29
theorem :: BCIALG_4:30
theorem :: BCIALG_4:31
theorem :: BCIALG_4:32
theorem Th33: :: BCIALG_4:33
theorem Th34: :: BCIALG_4:34
theorem :: BCIALG_4:35
theorem :: BCIALG_4:36
theorem :: BCIALG_4:37
theorem Th38: :: BCIALG_4:38
theorem :: BCIALG_4:39
theorem :: BCIALG_4:40
theorem :: BCIALG_4:41
:: deftheorem Def9 defines commutative BCIALG_4:def 9 :
theorem :: BCIALG_4:42
theorem :: BCIALG_4:43
:: deftheorem defines Initial_section BCIALG_4:def 10 :
theorem :: BCIALG_4:44
:: deftheorem Def11 defines positive-implicative BCIALG_4:def 11 :
theorem Th45: :: BCIALG_4:45
theorem Th46: :: BCIALG_4:46
theorem Th47: :: BCIALG_4:47
theorem Th48: :: BCIALG_4:48
theorem Th49: :: BCIALG_4:49
:: deftheorem Def12 defines being_SB-1 BCIALG_4:def 12 :
:: deftheorem Def13 defines being_SB-2 BCIALG_4:def 13 :
:: deftheorem Def14 defines being_SB-4 BCIALG_4:def 14 :
Lm8:
( BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )
theorem :: BCIALG_4:50
:: deftheorem Def15 defines implicative BCIALG_4:def 15 :
theorem Th51: :: BCIALG_4:51
theorem :: BCIALG_4:52