:: BCIALG_1 semantic presentation
begin
definition
attrc1 is strict ;
struct BCIStr -> 1-sorted ;
aggrBCIStr(# carrier, InternalDiff #) -> BCIStr ;
sel InternalDiff c1 -> BinOp of the carrier of c1;
end;
registration
cluster non empty strict for BCIStr ;
existence
ex b1 being BCIStr st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set m = the BinOp of the non empty set ;
take BCIStr(# the non empty set , the BinOp of the non empty set #) ; ::_thesis: ( not BCIStr(# the non empty set , the BinOp of the non empty set #) is empty & BCIStr(# the non empty set , the BinOp of the non empty set #) is strict )
thus not the carrier of BCIStr(# the non empty set , the BinOp of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: BCIStr(# the non empty set , the BinOp of the non empty set #) is strict
thus BCIStr(# the non empty set , the BinOp of the non empty set #) is strict ; ::_thesis: verum
end;
end;
definition
let A be BCIStr ;
let x, y be Element of A;
funcx \ y -> Element of A equals :: BCIALG_1:def 1
the InternalDiff of A . (x,y);
coherence
the InternalDiff of A . (x,y) is Element of A ;
end;
:: deftheorem defines \ BCIALG_1:def_1_:_
for A being BCIStr
for x, y being Element of A holds x \ y = the InternalDiff of A . (x,y);
definition
attrc1 is strict ;
struct BCIStr_0 -> BCIStr , ZeroStr ;
aggrBCIStr_0(# carrier, InternalDiff, ZeroF #) -> BCIStr_0 ;
end;
registration
cluster non empty strict for BCIStr_0 ;
existence
ex b1 being BCIStr_0 st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set m = the BinOp of the non empty set ;
set u = the Element of the non empty set ;
take BCIStr_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) ; ::_thesis: ( not BCIStr_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty & BCIStr_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict )
thus not the carrier of BCIStr_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: BCIStr_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict
thus BCIStr_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict ; ::_thesis: verum
end;
end;
definition
let IT be non empty BCIStr_0 ;
let x be Element of IT;
funcx ` -> Element of IT equals :: BCIALG_1:def 2
(0. IT) \ x;
coherence
(0. IT) \ x is Element of IT ;
end;
:: deftheorem defines ` BCIALG_1:def_2_:_
for IT being non empty BCIStr_0
for x being Element of IT holds x ` = (0. IT) \ x;
definition
let IT be non empty BCIStr_0 ;
attrIT is being_B means :Def3: :: BCIALG_1:def 3
for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT;
attrIT is being_C means :Def4: :: BCIALG_1:def 4
for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT;
attrIT is being_I means :Def5: :: BCIALG_1:def 5
for x being Element of IT holds x \ x = 0. IT;
attrIT is being_K means :Def6: :: BCIALG_1:def 6
for x, y being Element of IT holds (x \ y) \ x = 0. IT;
attrIT is being_BCI-4 means :Def7: :: BCIALG_1:def 7
for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y;
attrIT is being_BCK-5 means :Def8: :: BCIALG_1:def 8
for x being Element of IT holds x ` = 0. IT;
end;
:: deftheorem Def3 defines being_B BCIALG_1:def_3_:_
for IT being non empty BCIStr_0 holds
( IT is being_B iff for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT );
:: deftheorem Def4 defines being_C BCIALG_1:def_4_:_
for IT being non empty BCIStr_0 holds
( IT is being_C iff for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT );
:: deftheorem Def5 defines being_I BCIALG_1:def_5_:_
for IT being non empty BCIStr_0 holds
( IT is being_I iff for x being Element of IT holds x \ x = 0. IT );
:: deftheorem Def6 defines being_K BCIALG_1:def_6_:_
for IT being non empty BCIStr_0 holds
( IT is being_K iff for x, y being Element of IT holds (x \ y) \ x = 0. IT );
:: deftheorem Def7 defines being_BCI-4 BCIALG_1:def_7_:_
for IT being non empty BCIStr_0 holds
( IT is being_BCI-4 iff for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y );
:: deftheorem Def8 defines being_BCK-5 BCIALG_1:def_8_:_
for IT being non empty BCIStr_0 holds
( IT is being_BCK-5 iff for x being Element of IT holds x ` = 0. IT );
definition
func BCI-EXAMPLE -> BCIStr_0 equals :: BCIALG_1:def 9
BCIStr_0(# 1,op2,op0 #);
coherence
BCIStr_0(# 1,op2,op0 #) is BCIStr_0 ;
end;
:: deftheorem defines BCI-EXAMPLE BCIALG_1:def_9_:_
BCI-EXAMPLE = BCIStr_0(# 1,op2,op0 #);
registration
cluster BCI-EXAMPLE -> 1 -element strict ;
coherence
( BCI-EXAMPLE is strict & BCI-EXAMPLE is 1 -element ) by CARD_1:49, STRUCT_0:def_19;
end;
registration
cluster BCI-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5 ;
coherence
( BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )
proof
thus BCI-EXAMPLE is being_B ::_thesis: ( BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )
proof
let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_3 ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI-EXAMPLE
thus ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI-EXAMPLE is being_C ::_thesis: ( BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )
proof
let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_4 ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI-EXAMPLE
thus ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI-EXAMPLE is being_I ::_thesis: ( BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )
proof
let x be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_5 ::_thesis: x \ x = 0. BCI-EXAMPLE
thus x \ x = 0. BCI-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI-EXAMPLE is being_BCI-4 ::_thesis: BCI-EXAMPLE is being_BCK-5
proof
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_7 ::_thesis: ( x \ y = 0. BCI-EXAMPLE & y \ x = 0. BCI-EXAMPLE implies x = y )
thus ( x \ y = 0. BCI-EXAMPLE & y \ x = 0. BCI-EXAMPLE implies x = y ) by STRUCT_0:def_10; ::_thesis: verum
end;
for x being Element of BCI-EXAMPLE holds x ` = 0. BCI-EXAMPLE by STRUCT_0:def_10;
hence BCI-EXAMPLE is being_BCK-5 by Def8; ::_thesis: verum
end;
end;
registration
cluster non empty strict being_B being_C being_I being_BCI-4 being_BCK-5 for BCIStr_0 ;
existence
ex b1 being non empty BCIStr_0 st
( b1 is strict & b1 is being_B & b1 is being_C & b1 is being_I & b1 is being_BCI-4 & b1 is being_BCK-5 )
proof
take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is strict & BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )
thus ( BCI-EXAMPLE is strict & BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) ; ::_thesis: verum
end;
end;
definition
mode BCI-algebra is non empty being_B being_C being_I being_BCI-4 BCIStr_0 ;
end;
definition
mode BCK-algebra is being_BCK-5 BCI-algebra;
end;
definition
let X be BCI-algebra;
mode SubAlgebra of X -> BCI-algebra means :Def10: :: BCIALG_1:def 10
( 0. it = 0. X & the carrier of it c= the carrier of X & the InternalDiff of it = the InternalDiff of X || the carrier of it );
existence
ex b1 being BCI-algebra st
( 0. b1 = 0. X & the carrier of b1 c= the carrier of X & the InternalDiff of b1 = the InternalDiff of X || the carrier of b1 )
proof
take X ; ::_thesis: ( 0. X = 0. X & the carrier of X c= the carrier of X & the InternalDiff of X = the InternalDiff of X || the carrier of X )
dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def_1;
hence ( 0. X = 0. X & the carrier of X c= the carrier of X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) by RELAT_1:68; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines SubAlgebra BCIALG_1:def_10_:_
for X, b2 being BCI-algebra holds
( b2 is SubAlgebra of X iff ( 0. b2 = 0. X & the carrier of b2 c= the carrier of X & the InternalDiff of b2 = the InternalDiff of X || the carrier of b2 ) );
theorem Th1: :: BCIALG_1:1
for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is BCI-algebra iff ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) )
thus ( X is BCI-algebra implies ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ) ::_thesis: ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) implies X is BCI-algebra )
proof
assume A1: X is BCI-algebra ; ::_thesis: ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) )
now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_
(_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_&_x_\_x_=_0._X_&_(_x_\_y_=_0._X_&_y_\_x_=_0._X_implies_x_=_y_)_)
let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & x \ x = 0. X & ( x \ y = 0. X & y \ x = 0. X implies x = y ) )
A2: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A1, Def3;
A3: for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ y
( ((x \ y) \ z) \ ((x \ z) \ y) = 0. X & ((x \ z) \ y) \ ((x \ y) \ z) = 0. X ) by A1, Def4;
hence (x \ y) \ z = (x \ z) \ y by A1, Def7; ::_thesis: verum
end;
then (x \ (x \ y)) \ y = (x \ y) \ (x \ y) ;
hence ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & x \ x = 0. X & ( x \ y = 0. X & y \ x = 0. X implies x = y ) ) by A1, A2, A3, Def5, Def7; ::_thesis: verum
end;
hence ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) by A1; ::_thesis: verum
end;
assume that
A4: X is being_I and
A5: X is being_BCI-4 and
A6: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ; ::_thesis: X is BCI-algebra
A7: for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X
proof
let x be Element of X; ::_thesis: ( x \ (0. X) = 0. X implies x = 0. X )
assume A8: x \ (0. X) = 0. X ; ::_thesis: x = 0. X
then x ` = (x \ (x \ x)) \ x by A4, Def5
.= 0. X by A6 ;
hence x = 0. X by A5, A8, Def7; ::_thesis: verum
end;
A9: for x being Element of X holds x \ (0. X) = x
proof
let x be Element of X; ::_thesis: x \ (0. X) = x
(x \ (x \ (0. X))) \ (0. X) = 0. X by A6;
then A10: x \ (x \ (0. X)) = 0. X by A7;
0. X = (x \ (x \ x)) \ x by A6
.= (x \ (0. X)) \ x by A4, Def5 ;
hence x \ (0. X) = x by A5, A10, Def7; ::_thesis: verum
end;
A11: for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
proof
let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X & y \ z = 0. X implies x \ z = 0. X )
assume that
A12: x \ y = 0. X and
A13: y \ z = 0. X ; ::_thesis: x \ z = 0. X
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A6;
then (x \ z) \ (x \ y) = 0. X by A9, A13;
hence x \ z = 0. X by A9, A12; ::_thesis: verum
end;
A14: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
(((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ z) = 0. X by A6;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (0. X) = 0. X by A6;
then A15: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A7;
((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by A6;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A11, A15; ::_thesis: verum
end;
A16: for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
proof
let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X implies ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) )
assume A17: x \ y = 0. X ; ::_thesis: ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
( ((z \ y) \ (z \ x)) \ (x \ y) = 0. X & ((x \ z) \ (x \ y)) \ (y \ z) = 0. X ) by A6;
hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A9, A17; ::_thesis: verum
end;
for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A6;
then ((x \ y) \ (z \ y)) \ ((x \ y) \ ((x \ y) \ (x \ z))) = 0. X by A16;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (((x \ y) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A16;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (0. X) = 0. X by A6;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A7; ::_thesis: verum
end;
hence X is BCI-algebra by A4, A5, A14, Def3, Def4; ::_thesis: verum
end;
definition
let IT be non empty BCIStr_0 ;
let x, y be Element of IT;
predx <= y means :Def11: :: BCIALG_1:def 11
x \ y = 0. IT;
end;
:: deftheorem Def11 defines <= BCIALG_1:def_11_:_
for IT being non empty BCIStr_0
for x, y being Element of IT holds
( x <= y iff x \ y = 0. IT );
Lm1: for X being BCI-algebra
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X
proof
let X be BCI-algebra; ::_thesis: for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X
let x be Element of X; ::_thesis: ( x \ (0. X) = 0. X implies x = 0. X )
assume A1: x \ (0. X) = 0. X ; ::_thesis: x = 0. X
then x ` = (x \ (x \ x)) \ x by Def5
.= 0. X by Th1 ;
hence x = 0. X by A1, Def7; ::_thesis: verum
end;
theorem Th2: :: BCIALG_1:2
for X being BCI-algebra
for x being Element of X holds x \ (0. X) = x
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds x \ (0. X) = x
let x be Element of X; ::_thesis: x \ (0. X) = x
(x \ (x \ (0. X))) \ (0. X) = 0. X by Th1;
then A1: x \ (x \ (0. X)) = 0. X by Lm1;
0. X = (x \ (x \ x)) \ x by Th1
.= (x \ (0. X)) \ x by Def5 ;
hence x \ (0. X) = x by A1, Def7; ::_thesis: verum
end;
theorem Th3: :: BCIALG_1:3
for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X & y \ z = 0. X implies x \ z = 0. X )
assume that
A1: x \ y = 0. X and
A2: y \ z = 0. X ; ::_thesis: x \ z = 0. X
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by Th1;
then (x \ z) \ (x \ y) = 0. X by A2, Th2;
hence x \ z = 0. X by A1, Th2; ::_thesis: verum
end;
theorem Th4: :: BCIALG_1:4
for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X implies ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) )
assume A1: x \ y = 0. X ; ::_thesis: ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
( ((z \ y) \ (z \ x)) \ (x \ y) = 0. X & ((x \ z) \ (x \ y)) \ (y \ z) = 0. X ) by Th1;
hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A1, Th2; ::_thesis: verum
end;
theorem :: BCIALG_1:5
for X being BCI-algebra
for x, y, z being Element of X st x <= y holds
( x \ z <= y \ z & z \ y <= z \ x )
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X st x <= y holds
( x \ z <= y \ z & z \ y <= z \ x )
let x, y, z be Element of X; ::_thesis: ( x <= y implies ( x \ z <= y \ z & z \ y <= z \ x ) )
assume x <= y ; ::_thesis: ( x \ z <= y \ z & z \ y <= z \ x )
then x \ y = 0. X by Def11;
then ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by Th4;
hence ( x \ z <= y \ z & z \ y <= z \ x ) by Def11; ::_thesis: verum
end;
theorem :: BCIALG_1:6
for X being BCI-algebra
for x, y being Element of X st x \ y = 0. X holds
(y \ x) ` = 0. X
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X st x \ y = 0. X holds
(y \ x) ` = 0. X
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies (y \ x) ` = 0. X )
assume x \ y = 0. X ; ::_thesis: (y \ x) ` = 0. X
then (x \ x) \ (y \ x) = 0. X by Th4;
hence (y \ x) ` = 0. X by Def5; ::_thesis: verum
end;
theorem Th7: :: BCIALG_1:7
for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ y
(x \ (x \ z)) \ z = 0. X by Th1;
then A1: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by Th4;
(x \ (x \ y)) \ y = 0. X by Th1;
then A2: ((x \ z) \ y) \ ((x \ z) \ (x \ (x \ y))) = 0. X by Th4;
((x \ z) \ (x \ (x \ y))) \ ((x \ y) \ z) = 0. X by Th1;
then A3: ((x \ z) \ y) \ ((x \ y) \ z) = 0. X by A2, Th3;
((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by Th1;
then ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A1, Th3;
hence (x \ y) \ z = (x \ z) \ y by A3, Def7; ::_thesis: verum
end;
theorem Th8: :: BCIALG_1:8
for X being BCI-algebra
for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y
let x, y be Element of X; ::_thesis: x \ (x \ (x \ y)) = x \ y
((x \ y) \ (x \ (x \ (x \ y)))) \ ((x \ (x \ y)) \ y) = 0. X by Th1;
then ((x \ y) \ (x \ (x \ (x \ y)))) \ (0. X) = 0. X by Th1;
then A1: (x \ y) \ (x \ (x \ (x \ y))) = 0. X by Th2;
(x \ (x \ (x \ y))) \ (x \ y) = 0. X by Th1;
hence x \ (x \ (x \ y)) = x \ y by A1, Def7; ::_thesis: verum
end;
theorem Th9: :: BCIALG_1:9
for X being BCI-algebra
for x, y being Element of X holds (x \ y) ` = (x `) \ (y `)
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds (x \ y) ` = (x `) \ (y `)
let x, y be Element of X; ::_thesis: (x \ y) ` = (x `) \ (y `)
(x `) \ (y `) = (((x \ y) \ (x \ y)) \ x) \ (y `) by Def5
.= (((x \ y) \ x) \ (x \ y)) \ (y `) by Th7
.= (((x \ x) \ y) \ (x \ y)) \ (y `) by Th7
.= ((y `) \ (x \ y)) \ (y `) by Def5
.= ((y `) \ (y `)) \ (x \ y) by Th7 ;
hence (x \ y) ` = (x `) \ (y `) by Def5; ::_thesis: verum
end;
theorem Th10: :: BCIALG_1:10
for X being BCI-algebra
for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X
let x, y be Element of X; ::_thesis: ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X
((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) \ (y \ x) by Th7
.= ((x \ (x \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (y \ x) by Th7
.= ((x \ (y \ (y \ x))) \ (x \ y)) \ (y \ x) by Th8
.= ((x \ (y \ (y \ x))) \ (x \ y)) \ (y \ (y \ (y \ x))) by Th8 ;
hence ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by Th1; ::_thesis: verum
end;
theorem :: BCIALG_1:11
for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is BCI-algebra iff ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )
thus ( X is BCI-algebra implies ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) ) by Th1, Th2; ::_thesis: ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra )
thus ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra ) ::_thesis: verum
proof
assume that
A1: X is being_BCI-4 and
A2: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ; ::_thesis: X is BCI-algebra
A3: X is being_I
proof
let x be Element of X; :: according to BCIALG_1:def_5 ::_thesis: x \ x = 0. X
x \ x = (x \ x) \ (0. X) by A2;
then x \ x = ((x \ (0. X)) \ x) \ (0. X) by A2;
then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) by A2;
then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) by A2;
hence x \ x = 0. X by A2; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_
(_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_)
let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )
((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) = 0. X by A2;
then (x \ (x \ y)) \ (y \ (0. X)) = 0. X by A2;
hence ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) by A2; ::_thesis: verum
end;
hence X is BCI-algebra by A1, A3, Th1; ::_thesis: verum
end;
end;
theorem :: BCIALG_1:12
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds
X is BCK-algebra
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ; ::_thesis: X is BCK-algebra
for z being Element of X holds z ` = 0. X
proof
let z be Element of X; ::_thesis: z ` = 0. X
(z `) ` = z \ (z \ (0. X)) by A1;
then (z `) ` = z \ z by Th2;
then ((z `) `) \ z = z ` by Def5;
hence z ` = 0. X by Th1; ::_thesis: verum
end;
hence X is BCK-algebra by Def8; ::_thesis: verum
end;
theorem :: BCIALG_1:13
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) holds
X is BCK-algebra
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ; ::_thesis: X is BCK-algebra
for z being Element of X holds z ` = 0. X
proof
let z be Element of X; ::_thesis: z ` = 0. X
(z `) \ ((z `) \ z) = (z `) \ (z `) by A1;
then (z `) \ ((z `) \ z) = 0. X by Def5;
hence z ` = 0. X by Th1; ::_thesis: verum
end;
hence X is BCK-algebra by Def8; ::_thesis: verum
end;
theorem :: BCIALG_1:14
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) holds
X is BCK-algebra
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ; ::_thesis: X is BCK-algebra
for z being Element of X holds z ` = 0. X
proof
let z be Element of X; ::_thesis: z ` = 0. X
(z \ (0. X)) ` = 0. X by A1;
hence z ` = 0. X by Th2; ::_thesis: verum
end;
hence X is BCK-algebra by Def8; ::_thesis: verum
end;
theorem :: BCIALG_1:15
for X being BCI-algebra st ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds
X is BCK-algebra
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ; ::_thesis: X is BCK-algebra
for s being Element of X holds s ` = 0. X
proof
let s be Element of X; ::_thesis: s ` = 0. X
(s `) \ s = (s `) \ (s \ s) by A1;
then (s `) \ s = (s `) \ (0. X) by Def5;
then (s `) \ ((s `) \ s) = (s `) \ (s `) by Th2;
then (s `) \ ((s `) \ s) = 0. X by Def5;
hence s ` = 0. X by Th1; ::_thesis: verum
end;
hence X is BCK-algebra by Def8; ::_thesis: verum
end;
theorem :: BCIALG_1:16
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds
X is BCK-algebra
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ; ::_thesis: X is BCK-algebra
for s being Element of X holds s ` = 0. X
proof
let s be Element of X; ::_thesis: s ` = 0. X
(s `) \ (s \ (0. X)) = s ` by A1;
then (s `) \ ((s `) \ s) = (s `) \ (s `) by Th2;
then (s `) \ ((s `) \ s) = 0. X by Def5;
hence s ` = 0. X by Th1; ::_thesis: verum
end;
hence X is BCK-algebra by Def8; ::_thesis: verum
end;
theorem :: BCIALG_1:17
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds
X is BCK-algebra
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ; ::_thesis: X is BCK-algebra
for s being Element of X holds s ` = 0. X
proof
let s be Element of X; ::_thesis: s ` = 0. X
(s `) \ ((s `) \ (s \ (0. X))) = 0. X by A1;
then ((s `) \ ((s `) \ s)) \ s = s ` by Th2;
hence s ` = 0. X by Th1; ::_thesis: verum
end;
hence X is BCK-algebra by Def8; ::_thesis: verum
end;
theorem :: BCIALG_1:18
for X being BCI-algebra holds
( X is being_K iff X is BCK-algebra )
proof
let X be BCI-algebra; ::_thesis: ( X is being_K iff X is BCK-algebra )
thus ( X is being_K implies X is BCK-algebra ) ::_thesis: ( X is BCK-algebra implies X is being_K )
proof
assume A1: X is being_K ; ::_thesis: X is BCK-algebra
now__::_thesis:_for_s_being_Element_of_X_holds_s_`_=_0._X
let s be Element of X; ::_thesis: s ` = 0. X
(s `) \ (0. X) = 0. X by A1, Def6;
hence s ` = 0. X by Th2; ::_thesis: verum
end;
hence X is BCK-algebra by Def8; ::_thesis: verum
end;
assume A2: X is BCK-algebra ; ::_thesis: X is being_K
let x, y be Element of X; :: according to BCIALG_1:def_6 ::_thesis: (x \ y) \ x = 0. X
y ` = 0. X by A2, Def8;
then (x \ y) \ (x \ (0. X)) = 0. X by Th4;
hence (x \ y) \ x = 0. X by Th2; ::_thesis: verum
end;
definition
let X be BCI-algebra;
func BCK-part X -> non empty Subset of X equals :: BCIALG_1:def 12
{ x where x is Element of X : 0. X <= x } ;
coherence
{ x where x is Element of X : 0. X <= x } is non empty Subset of X
proof
set Y = { x where x is Element of X : 0. X <= x } ;
A1: now__::_thesis:_for_y_being_set_st_y_in__{__x_where_x_is_Element_of_X_:_0._X_<=_x__}__holds_
y_in_the_carrier_of_X
let y be set ; ::_thesis: ( y in { x where x is Element of X : 0. X <= x } implies y in the carrier of X )
assume y in { x where x is Element of X : 0. X <= x } ; ::_thesis: y in the carrier of X
then ex x being Element of X st
( y = x & 0. X <= x ) ;
hence y in the carrier of X ; ::_thesis: verum
end;
(0. X) ` = 0. X by Def5;
then 0. X <= 0. X by Def11;
then 0. X in { x where x is Element of X : 0. X <= x } ;
hence { x where x is Element of X : 0. X <= x } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines BCK-part BCIALG_1:def_12_:_
for X being BCI-algebra holds BCK-part X = { x where x is Element of X : 0. X <= x } ;
theorem Th19: :: BCIALG_1:19
for X being BCI-algebra holds 0. X in BCK-part X
proof
let X be BCI-algebra; ::_thesis: 0. X in BCK-part X
(0. X) ` = 0. X by Def5;
then 0. X <= 0. X by Def11;
hence 0. X in BCK-part X ; ::_thesis: verum
end;
theorem :: BCIALG_1:20
for X being BCI-algebra
for x, y being Element of BCK-part X holds x \ y in BCK-part X
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of BCK-part X holds x \ y in BCK-part X
let x, y be Element of BCK-part X; ::_thesis: x \ y in BCK-part X
x in { x1 where x1 is Element of X : 0. X <= x1 } ;
then A1: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
y in { y1 where y1 is Element of X : 0. X <= y1 } ;
then A2: ex y1 being Element of X st
( y = y1 & 0. X <= y1 ) ;
(x \ y) ` = (x `) \ (y `) by Th9;
then (x \ y) ` = (y `) ` by A1, Def11;
then (x \ y) ` = (0. X) ` by A2, Def11;
then (x \ y) ` = 0. X by Def5;
then 0. X <= x \ y by Def11;
hence x \ y in BCK-part X ; ::_thesis: verum
end;
theorem :: BCIALG_1:21
for X being BCI-algebra
for x being Element of X
for y being Element of BCK-part X holds x \ y <= x
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for y being Element of BCK-part X holds x \ y <= x
let x be Element of X; ::_thesis: for y being Element of BCK-part X holds x \ y <= x
let y be Element of BCK-part X; ::_thesis: x \ y <= x
y in { y1 where y1 is Element of X : 0. X <= y1 } ;
then ex y1 being Element of X st
( y = y1 & 0. X <= y1 ) ;
then y ` = 0. X by Def11;
then (x \ x) \ y = 0. X by Def5;
then (x \ y) \ x = 0. X by Th7;
hence x \ y <= x by Def11; ::_thesis: verum
end;
theorem Th22: :: BCIALG_1:22
for X being BCI-algebra holds X is SubAlgebra of X
proof
let X be BCI-algebra; ::_thesis: X is SubAlgebra of X
dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def_1;
then ( 0. X = 0. X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) by RELAT_1:68;
hence X is SubAlgebra of X by Def10; ::_thesis: verum
end;
definition
let X be BCI-algebra;
let IT be SubAlgebra of X;
attrIT is proper means :Def13: :: BCIALG_1:def 13
IT <> X;
end;
:: deftheorem Def13 defines proper BCIALG_1:def_13_:_
for X being BCI-algebra
for IT being SubAlgebra of X holds
( IT is proper iff IT <> X );
registration
let X be BCI-algebra;
cluster non empty being_B being_C being_I being_BCI-4 non proper for SubAlgebra of X;
existence
not for b1 being SubAlgebra of X holds b1 is proper
proof
take X ; ::_thesis: ( X is SubAlgebra of X & not X is proper )
X is SubAlgebra of X by Th22;
hence ( X is SubAlgebra of X & not X is proper ) by Def13; ::_thesis: verum
end;
end;
definition
let X be BCI-algebra;
let IT be Element of X;
attrIT is atom means :Def14: :: BCIALG_1:def 14
for z being Element of X st z \ IT = 0. X holds
z = IT;
end;
:: deftheorem Def14 defines atom BCIALG_1:def_14_:_
for X being BCI-algebra
for IT being Element of X holds
( IT is atom iff for z being Element of X st z \ IT = 0. X holds
z = IT );
definition
let X be BCI-algebra;
func AtomSet X -> non empty Subset of X equals :: BCIALG_1:def 15
{ x where x is Element of X : x is atom } ;
coherence
{ x where x is Element of X : x is atom } is non empty Subset of X
proof
set Y = { x where x is Element of X : x is atom } ;
A1: now__::_thesis:_for_y_being_set_st_y_in__{__x_where_x_is_Element_of_X_:_x_is_atom__}__holds_
y_in_the_carrier_of_X
let y be set ; ::_thesis: ( y in { x where x is Element of X : x is atom } implies y in the carrier of X )
assume y in { x where x is Element of X : x is atom } ; ::_thesis: y in the carrier of X
then ex x being Element of X st
( y = x & x is atom ) ;
hence y in the carrier of X ; ::_thesis: verum
end;
for z being Element of X st z \ (0. X) = 0. X holds
z = 0. X by Th2;
then 0. X is atom by Def14;
then 0. X in { x where x is Element of X : x is atom } ;
hence { x where x is Element of X : x is atom } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines AtomSet BCIALG_1:def_15_:_
for X being BCI-algebra holds AtomSet X = { x where x is Element of X : x is atom } ;
theorem Th23: :: BCIALG_1:23
for X being BCI-algebra holds 0. X in AtomSet X
proof
let X be BCI-algebra; ::_thesis: 0. X in AtomSet X
for z being Element of X st z \ (0. X) = 0. X holds
z = 0. X by Th2;
then 0. X is atom by Def14;
hence 0. X in AtomSet X ; ::_thesis: verum
end;
theorem Th24: :: BCIALG_1:24
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )
thus ( x in AtomSet X implies for z being Element of X holds z \ (z \ x) = x ) ::_thesis: ( ( for z being Element of X holds z \ (z \ x) = x ) implies x in AtomSet X )
proof
assume x in AtomSet X ; ::_thesis: for z being Element of X holds z \ (z \ x) = x
then A1: ex x1 being Element of X st
( x = x1 & x1 is atom ) ;
let z be Element of X; ::_thesis: z \ (z \ x) = x
(z \ (z \ x)) \ x = 0. X by Th1;
hence z \ (z \ x) = x by A1, Def14; ::_thesis: verum
end;
assume A2: for z being Element of X holds z \ (z \ x) = x ; ::_thesis: x in AtomSet X
now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_
z_=_x
let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x )
assume z \ x = 0. X ; ::_thesis: z = x
then z \ (0. X) = x by A2;
hence z = x by Th2; ::_thesis: verum
end;
then x is atom by Def14;
hence x in AtomSet X ; ::_thesis: verum
end;
theorem :: BCIALG_1:25
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u )
thus ( x in AtomSet X implies for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ) ::_thesis: ( ( for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ) implies x in AtomSet X )
proof
assume x in AtomSet X ; ::_thesis: for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u
then A1: ex x1 being Element of X st
( x = x1 & x1 is atom ) ;
let u, z be Element of X; ::_thesis: (z \ u) \ (z \ x) = x \ u
(z \ (z \ x)) \ x = 0. X by Th1;
then z \ (z \ x) = x by A1, Def14;
hence (z \ u) \ (z \ x) = x \ u by Th7; ::_thesis: verum
end;
assume A2: for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ; ::_thesis: x in AtomSet X
now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_
z_=_x
let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x )
assume z \ x = 0. X ; ::_thesis: z = x
then (z \ (0. X)) \ (0. X) = x \ (0. X) by A2;
then (z \ (0. X)) \ (0. X) = x by Th2;
then z \ (0. X) = x by Th2;
hence z = x by Th2; ::_thesis: verum
end;
then x is atom by Def14;
hence x in AtomSet X ; ::_thesis: verum
end;
theorem :: BCIALG_1:26
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) )
thus ( x in AtomSet X implies for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ) ::_thesis: ( ( for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ) implies x in AtomSet X )
proof
assume x in AtomSet X ; ::_thesis: for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x)
then A1: ex x1 being Element of X st
( x = x1 & x1 is atom ) ;
let y, z be Element of X; ::_thesis: x \ (z \ y) <= y \ (z \ x)
(z \ (z \ x)) \ x = 0. X by Th1;
then (x \ (z \ y)) \ (y \ (z \ x)) = ((z \ (z \ x)) \ (z \ y)) \ (y \ (z \ x)) by A1, Def14;
then (x \ (z \ y)) \ (y \ (z \ x)) = ((z \ (z \ y)) \ (z \ x)) \ (y \ (z \ x)) by Th7;
then (x \ (z \ y)) \ (y \ (z \ x)) = (((z \ (z \ y)) \ (z \ x)) \ (y \ (z \ x))) \ (0. X) by Th2;
then (x \ (z \ y)) \ (y \ (z \ x)) = (((z \ (z \ y)) \ (z \ x)) \ (y \ (z \ x))) \ ((z \ (z \ y)) \ y) by Th1;
then (x \ (z \ y)) \ (y \ (z \ x)) = 0. X by Def3;
hence x \ (z \ y) <= y \ (z \ x) by Def11; ::_thesis: verum
end;
assume A2: for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ; ::_thesis: x in AtomSet X
now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_
z_=_x
let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x )
assume A3: z \ x = 0. X ; ::_thesis: z = x
x \ (z \ (0. X)) <= (z \ x) ` by A2;
then (x \ (z \ (0. X))) \ ((0. X) `) = 0. X by A3, Def11;
then (x \ (z \ (0. X))) \ (0. X) = 0. X by Th2;
then x \ (z \ (0. X)) = 0. X by Th2;
then x \ z = 0. X by Th2;
hence z = x by A3, Def7; ::_thesis: verum
end;
then x is atom by Def14;
hence x in AtomSet X ; ::_thesis: verum
end;
theorem :: BCIALG_1:27
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) )
thus ( x in AtomSet X implies for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ) ::_thesis: ( ( for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ) implies x in AtomSet X )
proof
assume x in AtomSet X ; ::_thesis: for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x)
then A1: ex x1 being Element of X st
( x = x1 & x1 is atom ) ;
let y, z, u be Element of X; ::_thesis: (x \ u) \ (z \ y) <= (y \ u) \ (z \ x)
(z \ (z \ x)) \ x = 0. X by Th1;
then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = (((z \ (z \ x)) \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) by A1, Def14;
then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = (((z \ u) \ (z \ x)) \ (z \ y)) \ ((y \ u) \ (z \ x)) by Th7;
then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = (((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x)) by Th7
.= ((((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x))) \ (0. X) by Th2 ;
then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = ((((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x))) \ (((z \ u) \ (z \ y)) \ (y \ u)) by Th1;
then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = 0. X by Def3;
hence (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) by Def11; ::_thesis: verum
end;
assume A2: for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ; ::_thesis: x in AtomSet X
now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_
z_=_x
let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x )
assume A3: z \ x = 0. X ; ::_thesis: z = x
(x \ (0. X)) \ (z \ (0. X)) <= ((0. X) `) \ (z \ x) by A2;
then ((x \ (0. X)) \ (z \ (0. X))) \ (((0. X) `) \ (0. X)) = 0. X by A3, Def11;
then ((x \ (0. X)) \ (z \ (0. X))) \ ((0. X) `) = 0. X by Th2;
then ((x \ (0. X)) \ (z \ (0. X))) \ (0. X) = 0. X by Th2;
then (x \ (0. X)) \ (z \ (0. X)) = 0. X by Th2;
then (x \ (0. X)) \ z = 0. X by Th2;
then x \ z = 0. X by Th2;
hence z = x by A3, Def7; ::_thesis: verum
end;
then x is atom by Def14;
hence x in AtomSet X ; ::_thesis: verum
end;
theorem Th28: :: BCIALG_1:28
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z `) \ (x `) = x \ z )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z `) \ (x `) = x \ z )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds (z `) \ (x `) = x \ z )
thus ( x in AtomSet X implies for z being Element of X holds (z `) \ (x `) = x \ z ) ::_thesis: ( ( for z being Element of X holds (z `) \ (x `) = x \ z ) implies x in AtomSet X )
proof
assume x in AtomSet X ; ::_thesis: for z being Element of X holds (z `) \ (x `) = x \ z
then A1: ex x1 being Element of X st
( x = x1 & x1 is atom ) ;
let z be Element of X; ::_thesis: (z `) \ (x `) = x \ z
(z \ (z \ x)) \ x = 0. X by Th1;
then z \ (z \ x) = x by A1, Def14;
then x \ z = (z \ z) \ (z \ x) by Th7;
then x \ z = (z \ x) ` by Def5;
hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum
end;
assume A2: for z being Element of X holds (z `) \ (x `) = x \ z ; ::_thesis: x in AtomSet X
now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_
z_=_x
let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x )
assume A3: z \ x = 0. X ; ::_thesis: z = x
then (z \ x) ` = 0. X by Def5;
then (z `) \ (x `) = 0. X by Th9;
then x \ z = 0. X by A2;
hence z = x by A3, Def7; ::_thesis: verum
end;
then x is atom by Def14;
hence x in AtomSet X ; ::_thesis: verum
end;
theorem Th29: :: BCIALG_1:29
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff (x `) ` = x )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff (x `) ` = x )
let x be Element of X; ::_thesis: ( x in AtomSet X iff (x `) ` = x )
thus ( x in AtomSet X implies (x `) ` = x ) ::_thesis: ( (x `) ` = x implies x in AtomSet X )
proof
assume x in AtomSet X ; ::_thesis: (x `) ` = x
then ((0. X) `) \ (x `) = x \ (0. X) by Th28;
then ((0. X) `) \ (x `) = x by Th2;
hence (x `) ` = x by Def5; ::_thesis: verum
end;
assume A1: (x `) ` = x ; ::_thesis: x in AtomSet X
now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_
z_=_x
let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x )
assume A2: z \ x = 0. X ; ::_thesis: z = x
then ((z \ x) \ (x `)) \ (z \ (0. X)) = x \ z by A1, Th2;
then 0. X = x \ z by Def3;
hence z = x by A2, Def7; ::_thesis: verum
end;
then x is atom by Def14;
hence x in AtomSet X ; ::_thesis: verum
end;
theorem Th30: :: BCIALG_1:30
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )
A1: ( ( for z being Element of X holds (z `) \ (x `) = x \ z ) implies for z being Element of X holds (z \ x) ` = x \ z )
proof
assume A2: for z being Element of X holds (z `) \ (x `) = x \ z ; ::_thesis: for z being Element of X holds (z \ x) ` = x \ z
let z be Element of X; ::_thesis: (z \ x) ` = x \ z
(z `) \ (x `) = x \ z by A2;
hence (z \ x) ` = x \ z by Th9; ::_thesis: verum
end;
( ( for z being Element of X holds (z \ x) ` = x \ z ) implies for z being Element of X holds (z `) \ (x `) = x \ z )
proof
assume A3: for z being Element of X holds (z \ x) ` = x \ z ; ::_thesis: for z being Element of X holds (z `) \ (x `) = x \ z
let z be Element of X; ::_thesis: (z `) \ (x `) = x \ z
(z \ x) ` = x \ z by A3;
hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum
end;
hence ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z ) by A1, Th28; ::_thesis: verum
end;
theorem Th31: :: BCIALG_1:31
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z )
thus ( x in AtomSet X implies for z being Element of X holds ((x \ z) `) ` = x \ z ) ::_thesis: ( ( for z being Element of X holds ((x \ z) `) ` = x \ z ) implies x in AtomSet X )
proof
assume A1: x in AtomSet X ; ::_thesis: for z being Element of X holds ((x \ z) `) ` = x \ z
let z be Element of X; ::_thesis: ((x \ z) `) ` = x \ z
A2: (z \ (z \ x)) \ x = 0. X by Th1;
ex x1 being Element of X st
( x = x1 & x1 is atom ) by A1;
then z \ (z \ x) = x by A2, Def14;
then ((x \ z) `) ` = (((z \ z) \ (z \ x)) `) ` by Th7;
then ((x \ z) `) ` = (((z \ x) `) `) ` by Def5;
then ((x \ z) `) ` = (z \ x) ` by Th8;
hence ((x \ z) `) ` = x \ z by A1, Th30; ::_thesis: verum
end;
assume for z being Element of X holds ((x \ z) `) ` = x \ z ; ::_thesis: x in AtomSet X
then ((x \ (0. X)) `) ` = x \ (0. X) ;
then (x `) ` = x \ (0. X) by Th2;
then (x `) ` = x by Th2;
hence x in AtomSet X by Th29; ::_thesis: verum
end;
theorem :: BCIALG_1:32
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u )
let x be Element of X; ::_thesis: ( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u )
thus ( x in AtomSet X implies for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ) ::_thesis: ( ( for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ) implies x in AtomSet X )
proof
assume A1: x in AtomSet X ; ::_thesis: for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u
let z, u be Element of X; ::_thesis: z \ (z \ (x \ u)) = x \ u
x \ u = ((x \ u) `) ` by A1, Th31
.= ((z \ z) \ (x \ u)) ` by Def5
.= ((z \ (x \ u)) \ z) ` by Th7
.= ((z \ (x \ u)) `) \ (z `) by Th9 ;
then A2: (x \ u) \ (z \ (z \ (x \ u))) = 0. X by Th1;
(z \ (z \ (x \ u))) \ (x \ u) = 0. X by Th1;
hence z \ (z \ (x \ u)) = x \ u by A2, Def7; ::_thesis: verum
end;
assume for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ; ::_thesis: x in AtomSet X
then for u being Element of X holds ((x \ u) `) ` = x \ u ;
hence x in AtomSet X by Th31; ::_thesis: verum
end;
theorem Th33: :: BCIALG_1:33
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of X holds a \ x in AtomSet X
proof
let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X
for x being Element of X holds a \ x in AtomSet X
let a be Element of AtomSet X; ::_thesis: for x being Element of X holds a \ x in AtomSet X
let x be Element of X; ::_thesis: a \ x in AtomSet X
((a \ x) `) ` = a \ x by Th31;
hence a \ x in AtomSet X by Th29; ::_thesis: verum
end;
definition
let X be BCI-algebra;
let a, b be Element of AtomSet X;
:: original: \
redefine funca \ b -> Element of AtomSet X;
coherence
a \ b is Element of AtomSet X by Th33;
end;
theorem Th34: :: BCIALG_1:34
for X being BCI-algebra
for x being Element of X holds x ` in AtomSet X
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds x ` in AtomSet X
let x be Element of X; ::_thesis: x ` in AtomSet X
0. X in AtomSet X by Th23;
hence x ` in AtomSet X by Th33; ::_thesis: verum
end;
theorem Th35: :: BCIALG_1:35
for X being BCI-algebra
for x being Element of X ex a being Element of AtomSet X st a <= x
proof
let X be BCI-algebra; ::_thesis: for x being Element of X ex a being Element of AtomSet X st a <= x
let x be Element of X; ::_thesis: ex a being Element of AtomSet X st a <= x
take a = (x `) ` ; ::_thesis: ( a is Element of AtomSet X & a <= x )
a \ x = 0. X by Th1;
hence ( a is Element of AtomSet X & a <= x ) by Def11, Th34; ::_thesis: verum
end;
definition
let X be BCI-algebra;
attrX is generated_by_atom means :Def16: :: BCIALG_1:def 16
for x being Element of X ex a being Element of AtomSet X st a <= x;
end;
:: deftheorem Def16 defines generated_by_atom BCIALG_1:def_16_:_
for X being BCI-algebra holds
( X is generated_by_atom iff for x being Element of X ex a being Element of AtomSet X st a <= x );
definition
let X be BCI-algebra;
let a be Element of AtomSet X;
func BranchV a -> non empty Subset of X equals :: BCIALG_1:def 17
{ x where x is Element of X : a <= x } ;
coherence
{ x where x is Element of X : a <= x } is non empty Subset of X
proof
set Y = { x where x is Element of X : a <= x } ;
A1: now__::_thesis:_for_y_being_set_st_y_in__{__x_where_x_is_Element_of_X_:_a_<=_x__}__holds_
y_in_the_carrier_of_X
let y be set ; ::_thesis: ( y in { x where x is Element of X : a <= x } implies y in the carrier of X )
assume y in { x where x is Element of X : a <= x } ; ::_thesis: y in the carrier of X
then ex x being Element of X st
( y = x & a <= x ) ;
hence y in the carrier of X ; ::_thesis: verum
end;
a \ a = 0. X by Def5;
then a <= a by Def11;
then a in { x where x is Element of X : a <= x } ;
hence { x where x is Element of X : a <= x } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines BranchV BCIALG_1:def_17_:_
for X being BCI-algebra
for a being Element of AtomSet X holds BranchV a = { x where x is Element of X : a <= x } ;
theorem :: BCIALG_1:36
for X being BCI-algebra holds X is generated_by_atom
proof
let X be BCI-algebra; ::_thesis: X is generated_by_atom
for x being Element of X ex a being Element of AtomSet X st a <= x by Th35;
hence X is generated_by_atom by Def16; ::_thesis: verum
end;
theorem :: BCIALG_1:37
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV b holds a \ x = a \ b
proof
let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X
for x being Element of BranchV b holds a \ x = a \ b
let a, b be Element of AtomSet X; ::_thesis: for x being Element of BranchV b holds a \ x = a \ b
let x be Element of BranchV b; ::_thesis: a \ x = a \ b
a \ b in { x1 where x1 is Element of X : x1 is atom } ;
then A1: ex x1 being Element of X st
( a \ b = x1 & x1 is atom ) ;
x in { yy where yy is Element of X : b <= yy } ;
then A2: ex yy being Element of X st
( x = yy & b <= yy ) ;
(a \ x) \ (a \ b) = (a \ (a \ b)) \ x by Th7;
then (a \ x) \ (a \ b) = b \ x by Th24;
then (a \ x) \ (a \ b) = 0. X by A2, Def11;
hence a \ x = a \ b by A1, Def14; ::_thesis: verum
end;
theorem Th38: :: BCIALG_1:38
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BCK-part X holds a \ x = a
proof
let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X
for x being Element of BCK-part X holds a \ x = a
let a be Element of AtomSet X; ::_thesis: for x being Element of BCK-part X holds a \ x = a
let x be Element of BCK-part X; ::_thesis: a \ x = a
a \ (0. X) in { x1 where x1 is Element of X : x1 is atom } by Th33;
then A1: ex x1 being Element of X st
( a \ (0. X) = x1 & x1 is atom ) ;
(a \ x) \ (a \ (0. X)) = (a \ (a \ (0. X))) \ x by Th7;
then (a \ x) \ (a \ (0. X)) = (a \ a) \ x by Th2;
then A2: (a \ x) \ (a \ (0. X)) = x ` by Def5;
x in { x2 where x2 is Element of X : 0. X <= x2 } ;
then ex x2 being Element of X st
( x = x2 & 0. X <= x2 ) ;
then (a \ x) \ (a \ (0. X)) = 0. X by A2, Def11;
then a \ x = a \ (0. X) by A1, Def14;
hence a \ x = a by Th2; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X
for x being Element of BranchV a holds a \ x = 0. X
let a be Element of AtomSet X; ::_thesis: for x being Element of BranchV a holds a \ x = 0. X
let x be Element of BranchV a; ::_thesis: a \ x = 0. X
x in { x1 where x1 is Element of X : a <= x1 } ;
then ex x1 being Element of X st
( x = x1 & a <= x1 ) ;
hence a \ x = 0. X by Def11; ::_thesis: verum
end;
theorem Th39: :: BCIALG_1:39
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b holds x \ y in BranchV (a \ b)
proof
let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b holds x \ y in BranchV (a \ b)
let a, b be Element of AtomSet X; ::_thesis: for x being Element of BranchV a
for y being Element of BranchV b holds x \ y in BranchV (a \ b)
let x be Element of BranchV a; ::_thesis: for y being Element of BranchV b holds x \ y in BranchV (a \ b)
let y be Element of BranchV b; ::_thesis: x \ y in BranchV (a \ b)
(a \ b) \ (x \ y) = (((a \ b) `) `) \ (x \ y) by Th29;
then (a \ b) \ (x \ y) = ((x \ y) `) \ ((a \ b) `) by Th7;
then (a \ b) \ (x \ y) = ((x `) \ (y `)) \ ((a \ b) `) by Th9;
then (a \ b) \ (x \ y) = ((x `) \ ((a \ b) `)) \ (y `) by Th7;
then (a \ b) \ (x \ y) = ((((a \ b) `) `) \ x) \ (y `) by Th7;
then (a \ b) \ (x \ y) = ((a \ b) \ x) \ (y `) by Th29;
then (a \ b) \ (x \ y) = ((a \ x) \ b) \ (y `) by Th7;
then (a \ b) \ (x \ y) = (b `) \ (y `) by Lm2;
then (a \ b) \ (x \ y) = (b \ y) ` by Th9;
then (a \ b) \ (x \ y) = (0. X) ` by Lm2;
then (a \ b) \ (x \ y) = 0. X by Def5;
then a \ b <= x \ y by Def11;
hence x \ y in BranchV (a \ b) ; ::_thesis: verum
end;
theorem :: BCIALG_1:40
for X being BCI-algebra
for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ y in BCK-part X
proof
let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ y in BCK-part X
let a be Element of AtomSet X; ::_thesis: for x, y being Element of BranchV a holds x \ y in BCK-part X
let x, y be Element of BranchV a; ::_thesis: x \ y in BCK-part X
set b = a \ a;
( a \ a = 0. X & x \ y in BranchV (a \ a) ) by Def5, Th39;
hence x \ y in BCK-part X ; ::_thesis: verum
end;
theorem :: BCIALG_1:41
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
proof
let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
let a, b be Element of AtomSet X; ::_thesis: for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
let x be Element of BranchV a; ::_thesis: for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
let y be Element of BranchV b; ::_thesis: ( a <> b implies not x \ y in BCK-part X )
assume A1: a <> b ; ::_thesis: not x \ y in BCK-part X
x \ y in BranchV (a \ b) by Th39;
then ex xy being Element of X st
( x \ y = xy & a \ b <= xy ) ;
then (a \ b) \ (x \ y) = 0. X by Def11;
then (a \ (x \ y)) \ b = 0. X by Th7;
then (a \ (x \ y)) \ ((a \ (x \ y)) \ b) = a \ (x \ y) by Th2;
then A2: b = a \ (x \ y) by Th24;
assume x \ y in BCK-part X ; ::_thesis: contradiction
hence contradiction by A1, A2, Th38; ::_thesis: verum
end;
theorem :: BCIALG_1:42
for X being BCI-algebra
for a, b being Element of AtomSet X st a <> b holds
(BranchV a) /\ (BranchV b) = {}
proof
let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X st a <> b holds
(BranchV a) /\ (BranchV b) = {}
let a, b be Element of AtomSet X; ::_thesis: ( a <> b implies (BranchV a) /\ (BranchV b) = {} )
assume A1: a <> b ; ::_thesis: (BranchV a) /\ (BranchV b) = {}
assume (BranchV a) /\ (BranchV b) <> {} ; ::_thesis: contradiction
then consider c being set such that
A2: c in (BranchV a) /\ (BranchV b) by XBOOLE_0:def_1;
reconsider z2 = c as Element of BranchV b by A2, XBOOLE_0:def_4;
reconsider z1 = c as Element of BranchV a by A2, XBOOLE_0:def_4;
z1 \ z2 in BranchV (a \ b) by Th39;
then 0. X in { x3 where x3 is Element of X : a \ b <= x3 } by Def5;
then ex x3 being Element of X st
( 0. X = x3 & a \ b <= x3 ) ;
then (a \ b) \ (0. X) = 0. X by Def11;
then A3: a \ b = 0. X by Th2;
b in { xx where xx is Element of X : xx is atom } ;
then ex xx being Element of X st
( b = xx & xx is atom ) ;
hence contradiction by A1, A3, Def14; ::_thesis: verum
end;
definition
let X be BCI-algebra;
mode Ideal of X -> non empty Subset of X means :Def18: :: BCIALG_1:def 18
( 0. X in it & ( for x, y being Element of X st x \ y in it & y in it holds
x in it ) );
existence
ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y being Element of X st x \ y in b1 & y in b1 holds
x in b1 ) )
proof
take X1 = {(0. X)}; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1 ) )
A1: for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1
proof
let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 )
assume ( x \ y in X1 & y in X1 ) ; ::_thesis: x in X1
then ( x \ y = 0. X & y = 0. X ) by TARSKI:def_1;
then x = 0. X by Th2;
hence x in X1 by TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_for_xx_being_set_st_xx_in_X1_holds_
xx_in_the_carrier_of_X
let xx be set ; ::_thesis: ( xx in X1 implies xx in the carrier of X )
assume xx in X1 ; ::_thesis: xx in the carrier of X
then xx = 0. X by TARSKI:def_1;
hence xx in the carrier of X ; ::_thesis: verum
end;
hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y being Element of X st x \ y in X1 & y in X1 holds
x in X1 ) ) by A1, TARSKI:def_1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines Ideal BCIALG_1:def_18_:_
for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is Ideal of X iff ( 0. X in b2 & ( for x, y being Element of X st x \ y in b2 & y in b2 holds
x in b2 ) ) );
definition
let X be BCI-algebra;
let IT be Ideal of X;
attrIT is closed means :Def19: :: BCIALG_1:def 19
for x being Element of IT holds x ` in IT;
end;
:: deftheorem Def19 defines closed BCIALG_1:def_19_:_
for X being BCI-algebra
for IT being Ideal of X holds
( IT is closed iff for x being Element of IT holds x ` in IT );
Lm3: for X being BCI-algebra holds {(0. X)} is Ideal of X
proof
let X be BCI-algebra; ::_thesis: {(0. X)} is Ideal of X
set X1 = {(0. X)};
now__::_thesis:_for_xx_being_set_st_xx_in_{(0._X)}_holds_
xx_in_the_carrier_of_X
let xx be set ; ::_thesis: ( xx in {(0. X)} implies xx in the carrier of X )
assume xx in {(0. X)} ; ::_thesis: xx in the carrier of X
then xx = 0. X by TARSKI:def_1;
hence xx in the carrier of X ; ::_thesis: verum
end;
then A1: {(0. X)} is Subset of X by TARSKI:def_3;
A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds
x in {(0. X)}
proof
set X1 = {(0. X)};
let x, y be Element of X; ::_thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )
assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; ::_thesis: x in {(0. X)}
then ( x \ y = 0. X & y = 0. X ) by TARSKI:def_1;
then x = 0. X by Th2;
hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
0. X in {(0. X)} by TARSKI:def_1;
hence {(0. X)} is Ideal of X by A1, A2, Def18; ::_thesis: verum
end;
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)}
proof
let X be BCI-algebra; ::_thesis: for X1 being Ideal of X st X1 = {(0. X)} holds
for x being Element of X1 holds x ` in {(0. X)}
let X1 be Ideal of X; ::_thesis: ( X1 = {(0. X)} implies for x being Element of X1 holds x ` in {(0. X)} )
assume A1: X1 = {(0. X)} ; ::_thesis: for x being Element of X1 holds x ` in {(0. X)}
let x be Element of X1; ::_thesis: x ` in {(0. X)}
x = 0. X by A1, TARSKI:def_1;
then x ` = 0. X by Def5;
hence x ` in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
registration
let X be BCI-algebra;
cluster non empty closed for Ideal of X;
existence
ex b1 being Ideal of X st b1 is closed
proof
set X1 = {(0. X)};
reconsider X1 = {(0. X)} as Ideal of X by Lm3;
take X1 ; ::_thesis: X1 is closed
for x being Element of X1 holds x ` in X1 by Lm4;
hence X1 is closed by Def19; ::_thesis: verum
end;
end;
theorem :: BCIALG_1:43
for X being BCI-algebra holds {(0. X)} is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: {(0. X)} is closed Ideal of X
set X1 = {(0. X)};
reconsider X1 = {(0. X)} as Ideal of X by Lm3;
for x being Element of X1 holds x ` in X1 by Lm4;
hence {(0. X)} is closed Ideal of X by Def19; ::_thesis: verum
end;
theorem :: BCIALG_1:44
for X being BCI-algebra holds the carrier of X is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: the carrier of X is closed Ideal of X
A1: ( ( for x being Element of X holds x ` in the carrier of X ) & ( for x, y being Element of X st x \ y in the carrier of X & y in the carrier of X holds
x in the carrier of X ) ) ;
( the carrier of X is non empty Subset of X & 0. X in the carrier of X ) by ZFMISC_1:def_1;
hence the carrier of X is closed Ideal of X by A1, Def18, Def19; ::_thesis: verum
end;
theorem :: BCIALG_1:45
for X being BCI-algebra holds BCK-part X is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: BCK-part X is closed Ideal of X
set X1 = BCK-part X;
A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X
proof
let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume that
A2: x \ y in BCK-part X and
A3: y in BCK-part X ; ::_thesis: x in BCK-part X
ex x1 being Element of X st
( x \ y = x1 & 0. X <= x1 ) by A2;
then (x \ y) ` = 0. X by Def11;
then A4: (x `) \ (y `) = 0. X by Th9;
ex x2 being Element of X st
( y = x2 & 0. X <= x2 ) by A3;
then (x `) \ (0. X) = 0. X by A4, Def11;
then x ` = 0. X by Th2;
then 0. X <= x by Def11;
hence x in BCK-part X ; ::_thesis: verum
end;
0. X in BCK-part X by Th19;
then reconsider X1 = BCK-part X as Ideal of X by A1, Def18;
now__::_thesis:_for_x_being_Element_of_X1_holds_x_`_in_X1
let x be Element of X1; ::_thesis: x ` in X1
x in X1 ;
then ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
then x ` = 0. X by Def11;
then (x `) ` = 0. X by Def5;
then 0. X <= x ` by Def11;
hence x ` in X1 ; ::_thesis: verum
end;
hence BCK-part X is closed Ideal of X by Def19; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: 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
let IT be non empty Subset of X; ::_thesis: ( IT is Ideal of X implies for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT )
assume A1: IT is Ideal of X ; ::_thesis: for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT
let x, y be Element of IT; ::_thesis: { z where z is Element of X : z \ x <= y } c= IT
A2: 0. X in IT by A1, Def18;
for ss being set st ss in { z where z is Element of X : z \ x <= y } holds
ss in IT
proof
let ss be set ; ::_thesis: ( ss in { z where z is Element of X : z \ x <= y } implies ss in IT )
assume ss in { z where z is Element of X : z \ x <= y } ; ::_thesis: ss in IT
then A3: ex z being Element of X st
( ss = z & z \ x <= y ) ;
then reconsider ss = ss as Element of X ;
(ss \ x) \ y in IT by A2, A3, Def11;
then ss \ x in IT by A1, Def18;
hence ss in IT by A1, Def18; ::_thesis: verum
end;
hence { z where z is Element of X : z \ x <= y } c= IT by TARSKI:def_3; ::_thesis: verum
end;
theorem :: BCIALG_1:46
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 X st x in IT & y <= x holds
y in IT
proof
let X be BCI-algebra; ::_thesis: for IT being non empty Subset of X st IT is Ideal of X holds
for x, y being Element of X st x in IT & y <= x holds
y in IT
let IT be non empty Subset of X; ::_thesis: ( IT is Ideal of X implies for x, y being Element of X st x in IT & y <= x holds
y in IT )
assume A1: IT is Ideal of X ; ::_thesis: for x, y being Element of X st x in IT & y <= x holds
y in IT
let x, y be Element of X; ::_thesis: ( x in IT & y <= x implies y in IT )
assume that
A2: x in IT and
A3: y <= x ; ::_thesis: y in IT
y \ (0. X) <= x by A3, Th2;
then A4: y in { z where z is Element of X : z \ (0. X) <= x } ;
0. X is Element of IT by A1, Def18;
then { z where z is Element of X : z \ (0. X) <= x } c= IT by A1, A2, Lm5;
hence y in IT by A4; ::_thesis: verum
end;
begin
definition
let IT be BCI-algebra;
attrIT is associative means :Def20: :: BCIALG_1:def 20
for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z);
attrIT is quasi-associative means :Def21: :: BCIALG_1:def 21
for x being Element of IT holds (x `) ` = x ` ;
attrIT is positive-implicative means :Def22: :: BCIALG_1:def 22
for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)));
attrIT is weakly-positive-implicative means :Def23: :: BCIALG_1:def 23
for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z);
attrIT is implicative means :Def24: :: BCIALG_1:def 24
for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x);
attrIT is weakly-implicative means :: BCIALG_1:def 25
for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x;
attrIT is p-Semisimple means :Def26: :: BCIALG_1:def 26
for x, y being Element of IT holds x \ (x \ y) = y;
attrIT is alternative means :Def27: :: BCIALG_1:def 27
for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) );
end;
:: deftheorem Def20 defines associative BCIALG_1:def_20_:_
for IT being BCI-algebra holds
( IT is associative iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z) );
:: deftheorem Def21 defines quasi-associative BCIALG_1:def_21_:_
for IT being BCI-algebra holds
( IT is quasi-associative iff for x being Element of IT holds (x `) ` = x ` );
:: deftheorem Def22 defines positive-implicative BCIALG_1:def_22_:_
for IT being BCI-algebra holds
( IT is positive-implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) );
:: deftheorem Def23 defines weakly-positive-implicative BCIALG_1:def_23_:_
for IT being BCI-algebra holds
( IT is weakly-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) );
:: deftheorem Def24 defines implicative BCIALG_1:def_24_:_
for IT being BCI-algebra holds
( IT is implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) );
:: deftheorem defines weakly-implicative BCIALG_1:def_25_:_
for IT being BCI-algebra holds
( IT is weakly-implicative iff for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x );
:: deftheorem Def26 defines p-Semisimple BCIALG_1:def_26_:_
for IT being BCI-algebra holds
( IT is p-Semisimple iff for x, y being Element of IT holds x \ (x \ y) = y );
:: deftheorem Def27 defines alternative BCIALG_1:def_27_:_
for IT being BCI-algebra holds
( IT is alternative iff for x, y being Element of IT holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) );
registration
cluster BCI-EXAMPLE -> associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple ;
coherence
( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative )
proof
set IT = BCI-EXAMPLE ;
A1: BCI-EXAMPLE is positive-implicative
proof
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_22 ::_thesis: (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
thus (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by STRUCT_0:def_10; ::_thesis: verum
end;
A2: BCI-EXAMPLE is p-Semisimple
proof
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_26 ::_thesis: x \ (x \ y) = y
x \ (x \ y) = {} by CARD_1:49, TARSKI:def_1;
hence x \ (x \ y) = y by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A3: BCI-EXAMPLE is weakly-implicative
proof
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_25 ::_thesis: (x \ (y \ x)) \ ((y \ x) `) = x
(x \ (y \ x)) \ ((y \ x) `) = {} by CARD_1:49, TARSKI:def_1;
hence (x \ (y \ x)) \ ((y \ x) `) = x by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A4: BCI-EXAMPLE is associative
proof
let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_20 ::_thesis: (x \ y) \ z = x \ (y \ z)
(x \ y) \ z = {} by CARD_1:49, TARSKI:def_1;
hence (x \ y) \ z = x \ (y \ z) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A5: BCI-EXAMPLE is weakly-positive-implicative
proof
let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_23 ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
thus (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by STRUCT_0:def_10; ::_thesis: verum
end;
BCI-EXAMPLE is implicative
proof
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_24 ::_thesis: (x \ (x \ y)) \ (y \ x) = y \ (y \ x)
thus (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum
end;
hence ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) by A1, A2, A4, A3, A5; ::_thesis: verum
end;
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple for BCIStr_0 ;
existence
ex b1 being BCI-algebra st
( b1 is implicative & b1 is positive-implicative & b1 is p-Semisimple & b1 is associative & b1 is weakly-implicative & b1 is weakly-positive-implicative )
proof
take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative )
thus ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) ; ::_thesis: verum
end;
end;
Lm6: for X being BCI-algebra st ( for x, y being Element of X holds y \ x = x \ y ) holds
X is associative
proof
let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds y \ x = x \ y ) implies X is associative )
assume A1: for x, y being Element of X holds y \ x = x \ y ; ::_thesis: X is associative
let x, y, z be Element of X; :: according to BCIALG_1:def_20 ::_thesis: (x \ y) \ z = x \ (y \ z)
x \ (y \ z) = (y \ z) \ x by A1
.= (y \ x) \ z by Th7 ;
hence (x \ y) \ z = x \ (y \ z) by A1; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: ( ( for x being Element of X holds x ` = x ) implies for x, y being Element of X holds x \ y = y \ x )
assume A1: for x being Element of X holds x ` = x ; ::_thesis: for x, y being Element of X holds x \ y = y \ x
let x, y be Element of X; ::_thesis: x \ y = y \ x
A2: (y \ x) \ (x \ y) = ((y `) \ x) \ (x \ y) by A1
.= ((y `) \ (x `)) \ (x \ y) by A1
.= 0. X by Th1 ;
(x \ y) \ (y \ x) = ((x `) \ y) \ (y \ x) by A1
.= ((x `) \ (y `)) \ (y \ x) by A1
.= 0. X by Th1 ;
hence x \ y = y \ x by A2, Def7; ::_thesis: verum
end;
theorem Th47: :: BCIALG_1:47
for X being BCI-algebra holds
( X is associative iff for x being Element of X holds x ` = x )
proof
let X be BCI-algebra; ::_thesis: ( X is associative iff for x being Element of X holds x ` = x )
thus ( X is associative implies for x being Element of X holds x ` = x ) ::_thesis: ( ( for x being Element of X holds x ` = x ) implies X is associative )
proof
assume A1: X is associative ; ::_thesis: for x being Element of X holds x ` = x
let x be Element of X; ::_thesis: x ` = x
A2: x \ (x `) = (x \ (0. X)) \ x by A1, Def20
.= x \ x by Th2
.= 0. X by Def5 ;
(x `) \ x = (x \ x) ` by A1, Def20
.= (0. X) ` by Def5
.= 0. X by Def5 ;
hence x ` = x by A2, Def7; ::_thesis: verum
end;
assume for x being Element of X holds x ` = x ; ::_thesis: X is associative
then for x, y being Element of X holds x \ y = y \ x by Lm7;
hence X is associative by Lm6; ::_thesis: verum
end;
theorem Th48: :: BCIALG_1:48
for X being BCI-algebra holds
( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative )
proof
let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative )
thus ( ( for x, y being Element of X holds y \ x = x \ y ) implies X is associative ) by Lm6; ::_thesis: ( X is associative implies for x, y being Element of X holds y \ x = x \ y )
assume X is associative ; ::_thesis: for x, y being Element of X holds y \ x = x \ y
then for x being Element of X holds x ` = x by Th47;
hence for x, y being Element of X holds y \ x = x \ y by Lm7; ::_thesis: verum
end;
theorem Th49: :: BCIALG_1:49
for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )
thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) ::_thesis: ( ( for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra )
proof
assume A1: X is associative BCI-algebra ; ::_thesis: for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
let x, y, z be Element of X; ::_thesis: ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
(z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (y \ x)) \ (z \ x) by A1, Def20;
then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (y \ x) by A1, Th7;
then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (x \ y) by A1, Th48;
then A2: (z \ y) \ ((y \ x) \ (z \ x)) = 0. X by A1, Th1;
((y \ x) \ (z \ x)) \ (z \ y) = ((y \ x) \ (z \ x)) \ (y \ z) by A1, Th48;
then ((y \ x) \ (z \ x)) \ (z \ y) = 0. X by A1, Def3;
hence ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) by A1, A2, Def7, Th2; ::_thesis: verum
end;
thus ( ( for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra ) ::_thesis: verum
proof
assume A3: for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ; ::_thesis: X is associative BCI-algebra
A4: for x, y being Element of X holds y \ x = x \ y
proof
let x, y be Element of X; ::_thesis: y \ x = x \ y
(y \ (0. X)) \ (x \ (0. X)) = x \ y by A3;
then y \ (x \ (0. X)) = x \ y by A3;
hence y \ x = x \ y by A3; ::_thesis: verum
end;
A5: for a being Element of X holds a \ a = 0. X
proof
let a be Element of X; ::_thesis: a \ a = 0. X
(a `) \ (a `) = (0. X) ` by A3;
then (a \ (0. X)) \ (a `) = (0. X) ` by A4;
then (a \ (0. X)) \ (a \ (0. X)) = (0. X) ` by A4;
then a \ a = (0. X) ` by A3;
hence a \ a = 0. X by A3; ::_thesis: verum
end;
A6: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )
proof
let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )
((x \ y) \ (x \ z)) \ (z \ y) = ((y \ x) \ (x \ z)) \ (z \ y) by A4
.= ((y \ x) \ (z \ x)) \ (z \ y) by A4
.= (z \ y) \ (z \ y) by A3 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A5; ::_thesis: (x \ (x \ y)) \ y = 0. X
(x `) \ (y \ x) = y \ (0. X) by A3;
then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;
then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;
then x \ (x \ y) = y \ (0. X) by A3;
then (x \ (x \ y)) \ y = y \ y by A3;
hence (x \ (x \ y)) \ y = 0. X by A5; ::_thesis: verum
end;
for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
x = y
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume that
A7: x \ y = 0. X and
y \ x = 0. X ; ::_thesis: x = y
(x `) \ (y \ x) = y \ (0. X) by A3;
then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;
then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;
then x \ (x \ y) = y \ (0. X) by A3;
then y = x \ (x \ y) by A3
.= x by A3, A7 ;
hence x = y ; ::_thesis: verum
end;
then A8: X is being_BCI-4 by Def7;
X is being_I by A5, Def5;
then reconsider Y = X as BCI-algebra by A6, A8, Th1;
Y is associative by A4, Th48;
hence X is associative BCI-algebra ; ::_thesis: verum
end;
end;
theorem Th50: :: BCIALG_1:50
for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) )
thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) ) ::_thesis: ( ( for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) ) implies X is associative BCI-algebra )
proof
assume A1: X is associative BCI-algebra ; ::_thesis: for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x )
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ (x \ z) = z \ y & x ` = x )
(y \ x) \ (z \ x) = z \ y by A1, Th49;
then A2: (x \ y) \ (z \ x) = z \ y by A1, Th48;
x \ (0. X) = x by A1, Th49;
hence ( (x \ y) \ (x \ z) = z \ y & x ` = x ) by A1, A2, Th48; ::_thesis: verum
end;
assume A3: for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) ; ::_thesis: X is associative BCI-algebra
for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
proof
A4: for x, y being Element of X holds y \ x = x \ y
proof
let x, y be Element of X; ::_thesis: y \ x = x \ y
(y `) \ (x `) = x \ y by A3;
then y \ (x `) = x \ y by A3;
hence y \ x = x \ y by A3; ::_thesis: verum
end;
let x, y, z be Element of X; ::_thesis: ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
A5: x ` = x by A3;
(x \ y) \ (x \ z) = z \ y by A3;
then (y \ x) \ (x \ z) = z \ y by A4;
hence ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) by A4, A5; ::_thesis: verum
end;
hence X is associative BCI-algebra by Th49; ::_thesis: verum
end;
theorem :: BCIALG_1:51
for X being non empty BCIStr_0 holds
( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) )
thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ) ::_thesis: ( ( for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ) implies X is associative BCI-algebra )
proof
assume A1: X is associative BCI-algebra ; ::_thesis: for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x )
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x )
(y \ x) \ (z \ x) = z \ y by A1, Th49;
then (x \ y) \ (z \ x) = z \ y by A1, Th48;
then (x \ y) \ (x \ z) = z \ y by A1, Th48;
hence ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) by A1, Th48, Th49; ::_thesis: verum
end;
assume A2: for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ; ::_thesis: X is associative BCI-algebra
for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x )
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ (x \ z) = z \ y & x ` = x )
A3: for x, y being Element of X holds y \ x = x \ y
proof
let x, y be Element of X; ::_thesis: y \ x = x \ y
(x \ (0. X)) \ (x \ (0. X)) = (0. X) ` by A2;
then x \ (x \ (0. X)) = (0. X) ` by A2;
then x \ x = (0. X) ` by A2;
then A4: x \ x = 0. X by A2;
(x \ y) \ (x \ x) = y \ x by A2;
hence y \ x = x \ y by A2, A4; ::_thesis: verum
end;
( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) by A2;
hence ( (x \ y) \ (x \ z) = z \ y & x ` = x ) by A3; ::_thesis: verum
end;
hence X is associative BCI-algebra by Th50; ::_thesis: verum
end;
begin
theorem :: BCIALG_1:52
for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X holds x is atom )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x being Element of X holds x is atom )
thus ( X is p-Semisimple implies for x being Element of X holds x is atom ) ::_thesis: ( ( for x being Element of X holds x is atom ) implies X is p-Semisimple )
proof
assume A1: X is p-Semisimple ; ::_thesis: for x being Element of X holds x is atom
let x be Element of X; ::_thesis: x is atom
now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_
z_=_x
let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x )
assume z \ x = 0. X ; ::_thesis: z = x
then z \ (0. X) = x by A1, Def26;
hence z = x by Th2; ::_thesis: verum
end;
hence x is atom by Def14; ::_thesis: verum
end;
assume A2: for x being Element of X holds x is atom ; ::_thesis: X is p-Semisimple
for x, y being Element of X holds x \ (x \ y) = y
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y
( y is atom & (x \ (x \ y)) \ y = 0. X ) by A2, Th1;
hence x \ (x \ y) = y by Def14; ::_thesis: verum
end;
hence X is p-Semisimple by Def26; ::_thesis: verum
end;
theorem :: BCIALG_1:53
for X being BCI-algebra st X is p-Semisimple holds
BCK-part X = {(0. X)}
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies BCK-part X = {(0. X)} )
assume A1: X is p-Semisimple ; ::_thesis: BCK-part X = {(0. X)}
thus BCK-part X c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= BCK-part X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BCK-part X or x in {(0. X)} )
assume A2: x in BCK-part X ; ::_thesis: x in {(0. X)}
then A3: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
reconsider x = x as Element of X by A2;
(x `) ` = x by A1, Def26;
then (0. X) ` = x by A3, Def11;
then x = 0. X by Def5;
hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
thus {(0. X)} c= BCK-part X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in BCK-part X )
assume A4: x in {(0. X)} ; ::_thesis: x in BCK-part X
then reconsider x = x as Element of X by TARSKI:def_1;
x = 0. X by A4, TARSKI:def_1;
then x ` = 0. X by Def5;
then 0. X <= x by Def11;
hence x in BCK-part X ; ::_thesis: verum
end;
end;
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 )
proof
let X be BCI-algebra; ::_thesis: ( ( for x being Element of X holds (x `) ` = x ) iff for x, y being Element of X holds y \ (y \ x) = x )
thus ( ( for x being Element of X holds (x `) ` = x ) implies for x, y being Element of X holds y \ (y \ x) = x ) ::_thesis: ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x being Element of X holds (x `) ` = x )
proof
assume A1: for x being Element of X holds (x `) ` = x ; ::_thesis: for x, y being Element of X holds y \ (y \ x) = x
let x, y be Element of X; ::_thesis: y \ (y \ x) = x
A2: (y \ (y \ x)) \ x = 0. X by Th1;
x \ (y \ (y \ x)) = ((x \ (y \ (y \ x))) `) ` by A1
.= ((x `) \ ((y \ (y \ x)) `)) ` by Th9
.= (0. X) \ (((x `) \ ((y \ (y \ x)) `)) \ (0. X)) by Th2
.= (0. X) \ ((((0. X) \ x) \ ((y \ (y \ x)) `)) \ ((y \ (y \ x)) \ x)) by Th1
.= (0. X) \ (0. X) by Th1
.= 0. X by Def5 ;
hence y \ (y \ x) = x by A2, Def7; ::_thesis: verum
end;
thus ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x being Element of X holds (x `) ` = x ) ; ::_thesis: verum
end;
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 )
proof
let X be BCI-algebra; ::_thesis: ( ( 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 )
thus ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) ::_thesis: ( ( for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) implies for x, y being Element of X holds y \ (y \ x) = x )
proof
assume A1: for x, y being Element of X holds y \ (y \ x) = x ; ::_thesis: for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y
let x, y, z be Element of X; ::_thesis: (z \ y) \ (z \ x) = x \ y
(z \ y) \ (z \ x) = (z \ (z \ x)) \ y by Th7;
hence (z \ y) \ (z \ x) = x \ y by A1; ::_thesis: verum
end;
assume A2: for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ; ::_thesis: for x, y being Element of X holds y \ (y \ x) = x
let x, y be Element of X; ::_thesis: y \ (y \ x) = x
(y \ (0. X)) \ (y \ x) = x \ (0. X) by A2;
then y \ (y \ x) = x \ (0. X) by Th2;
hence y \ (y \ x) = x by Th2; ::_thesis: verum
end;
theorem Th54: :: BCIALG_1:54
for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X holds (x `) ` = x )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x )
( ( for x being Element of X holds (x `) ` = x ) implies X is p-Semisimple )
proof
assume A1: for x being Element of X holds (x `) ` = x ; ::_thesis: X is p-Semisimple
now__::_thesis:_for_x,_y_being_Element_of_X_holds_x_\_(x_\_y)_=_y
let x, y be Element of X; ::_thesis: x \ (x \ y) = y
A2: (x \ (x \ y)) \ y = 0. X by Th1;
y \ (x \ (x \ y)) = ((y \ (x \ (x \ y))) `) ` by A1
.= ((y `) \ ((x \ (x \ y)) `)) ` by Th9
.= (0. X) \ ((((0. X) \ y) \ ((x \ (x \ y)) `)) \ (0. X)) by Th2
.= (0. X) \ ((((0. X) \ y) \ ((x \ (x \ y)) `)) \ ((x \ (x \ y)) \ y)) by Th1
.= (0. X) \ (0. X) by Th1
.= 0. X by Def5 ;
hence x \ (x \ y) = y by A2, Def7; ::_thesis: verum
end;
hence X is p-Semisimple by Def26; ::_thesis: verum
end;
hence ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x ) by Def26; ::_thesis: verum
end;
theorem Th55: :: BCIALG_1:55
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x )
( X is p-Semisimple iff for x being Element of X holds (x `) ` = x ) by Th54;
hence ( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) by Lm8; ::_thesis: verum
end;
theorem Th56: :: BCIALG_1:56
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )
( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) by Th55;
hence ( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) by Lm9; ::_thesis: verum
end;
theorem Th57: :: BCIALG_1:57
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) )
thus ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ) ::_thesis: ( ( for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ) implies X is p-Semisimple )
proof
assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x)
let x, y, z be Element of X; ::_thesis: x \ (z \ y) = y \ (z \ x)
y \ (z \ x) = (z \ (z \ y)) \ (z \ x) by A1, Def26;
then A2: (y \ (z \ x)) \ (x \ (z \ y)) = 0. X by Th1;
x \ (z \ y) = (z \ (z \ x)) \ (z \ y) by A1, Def26;
then (x \ (z \ y)) \ (y \ (z \ x)) = 0. X by Th1;
hence x \ (z \ y) = y \ (z \ x) by A2, Def7; ::_thesis: verum
end;
assume A3: for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ; ::_thesis: X is p-Semisimple
for x being Element of X holds (x `) ` = x
proof
let x be Element of X; ::_thesis: (x `) ` = x
(x `) ` = x \ ((0. X) `) by A3
.= x \ (0. X) by Def5 ;
hence (x `) ` = x by Th2; ::_thesis: verum
end;
hence X is p-Semisimple by Th54; ::_thesis: verum
end;
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) )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies 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) ) )
assume A1: X is p-Semisimple ; ::_thesis: 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) )
let x, y, z, u be Element of X; ::_thesis: ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )
A2: (x \ u) \ (z \ y) = (x \ (z \ y)) \ u by Th7
.= (y \ (z \ x)) \ u by A1, Th57 ;
(x \ u) \ (z \ y) = y \ (z \ (x \ u)) by A1, Th57
.= y \ (u \ (x \ z)) by A1, Th57
.= (x \ z) \ (u \ y) by A1, Th57 ;
hence ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) by A2, Th7; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y )
assume A1: X is p-Semisimple ; ::_thesis: for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y
let x, y be Element of X; ::_thesis: (y `) \ ((0. X) \ x) = x \ y
(y `) \ ((0. X) \ x) = (x \ y) \ ((0. X) \ (0. X)) by A1, Lm10
.= (x \ y) \ (0. X) by Def5 ;
hence (y `) \ ((0. X) \ x) = x \ y by Th2; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z )
assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z
let x, y, z be Element of X; ::_thesis: (x \ y) \ (z \ y) = x \ z
(x \ y) \ (z \ y) = (x \ z) \ (y \ y) by A1, Lm10
.= (x \ z) \ (0. X) by Def5 ;
hence (x \ y) \ (z \ y) = x \ z by Th2; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X st x \ y = x \ z holds
y = z )
assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X st x \ y = x \ z holds
y = z
let x, y, z be Element of X; ::_thesis: ( x \ y = x \ z implies y = z )
assume A2: x \ y = x \ z ; ::_thesis: y = z
(x \ z) \ (x \ y) = (y \ z) \ (x \ x) by A1, Lm10;
then (x \ z) \ (x \ y) = (y \ z) \ (0. X) by Def5;
then (x \ z) \ (x \ y) = y \ z by Th2;
then A3: 0. X = y \ z by A2, Def5;
(x \ y) \ (x \ z) = (z \ y) \ (x \ x) by A1, Lm10;
then (x \ y) \ (x \ z) = (z \ y) \ (0. X) by Def5;
then (x \ y) \ (x \ z) = z \ y by Th2;
then 0. X = z \ y by A2, Def5;
hence y = z by A3, Def7; ::_thesis: verum
end;
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 `)
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) )
assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `)
let x, y, z be Element of X; ::_thesis: x \ (y \ z) = (z \ y) \ (x `)
x \ (y \ z) = z \ (y \ x) by A1, Th57
.= (z \ (0. X)) \ (y \ x) by Th2 ;
hence x \ (y \ z) = (z \ y) \ (x `) by A1, Lm10; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X st y \ x = z \ x holds
y = z )
assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X st y \ x = z \ x holds
y = z
let x, y, z be Element of X; ::_thesis: ( y \ x = z \ x implies y = z )
assume A2: y \ x = z \ x ; ::_thesis: y = z
A3: z \ y = (z \ x) \ (y \ x) by A1, Lm12
.= 0. X by A2, Def5 ;
y \ z = (y \ x) \ (z \ x) by A1, Lm12
.= 0. X by A2, Def5 ;
hence y = z by A3, Def7; ::_thesis: verum
end;
theorem :: BCIALG_1:58
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) )
thus ( X is p-Semisimple implies for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) by Lm10; ::_thesis: ( ( for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) implies X is p-Semisimple )
thus ( ( for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) implies X is p-Semisimple ) ::_thesis: verum
proof
assume A1: for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ; ::_thesis: X is p-Semisimple
for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x)
proof
let x, y, z be Element of X; ::_thesis: x \ (z \ y) = y \ (z \ x)
(x \ (0. X)) \ (z \ y) = (y \ (0. X)) \ (z \ x) by A1;
then x \ (z \ y) = (y \ (0. X)) \ (z \ x) by Th2;
hence x \ (z \ y) = y \ (z \ x) by Th2; ::_thesis: verum
end;
hence X is p-Semisimple by Th57; ::_thesis: verum
end;
end;
theorem Th59: :: BCIALG_1:59
for X being BCI-algebra holds
( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z )
thus ( X is p-Semisimple implies for x, z being Element of X holds (z `) \ (x `) = x \ z ) by Lm11; ::_thesis: ( ( for x, z being Element of X holds (z `) \ (x `) = x \ z ) implies X is p-Semisimple )
assume A1: for x, z being Element of X holds (z `) \ (x `) = x \ z ; ::_thesis: X is p-Semisimple
for x being Element of X holds (x `) ` = x
proof
let x be Element of X; ::_thesis: (x `) ` = x
((0. X) `) \ (x `) = x \ (0. X) by A1;
then (x `) ` = x \ (0. X) by Th2;
hence (x `) ` = x by Th2; ::_thesis: verum
end;
hence X is p-Semisimple by Th54; ::_thesis: verum
end;
theorem :: BCIALG_1:60
for X being BCI-algebra holds
( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) `) ` = x \ z )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) `) ` = x \ z )
thus ( X is p-Semisimple implies for x, z being Element of X holds ((x \ z) `) ` = x \ z ) ::_thesis: ( ( for x, z being Element of X holds ((x \ z) `) ` = x \ z ) implies X is p-Semisimple )
proof
assume A1: X is p-Semisimple ; ::_thesis: for x, z being Element of X holds ((x \ z) `) ` = x \ z
let x, z be Element of X; ::_thesis: ((x \ z) `) ` = x \ z
((x \ z) `) ` = ((x `) \ (z `)) ` by Th9
.= (z \ x) ` by A1, Th59
.= (z `) \ (x `) by Th9 ;
hence ((x \ z) `) ` = x \ z by A1, Th59; ::_thesis: verum
end;
assume A2: for x, z being Element of X holds ((x \ z) `) ` = x \ z ; ::_thesis: X is p-Semisimple
now__::_thesis:_for_x_being_Element_of_X_holds_(x_`)_`_=_x
let x be Element of X; ::_thesis: (x `) ` = x
((x \ (0. X)) `) ` = x \ (0. X) by A2;
then (x `) ` = x \ (0. X) by Th2;
hence (x `) ` = x by Th2; ::_thesis: verum
end;
hence X is p-Semisimple by Th54; ::_thesis: verum
end;
theorem :: BCIALG_1:61
for X being BCI-algebra holds
( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u )
thus ( X is p-Semisimple implies for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ) ::_thesis: ( ( for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ) implies X is p-Semisimple )
proof
assume A1: X is p-Semisimple ; ::_thesis: for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u
let x, u, z be Element of X; ::_thesis: z \ (z \ (x \ u)) = x \ u
(z \ (z \ (x \ u))) \ (x \ u) = 0. X by Th1
.= (x \ u) \ (x \ u) by Def5 ;
hence z \ (z \ (x \ u)) = x \ u by A1, Lm15; ::_thesis: verum
end;
assume A2: for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ; ::_thesis: X is p-Semisimple
now__::_thesis:_for_x_being_Element_of_X_holds_(x_`)_`_=_x
let x be Element of X; ::_thesis: (x `) ` = x
((x \ (0. X)) `) ` = x \ (0. X) by A2;
then ((x \ (0. X)) `) ` = x by Th2;
hence (x `) ` = x by Th2; ::_thesis: verum
end;
hence X is p-Semisimple by Th54; ::_thesis: verum
end;
theorem Th62: :: BCIALG_1:62
for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds
x = 0. X )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds
x = 0. X )
thus ( X is p-Semisimple implies for x being Element of X st x ` = 0. X holds
x = 0. X ) ::_thesis: ( ( for x being Element of X st x ` = 0. X holds
x = 0. X ) implies X is p-Semisimple )
proof
assume A1: X is p-Semisimple ; ::_thesis: for x being Element of X st x ` = 0. X holds
x = 0. X
let x be Element of X; ::_thesis: ( x ` = 0. X implies x = 0. X )
assume x ` = 0. X ; ::_thesis: x = 0. X
then (x `) ` = 0. X by Def5;
hence x = 0. X by A1, Def26; ::_thesis: verum
end;
assume A2: for x being Element of X st x ` = 0. X holds
x = 0. X ; ::_thesis: X is p-Semisimple
for x being Element of X holds (x `) ` = x
proof
let x be Element of X; ::_thesis: (x `) ` = x
(x \ ((x `) `)) ` = (x `) \ (((x `) `) `) by Th9
.= (x `) \ (x `) by Th8
.= 0. X by Def5 ;
then A3: x \ ((x `) `) = 0. X by A2;
((x `) `) \ x = 0. X by Th1;
hence (x `) ` = x by A3, Def7; ::_thesis: verum
end;
hence X is p-Semisimple by Th54; ::_thesis: verum
end;
theorem Th63: :: BCIALG_1:63
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) )
thus ( X is p-Semisimple implies for x, y being Element of X holds x \ (y `) = y \ (x `) ) by Th57; ::_thesis: ( ( for x, y being Element of X holds x \ (y `) = y \ (x `) ) implies X is p-Semisimple )
assume A1: for x, y being Element of X holds x \ (y `) = y \ (x `) ; ::_thesis: X is p-Semisimple
now__::_thesis:_for_x_being_Element_of_X_holds_x_=_(x_`)_`
let x be Element of X; ::_thesis: x = (x `) `
x \ ((0. X) `) = (x `) ` by A1;
then x \ (0. X) = (x `) ` by Th2;
hence x = (x `) ` by Th2; ::_thesis: verum
end;
hence X is p-Semisimple by Th54; ::_thesis: verum
end;
theorem :: BCIALG_1:64
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) )
thus ( X is p-Semisimple implies for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ) by Lm10; ::_thesis: ( ( for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ) implies X is p-Semisimple )
assume A1: for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ; ::_thesis: X is p-Semisimple
for x, z being Element of X holds (z `) \ (x `) = x \ z
proof
let x, z be Element of X; ::_thesis: (z `) \ (x `) = x \ z
(z \ x) ` = (x \ x) \ (z \ x) by Def5;
then (z \ x) ` = (x \ z) \ (x \ x) by A1;
then (z \ x) ` = (x \ z) \ (0. X) by Def5;
then (z \ x) ` = x \ z by Th2;
hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum
end;
hence X is p-Semisimple by Th59; ::_thesis: verum
end;
theorem :: BCIALG_1:65
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z )
thus ( X is p-Semisimple implies for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ) by Lm12; ::_thesis: ( ( for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ) implies X is p-Semisimple )
assume A1: for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ; ::_thesis: X is p-Semisimple
for x, z being Element of X holds (z `) \ (x `) = x \ z
proof
let x, z be Element of X; ::_thesis: (z `) \ (x `) = x \ z
(z \ x) ` = (x \ x) \ (z \ x) by Def5;
then (z \ x) ` = x \ z by A1;
hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum
end;
hence X is p-Semisimple by Th59; ::_thesis: verum
end;
theorem :: BCIALG_1:66
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) )
thus ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ) by Lm14; ::_thesis: ( ( for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ) implies X is p-Semisimple )
assume A1: for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ; ::_thesis: X is p-Semisimple
for x, y being Element of X holds x \ (y `) = y \ (x `)
proof
let x, y be Element of X; ::_thesis: x \ (y `) = y \ (x `)
x \ (y `) = (y \ (0. X)) \ (x `) by A1;
hence x \ (y `) = y \ (x `) by Th2; ::_thesis: verum
end;
hence X is p-Semisimple by Th63; ::_thesis: verum
end;
theorem :: BCIALG_1:67
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds
y = z )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds
y = z )
thus ( X is p-Semisimple implies for x, y, z being Element of X st y \ x = z \ x holds
y = z ) by Lm15; ::_thesis: ( ( for x, y, z being Element of X st y \ x = z \ x holds
y = z ) implies X is p-Semisimple )
assume A1: for x, y, z being Element of X st y \ x = z \ x holds
y = z ; ::_thesis: X is p-Semisimple
for x, y being Element of X holds x \ (x \ y) = y
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y
(x \ (x \ y)) \ y = 0. X by Th1;
then (x \ (x \ y)) \ y = y \ y by Def5;
hence x \ (x \ y) = y by A1; ::_thesis: verum
end;
hence X is p-Semisimple by Def26; ::_thesis: verum
end;
theorem :: BCIALG_1:68
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds
y = z )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds
y = z )
thus ( X is p-Semisimple implies for x, y, z being Element of X st x \ y = x \ z holds
y = z ) by Lm13; ::_thesis: ( ( for x, y, z being Element of X st x \ y = x \ z holds
y = z ) implies X is p-Semisimple )
assume A1: for x, y, z being Element of X st x \ y = x \ z holds
y = z ; ::_thesis: X is p-Semisimple
for x being Element of X st x ` = 0. X holds
x = 0. X
proof
let x be Element of X; ::_thesis: ( x ` = 0. X implies x = 0. X )
assume x ` = 0. X ; ::_thesis: x = 0. X
then x ` = (0. X) ` by Def5;
hence x = 0. X by A1; ::_thesis: verum
end;
hence X is p-Semisimple by Th62; ::_thesis: verum
end;
theorem :: BCIALG_1:69
for X being non empty BCIStr_0 holds
( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) )
thus ( X is p-Semisimple BCI-algebra implies for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) by Th2, Th56; ::_thesis: ( ( for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) implies X is p-Semisimple BCI-algebra )
assume A1: for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ; ::_thesis: X is p-Semisimple BCI-algebra
A2: now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_
(_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_&_(_for_x,_y_being_Element_of_X_holds_x_\_(x_\_y)_=_y_)_)
let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )
((x \ y) \ (x \ z)) \ (z \ y) = (z \ y) \ (z \ y) by A1
.= ((z \ y) \ (0. X)) \ (z \ y) by A1
.= ((z \ y) \ (0. X)) \ ((z \ y) \ (0. X)) by A1
.= (0. X) ` by A1 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; ::_thesis: ( (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )
(x \ (x \ y)) \ y = ((x \ (0. X)) \ (x \ y)) \ y by A1
.= (y \ (0. X)) \ y by A1
.= (y \ (0. X)) \ (y \ (0. X)) by A1
.= (0. X) ` by A1 ;
hence (x \ (x \ y)) \ y = 0. X by A1; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y
thus for x, y being Element of X holds x \ (x \ y) = y ::_thesis: verum
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y
x \ (x \ y) = (x \ (0. X)) \ (x \ y) by A1;
then x \ (x \ y) = y \ (0. X) by A1;
hence x \ (x \ y) = y by A1; ::_thesis: verum
end;
end;
now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_
x_=_y
let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume that
A3: x \ y = 0. X and
y \ x = 0. X ; ::_thesis: x = y
x = x \ (0. X) by A1
.= (x \ (0. X)) \ (x \ y) by A1, A3
.= y \ (0. X) by A1 ;
hence x = y by A1; ::_thesis: verum
end;
then A4: X is being_BCI-4 by Def7;
now__::_thesis:_for_x_being_Element_of_X_holds_x_\_x_=_0._X
let x be Element of X; ::_thesis: x \ x = 0. X
x \ x = (x \ (0. X)) \ x by A1
.= (x \ (0. X)) \ (x \ (0. X)) by A1
.= (0. X) ` by A1 ;
hence x \ x = 0. X by A1; ::_thesis: verum
end;
then X is being_I by Def5;
hence X is p-Semisimple BCI-algebra by A4, A2, Def26, Th1; ::_thesis: verum
end;
theorem :: BCIALG_1:70
for X being non empty BCIStr_0 holds
( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds
( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds
( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) )
thus ( X is p-Semisimple BCI-algebra implies ( X is being_I & ( for x, y, z being Element of X holds
( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) ) by Th2, Th57; ::_thesis: ( X is being_I & ( for x, y, z being Element of X holds
( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) implies X is p-Semisimple BCI-algebra )
assume that
A1: X is being_I and
A2: for x, y, z being Element of X holds
( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ; ::_thesis: X is p-Semisimple BCI-algebra
A3: now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_
(_x_\_x_=_0._X_&_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_&_(_for_x,_y_being_Element_of_X_holds_x_\_(x_\_y)_=_y_)_)
let x, y, z be Element of X; ::_thesis: ( x \ x = 0. X & ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )
thus x \ x = 0. X by A1, Def5; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )
((x \ y) \ (x \ z)) \ (z \ y) = (z \ (x \ (x \ y))) \ (z \ y) by A2
.= (z \ (y \ (x \ x))) \ (z \ y) by A2
.= (z \ (y \ (0. X))) \ (z \ y) by A1, Def5
.= (z \ y) \ (z \ y) by A2 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1, Def5; ::_thesis: ( (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) )
(x \ (x \ y)) \ y = (y \ (x \ x)) \ y by A2
.= (y \ (0. X)) \ y by A1, Def5
.= y \ y by A2 ;
hence (x \ (x \ y)) \ y = 0. X by A1, Def5; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y
thus for x, y being Element of X holds x \ (x \ y) = y ::_thesis: verum
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y
x \ (x \ y) = y \ (x \ x) by A2;
then x \ (x \ y) = y \ (0. X) by A1, Def5;
hence x \ (x \ y) = y by A2; ::_thesis: verum
end;
end;
now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_
x_=_y
let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume that
A4: x \ y = 0. X and
y \ x = 0. X ; ::_thesis: x = y
x = x \ (0. X) by A2
.= y \ (x \ x) by A2, A4
.= y \ (0. X) by A1, Def5 ;
hence x = y by A2; ::_thesis: verum
end;
then X is being_BCI-4 by Def7;
hence X is p-Semisimple BCI-algebra by A1, A3, Def26, Th1; ::_thesis: verum
end;
begin
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) `
proof
let X be BCI-algebra; ::_thesis: ( ( for x being Element of X holds x ` <= x ) implies for x, y being Element of X holds (x \ y) ` = (y \ x) ` )
assume A1: for x being Element of X holds x ` <= x ; ::_thesis: for x, y being Element of X holds (x \ y) ` = (y \ x) `
let x, y be Element of X; ::_thesis: (x \ y) ` = (y \ x) `
(y \ x) ` = (((y \ x) `) `) ` by Th8
.= (((y `) \ (x `)) `) ` by Th9
.= (((y `) `) \ ((x `) `)) ` by Th9
.= ((((x `) `) `) \ (y `)) ` by Th7
.= ((x `) \ (y `)) ` by Th8
.= ((x \ y) `) ` by Th9 ;
then (y \ x) ` <= (x \ y) ` by A1;
then A2: ((y \ x) `) \ ((x \ y) `) = 0. X by Def11;
(x \ y) ` = (((x \ y) `) `) ` by Th8
.= (((x `) \ (y `)) `) ` by Th9
.= (((x `) `) \ ((y `) `)) ` by Th9
.= ((((y `) `) `) \ (x `)) ` by Th7
.= ((y `) \ (x `)) ` by Th8
.= ((y \ x) `) ` by Th9 ;
then (x \ y) ` <= (y \ x) ` by A1;
then ((x \ y) `) \ ((y \ x) `) = 0. X by Def11;
hence (x \ y) ` = (y \ x) ` by A2, Def7; ::_thesis: verum
end;
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) `
proof
let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) implies for x, y being Element of X holds (x `) \ y = (x \ y) ` )
assume A1: for x, y being Element of X holds (x \ y) ` = (y \ x) ` ; ::_thesis: for x, y being Element of X holds (x `) \ y = (x \ y) `
let x, y be Element of X; ::_thesis: (x `) \ y = (x \ y) `
thus (x \ y) ` = (x `) \ (y `) by Th9
.= ((y `) `) \ x by Th7
.= ((y \ (0. X)) `) \ x by A1
.= (y `) \ x by Th2
.= (x `) \ y by Th7 ; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) implies for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )
assume A1: for x, y being Element of X holds (x `) \ y = (x \ y) ` ; ::_thesis: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X
let x, y be Element of X; ::_thesis: (x \ y) \ (y \ x) in BCK-part X
((x \ y) \ (y \ x)) ` = ((x \ y) `) \ (y \ x) by A1
.= ((x `) \ (y `)) \ (y \ x) by Th9
.= (((y `) `) \ x) \ (y \ x) by Th7
.= (((y `) \ x) `) \ (y \ x) by A1
.= (((y \ x) `) `) \ (y \ x) by A1
.= 0. X by Th1 ;
then 0. X <= (x \ y) \ (y \ x) by Def11;
hence (x \ y) \ (y \ x) in BCK-part X ; ::_thesis: verum
end;
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
proof
let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative )
assume A1: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ; ::_thesis: X is quasi-associative
for x being Element of X holds (x `) ` = x `
proof
let x be Element of X; ::_thesis: (x `) ` = x `
x \ (x `) = (x \ (0. X)) \ (x `) by Th2;
then x \ (x `) in { x2 where x2 is Element of X : 0. X <= x2 } by A1;
then ex x2 being Element of X st
( x \ (x `) = x2 & 0. X <= x2 ) ;
then (x \ (x `)) ` = 0. X by Def11;
then A2: (x `) \ ((x `) `) = 0. X by Th9;
(x `) \ x = (x `) \ (x \ (0. X)) by Th2;
then (x `) \ x in { x1 where x1 is Element of X : 0. X <= x1 } by A1;
then ex x1 being Element of X st
( (x `) \ x = x1 & 0. X <= x1 ) ;
then ((x `) \ x) ` = 0. X by Def11;
then ((x `) `) \ (x `) = 0. X by Th9;
hence (x `) ` = x ` by A2, Def7; ::_thesis: verum
end;
hence X is quasi-associative by Def21; ::_thesis: verum
end;
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) )
proof
let X be BCI-algebra; ::_thesis: ( ( 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) )
thus ( ( for x being Element of X holds x ` <= x ) implies for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) implies for x being Element of X holds x ` <= x )
proof
assume A1: for x being Element of X holds x ` <= x ; ::_thesis: for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z)
let x, y, z be Element of X; ::_thesis: (x \ y) \ z <= x \ (y \ z)
(x \ (x \ (y \ z))) \ (y \ z) = 0. X by Th1;
then A2: ((x \ (x \ (y \ z))) \ y) \ ((y \ z) \ y) = 0. X by Th4;
((x \ y) \ z) \ (x \ (y \ z)) = ((x \ y) \ (x \ (y \ z))) \ z by Th7
.= ((x \ (x \ (y \ z))) \ y) \ z by Th7 ;
then (((x \ y) \ z) \ (x \ (y \ z))) \ (((y \ z) \ y) \ z) = 0. X by A2, Th4;
then A3: (((x \ y) \ z) \ (x \ (y \ z))) \ (((y \ y) \ z) \ z) = 0. X by Th7;
z ` <= z by A1;
then (z `) \ z = 0. X by Def11;
then (((x \ y) \ z) \ (x \ (y \ z))) \ (0. X) = 0. X by A3, Def5;
then ((x \ y) \ z) \ (x \ (y \ z)) = 0. X by Th2;
hence (x \ y) \ z <= x \ (y \ z) by Def11; ::_thesis: verum
end;
assume A4: for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ; ::_thesis: for x being Element of X holds x ` <= x
let x be Element of X; ::_thesis: x ` <= x
((0. X) `) \ x <= (x `) ` by A4;
then x ` <= (x `) ` by Def5;
then (x `) \ ((x `) `) = 0. X by Def11;
then (((x `) `) `) \ x = 0. X by Th7;
then (x `) \ x = 0. X by Th8;
hence x ` <= x by Def11; ::_thesis: verum
end;
theorem Th71: :: BCIALG_1:71
for X being BCI-algebra holds
( X is quasi-associative iff for x being Element of X holds x ` <= x )
proof
let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x being Element of X holds x ` <= x )
thus ( X is quasi-associative implies for x being Element of X holds x ` <= x ) ::_thesis: ( ( for x being Element of X holds x ` <= x ) implies X is quasi-associative )
proof
assume A1: X is quasi-associative ; ::_thesis: for x being Element of X holds x ` <= x
let x be Element of X; ::_thesis: x ` <= x
((x `) `) \ x = 0. X by Th1;
then (x `) \ x = 0. X by A1, Def21;
hence x ` <= x by Def11; ::_thesis: verum
end;
assume for x being Element of X holds x ` <= x ; ::_thesis: X is quasi-associative
then for x, y being Element of X holds (x \ y) ` = (y \ x) ` by Lm16;
then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Lm17;
then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18;
hence X is quasi-associative by Lm19; ::_thesis: verum
end;
theorem Th72: :: BCIALG_1:72
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x \ y) ` = (y \ x) ` )
proof
let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y being Element of X holds (x \ y) ` = (y \ x) ` )
thus ( X is quasi-associative implies for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) ::_thesis: ( ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) implies X is quasi-associative )
proof
assume X is quasi-associative ; ::_thesis: for x, y being Element of X holds (x \ y) ` = (y \ x) `
then for x being Element of X holds x ` <= x by Th71;
hence for x, y being Element of X holds (x \ y) ` = (y \ x) ` by Lm16; ::_thesis: verum
end;
assume for x, y being Element of X holds (x \ y) ` = (y \ x) ` ; ::_thesis: X is quasi-associative
then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Lm17;
then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18;
hence X is quasi-associative by Lm19; ::_thesis: verum
end;
theorem Th73: :: BCIALG_1:73
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` )
proof
let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` )
thus ( X is quasi-associative implies for x, y being Element of X holds (x `) \ y = (x \ y) ` ) ::_thesis: ( ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) implies X is quasi-associative )
proof
assume X is quasi-associative ; ::_thesis: for x, y being Element of X holds (x `) \ y = (x \ y) `
then for x, y being Element of X holds (x \ y) ` = (y \ x) ` by Th72;
hence for x, y being Element of X holds (x `) \ y = (x \ y) ` by Lm17; ::_thesis: verum
end;
assume for x, y being Element of X holds (x `) \ y = (x \ y) ` ; ::_thesis: X is quasi-associative
then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18;
hence X is quasi-associative by Lm19; ::_thesis: verum
end;
theorem :: BCIALG_1:74
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )
proof
let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )
thus ( X is quasi-associative implies for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) ::_thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative )
proof
assume X is quasi-associative ; ::_thesis: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X
then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Th73;
hence for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18; ::_thesis: verum
end;
thus ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative ) by Lm19; ::_thesis: verum
end;
theorem :: BCIALG_1:75
for X being BCI-algebra holds
( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )
proof
let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )
thus ( X is quasi-associative implies for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) implies X is quasi-associative )
proof
assume X is quasi-associative ; ::_thesis: for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z)
then for x being Element of X holds x ` <= x by Th71;
hence for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) by Lm20; ::_thesis: verum
end;
assume for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ; ::_thesis: X is quasi-associative
then for x being Element of X holds x ` <= x by Lm20;
hence X is quasi-associative by Th71; ::_thesis: verum
end;
begin
theorem Th76: :: BCIALG_1:76
for X being BCI-algebra
for x, y being Element of X st X is alternative holds
( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X st X is alternative holds
( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )
let x, y be Element of X; ::_thesis: ( X is alternative implies ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x ) )
assume A1: X is alternative ; ::_thesis: ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )
then x \ (x \ x) = (x \ x) \ x by Def27;
then x \ (0. X) = (x \ x) \ x by Def5;
then x \ (0. X) = x ` by Def5;
hence x ` = x by Th2; ::_thesis: ( x \ (x \ y) = y & (x \ y) \ y = x )
y \ (y \ y) = (y \ y) \ y by A1, Def27;
then y \ (0. X) = (y \ y) \ y by Def5;
then y \ (0. X) = y ` by Def5;
then A2: y = y ` by Th2;
x \ (x \ y) = (x \ x) \ y by A1, Def27;
hence x \ (x \ y) = y by A2, Def5; ::_thesis: (x \ y) \ y = x
(x \ y) \ y = x \ (y \ y) by A1, Def27;
then (x \ y) \ y = x \ (0. X) by Def5;
hence (x \ y) \ y = x by Th2; ::_thesis: verum
end;
theorem :: BCIALG_1:77
for X being BCI-algebra
for x, a, b being Element of X st X is alternative & x \ a = x \ b holds
a = b
proof
let X be BCI-algebra; ::_thesis: for x, a, b being Element of X st X is alternative & x \ a = x \ b holds
a = b
let x, a, b be Element of X; ::_thesis: ( X is alternative & x \ a = x \ b implies a = b )
assume that
A1: X is alternative and
A2: x \ a = x \ b ; ::_thesis: a = b
(x \ x) \ a = x \ (x \ b) by A1, A2, Def27;
then (x \ x) \ a = (x \ x) \ b by A1, Def27;
then a ` = (x \ x) \ b by Def5;
then a ` = b ` by Def5;
then a = b ` by A1, Th76;
hence a = b by A1, Th76; ::_thesis: verum
end;
theorem :: BCIALG_1:78
for X being BCI-algebra
for a, x, b being Element of X st X is alternative & a \ x = b \ x holds
a = b
proof
let X be BCI-algebra; ::_thesis: for a, x, b being Element of X st X is alternative & a \ x = b \ x holds
a = b
let a, x, b be Element of X; ::_thesis: ( X is alternative & a \ x = b \ x implies a = b )
assume that
A1: X is alternative and
A2: a \ x = b \ x ; ::_thesis: a = b
a \ (x \ x) = (b \ x) \ x by A1, A2, Def27;
then a \ (x \ x) = b \ (x \ x) by A1, Def27;
then a \ (0. X) = b \ (x \ x) by Def5;
then a \ (0. X) = b \ (0. X) by Def5;
then a = b \ (0. X) by Th2;
hence a = b by Th2; ::_thesis: verum
end;
theorem :: BCIALG_1:79
for X being BCI-algebra
for x, y being Element of X st X is alternative & x \ y = 0. X holds
x = y
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X st X is alternative & x \ y = 0. X holds
x = y
let x, y be Element of X; ::_thesis: ( X is alternative & x \ y = 0. X implies x = y )
assume that
A1: X is alternative and
A2: x \ y = 0. X ; ::_thesis: x = y
x \ (x \ y) = x by A2, Th2;
then (x \ x) \ y = x by A1, Def27;
then y ` = x by Def5;
hence x = y by A1, Th76; ::_thesis: verum
end;
theorem :: BCIALG_1:80
for X being BCI-algebra
for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds
( a = x \ b & b = x \ a )
proof
let X be BCI-algebra; ::_thesis: for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds
( a = x \ b & b = x \ a )
let x, a, b be Element of X; ::_thesis: ( X is alternative & (x \ a) \ b = 0. X implies ( a = x \ b & b = x \ a ) )
assume that
A1: X is alternative and
A2: (x \ a) \ b = 0. X ; ::_thesis: ( a = x \ b & b = x \ a )
(x \ a) \ (b \ b) = b ` by A1, A2, Def27;
then (x \ a) \ (0. X) = b ` by Def5;
then x \ a = b ` by Th2;
then x \ (x \ a) = x \ b by A1, Th76;
then (x \ x) \ a = x \ b by A1, Def27;
then a ` = x \ b by Def5;
then a = x \ b by A1, Th76;
hence ( a = x \ b & b = x \ a ) by A1, Th76; ::_thesis: verum
end;
Lm21: for X being BCI-algebra holds
( X is alternative iff X is associative )
proof
let X be BCI-algebra; ::_thesis: ( X is alternative iff X is associative )
thus ( X is alternative implies X is associative ) ::_thesis: ( X is associative implies X is alternative )
proof
assume A1: X is alternative ; ::_thesis: X is associative
for x, y, z being Element of X holds (x \ y) \ z = x \ (y \ z)
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = x \ (y \ z)
(((x \ y) \ y) \ ((x \ y) \ z)) \ (z \ y) = 0. X by Th1;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ y) \ (y \ z)) = 0. X by Th4;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ (y \ z)) \ y) = 0. X by Th7;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z `) \ (y \ z)) \ y) = 0. X by A1, Th76;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z `) \ (y \ z)) \ (y `)) = 0. X by A1, Th76;
then A2: ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X by Def3;
((x \ y) \ z) \ (x \ (y \ z)) = ((x \ y) \ (x \ (y \ z))) \ z by Th7;
then ((x \ y) \ z) \ (x \ (y \ z)) = ((x \ (x \ (y \ z))) \ y) \ z by Th7;
then ((x \ y) \ z) \ (x \ (y \ z)) = (((x \ x) \ (y \ z)) \ y) \ z by A1, Def27;
then ((x \ y) \ z) \ (x \ (y \ z)) = (((y \ z) `) \ y) \ z by Def5;
then ((x \ y) \ z) \ (x \ (y \ z)) = ((y \ z) \ y) \ z by A1, Th76;
then ((x \ y) \ z) \ (x \ (y \ z)) = ((y \ y) \ z) \ z by Th7;
then ((x \ y) \ z) \ (x \ (y \ z)) = (z `) \ z by Def5;
then A3: ((x \ y) \ z) \ (x \ (y \ z)) = 0. X by A1, Th76;
(x \ (y \ z)) \ ((x \ y) \ z) = (((x \ y) \ y) \ (y \ z)) \ ((x \ y) \ z) by A1, Th76
.= (((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z) by Th7 ;
then (x \ (y \ z)) \ ((x \ y) \ z) = 0. X by A2, Th2;
hence (x \ y) \ z = x \ (y \ z) by A3, Def7; ::_thesis: verum
end;
hence X is associative by Def20; ::_thesis: verum
end;
assume X is associative ; ::_thesis: X is alternative
then for x, y being Element of X holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) by Def20;
hence X is alternative by Def27; ::_thesis: verum
end;
Lm22: for X being BCI-algebra st X is alternative holds
X is implicative
proof
let X be BCI-algebra; ::_thesis: ( X is alternative implies X is implicative )
assume X is alternative ; ::_thesis: X is implicative
then for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by Th76;
hence X is implicative by Def24; ::_thesis: verum
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 alternative -> associative for BCIStr_0 ;
coherence
for b1 being BCI-algebra st b1 is alternative holds
b1 is associative by Lm21;
cluster non empty being_B being_C being_I being_BCI-4 associative -> alternative for BCIStr_0 ;
coherence
for b1 being BCI-algebra st b1 is associative holds
b1 is alternative by Lm21;
cluster non empty being_B being_C being_I being_BCI-4 alternative -> implicative for BCIStr_0 ;
coherence
for b1 being BCI-algebra st b1 is alternative holds
b1 is implicative by Lm22;
end;
theorem :: BCIALG_1:81
for X being BCI-algebra
for x, y being Element of X st X is alternative holds
(x \ (x \ y)) \ (y \ x) = x
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X st X is alternative holds
(x \ (x \ y)) \ (y \ x) = x
let x, y be Element of X; ::_thesis: ( X is alternative implies (x \ (x \ y)) \ (y \ x) = x )
assume A1: X is alternative ; ::_thesis: (x \ (x \ y)) \ (y \ x) = x
then x \ (x \ y) = y by Th76;
hence (x \ (x \ y)) \ (y \ x) = x by A1, Th76; ::_thesis: verum
end;
theorem :: BCIALG_1:82
for X being BCI-algebra
for y, x being Element of X st X is alternative holds
y \ (y \ (x \ (x \ y))) = y
proof
let X be BCI-algebra; ::_thesis: for y, x being Element of X st X is alternative holds
y \ (y \ (x \ (x \ y))) = y
let y, x be Element of X; ::_thesis: ( X is alternative implies y \ (y \ (x \ (x \ y))) = y )
assume X is alternative ; ::_thesis: y \ (y \ (x \ (x \ y))) = y
then y \ (y \ (x \ (x \ y))) = y \ (y \ y) by Th76
.= y \ (0. X) by Def5
.= y by Th2 ;
hence y \ (y \ (x \ (x \ y))) = y ; ::_thesis: verum
end;
begin
Lm23: for X being BCI-algebra st X is associative holds
X is weakly-positive-implicative
proof
let X be BCI-algebra; ::_thesis: ( X is associative implies X is weakly-positive-implicative )
assume A1: X is associative ; ::_thesis: X is weakly-positive-implicative
for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
(x \ y) \ z = x \ (y \ z) by A1, Def20;
then (x \ y) \ z = (x \ (0. X)) \ (y \ z) by Th2;
then (x \ y) \ z = (x \ (z \ z)) \ (y \ z) by Def5;
hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by A1, Def20; ::_thesis: verum
end;
hence X is weakly-positive-implicative by Def23; ::_thesis: verum
end;
Lm24: for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is weakly-positive-implicative BCI-algebra
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple BCI-algebra implies X is weakly-positive-implicative BCI-algebra )
assume A1: X is p-Semisimple BCI-algebra ; ::_thesis: X is weakly-positive-implicative BCI-algebra
for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
((x \ z) \ z) \ (y \ z) = (x \ z) \ y by A1, Lm12
.= (x \ z) \ (y \ (0. X)) by Th2
.= (x \ y) \ (z \ (0. X)) by A1, Lm10 ;
hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by Th2; ::_thesis: verum
end;
hence X is weakly-positive-implicative BCI-algebra by Def23; ::_thesis: verum
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 associative -> weakly-positive-implicative for BCIStr_0 ;
coherence
for b1 being BCI-algebra st b1 is associative holds
b1 is weakly-positive-implicative by Lm23;
cluster non empty being_B being_C being_I being_BCI-4 p-Semisimple -> weakly-positive-implicative for BCIStr_0 ;
coherence
for b1 being BCI-algebra st b1 is p-Semisimple holds
b1 is weakly-positive-implicative by Lm24;
end;
theorem :: BCIALG_1:83
for X being non empty BCIStr_0 holds
( X is implicative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is implicative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) )
thus ( X is implicative BCI-algebra implies for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) by Def24, Th1, Th2; ::_thesis: ( ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) implies X is implicative BCI-algebra )
thus ( ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) implies X is implicative BCI-algebra ) ::_thesis: verum
proof
assume A1: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ; ::_thesis: X is implicative BCI-algebra
A2: now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_
(_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_)
let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )
thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; ::_thesis: (x \ (x \ y)) \ y = 0. X
(x \ (x \ y)) \ y = ((x \ (0. X)) \ (x \ y)) \ y by A1
.= ((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) by A1 ;
hence (x \ (x \ y)) \ y = 0. X by A1; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_
x_=_y
let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume that
A3: x \ y = 0. X and
A4: y \ x = 0. X ; ::_thesis: x = y
x = x \ (0. X) by A1
.= (y \ (y \ x)) \ (x \ y) by A1, A3
.= y \ (0. X) by A1, A3, A4 ;
hence x = y by A1; ::_thesis: verum
end;
then A5: X is being_BCI-4 by Def7;
now__::_thesis:_for_x_being_Element_of_X_holds_x_\_x_=_0._X
let x be Element of X; ::_thesis: x \ x = 0. X
x \ x = (x \ (0. X)) \ x by A1
.= (x \ (0. X)) \ (x \ (0. X)) by A1
.= ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) by A1
.= ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) by A1 ;
hence x \ x = 0. X by A1; ::_thesis: verum
end;
then X is being_I by Def5;
hence X is implicative BCI-algebra by A1, A5, A2, Def24, Th1; ::_thesis: verum
end;
end;
theorem Th84: :: BCIALG_1:84
for X being BCI-algebra holds
( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) )
proof
let X be BCI-algebra; ::_thesis: ( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) )
thus ( X is weakly-positive-implicative implies for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) implies X is weakly-positive-implicative )
proof
assume A1: X is weakly-positive-implicative ; ::_thesis: for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `)
let x, y be Element of X; ::_thesis: x \ y = ((x \ y) \ y) \ (y `)
(x \ (0. X)) \ y = ((x \ y) \ y) \ (y `) by A1, Def23;
hence x \ y = ((x \ y) \ y) \ (y `) by Th2; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ; ::_thesis: X is weakly-positive-implicative
for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
((x \ z) \ (y \ z)) \ (x \ y) = 0. X by Def3;
then (((x \ z) \ (y \ z)) \ z) \ ((x \ y) \ z) = 0. X by Th4;
then A3: (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) = 0. X by Th7;
(((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (y \ z) = 0. X by Th1;
then ((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ ((y \ z) \ (z `)) = 0. X by Th4;
then (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (((y \ z) \ (z `)) \ y) = 0. X by Th4;
then (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (((y \ z) \ (z `)) \ (y \ (0. X))) = 0. X by Th2;
then A4: (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (0. X) = 0. X by Def3;
((x \ y) \ z) \ (((x \ z) \ z) \ (y \ z)) = ((x \ z) \ y) \ (((x \ z) \ z) \ (y \ z)) by Th7
.= ((((x \ z) \ z) \ (z `)) \ y) \ (((x \ z) \ z) \ (y \ z)) by A2
.= ((((x \ z) \ z) \ (z `)) \ (((x \ z) \ z) \ (y \ z))) \ y by Th7
.= ((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y by Th7 ;
then ((x \ y) \ z) \ (((x \ z) \ z) \ (y \ z)) = 0. X by A4, Th2;
hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by A3, Def7; ::_thesis: verum
end;
hence X is weakly-positive-implicative by Def23; ::_thesis: verum
end;
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)
proof
let X be BCI-algebra; ::_thesis: 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)
let x, y be Element of X; ::_thesis: ( X is weakly-positive-implicative implies (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) )
assume A1: X is weakly-positive-implicative ; ::_thesis: (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)
((x \ (x \ y)) \ (y \ (x \ y))) \ (x \ y) = 0. X by Def3;
then ((x \ (x \ y)) \ (x \ y)) \ (y \ (x \ y)) = 0. X by Th7;
then (((x \ (x \ y)) \ (x \ y)) \ ((x \ y) `)) \ ((y \ (x \ y)) \ ((x \ y) `)) = 0. X by Th4;
then ((((x \ (x \ y)) \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) \ (((y \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) = 0. X by Th4;
then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) = 0. X by A1, Th84;
then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (((x \ y) `) \ (y \ x))) = 0. X by A1, Def23;
then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (((x \ x) \ (x \ y)) \ (y \ x))) = 0. X by Def5;
then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (0. X)) = 0. X by Th1;
then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (x \ y)) \ (y \ x)) \ (y \ x)) = 0. X by Th2;
then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (y \ x)) \ (x \ y)) \ (y \ x)) = 0. X by Th7;
then A2: ((x \ (x \ y)) \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) = 0. X by Th7;
((y \ (y \ x)) \ (y \ x)) \ (x \ (y \ x)) = 0. X by Th1;
then (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) \ ((x \ (y \ x)) \ (x \ y)) = 0. X by Th4;
then (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by Th7;
hence (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by A2, Def7; ::_thesis: verum
end;
Lm26: for X being BCI-algebra holds
( X is positive-implicative iff X is weakly-positive-implicative )
proof
let X be BCI-algebra; ::_thesis: ( X is positive-implicative iff X is weakly-positive-implicative )
thus ( X is positive-implicative implies X is weakly-positive-implicative ) ::_thesis: ( X is weakly-positive-implicative implies X is positive-implicative )
proof
assume A1: X is positive-implicative ; ::_thesis: X is weakly-positive-implicative
for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `)
proof
let x, y be Element of X; ::_thesis: x \ y = ((x \ y) \ y) \ (y `)
((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) by A1, Def22;
then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ (x \ y)) by Th8;
then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (0. X) by Def5;
then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = x \ y by Th2;
then ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) = x \ y by Th7;
then ((x \ y) \ (x \ (x \ y))) \ ((x \ x) \ y) = x \ y by Th7;
then ((x \ (x \ (x \ y))) \ y) \ ((x \ x) \ y) = x \ y by Th7;
then ((x \ y) \ y) \ ((x \ x) \ y) = x \ y by Th8;
hence x \ y = ((x \ y) \ y) \ (y `) by Def5; ::_thesis: verum
end;
hence X is weakly-positive-implicative by Th84; ::_thesis: verum
end;
assume A2: X is weakly-positive-implicative ; ::_thesis: X is positive-implicative
for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
proof
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
A3: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) by A2, Lm25;
(y \ (y \ x)) \ x = 0. X by Th1;
then (x \ x) \ (x \ (y \ (y \ x))) = 0. X by Th4;
then (x \ (y \ (y \ x))) ` = 0. X by Def5;
then x \ (x \ (y \ (y \ x))) = ((x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x)))) \ (0. X) by A2, Th84;
then x \ (x \ (y \ (y \ x))) = (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) by Th2;
then (x \ (x \ (y \ (y \ x)))) \ ((y \ (y \ x)) \ (x \ (y \ (y \ x)))) = 0. X by Th1;
then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((y \ (y \ x)) \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) = 0. X by Th4;
then A4: ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (x \ (y \ (y \ x)))) = 0. X by Th7;
((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) `)) = ((((y \ (y \ x)) \ (y \ x)) \ ((y \ x) `)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) `)) by A2, Th84
.= 0. X by Th1 ;
then (((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (x \ (y \ (y \ x)))) \ (((x \ y) \ ((y \ x) `)) \ (x \ (y \ (y \ x)))) = 0. X by Th4;
then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((x \ y) \ ((y \ x) `)) \ (x \ (y \ (y \ x)))) = 0. X by A4, Th3;
then A5: ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ x) `)) = 0. X by Th7;
((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ (y \ x)) \ y) = 0. X by Th1;
then ((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ y) \ (y \ x)) = 0. X by Th7;
then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (0. X) = 0. X by A5, Def5;
then A6: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by A3, Th2;
((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by Th10;
hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A6, Def7; ::_thesis: verum
end;
hence X is positive-implicative by Def22; ::_thesis: verum
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 positive-implicative -> weakly-positive-implicative for BCIStr_0 ;
coherence
for b1 being BCI-algebra st b1 is positive-implicative holds
b1 is weakly-positive-implicative by Lm26;
cluster non empty being_B being_C being_I being_BCI-4 alternative -> weakly-positive-implicative for BCIStr_0 ;
coherence
for b1 being BCI-algebra st b1 is alternative holds
b1 is weakly-positive-implicative ;
end;
theorem :: BCIALG_1:85
for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds
for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by Lm25;
theorem :: BCIALG_1:86
for X being non empty BCIStr_0 holds
( X is positive-implicative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is positive-implicative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) )
thus ( X is positive-implicative BCI-algebra implies for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) by Lm25, Th1, Th2, Th84; ::_thesis: ( ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) implies X is positive-implicative BCI-algebra )
assume A1: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ; ::_thesis: X is positive-implicative BCI-algebra
now__::_thesis:_for_x_being_Element_of_X_holds_x_\_x_=_0._X
let x be Element of X; ::_thesis: x \ x = 0. X
((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) = 0. X by A1;
then ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) = 0. X by A1;
then ((x \ (0. X)) \ x) \ (0. X) = 0. X by A1;
then (x \ x) \ (0. X) = 0. X by A1;
hence x \ x = 0. X by A1; ::_thesis: verum
end;
then A2: X is being_I by Def5;
now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_
x_=_y
let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume ( x \ y = 0. X & y \ x = 0. X ) ; ::_thesis: x = y
then (x \ (0. X)) \ (0. X) = ((y \ (0. X)) \ (0. X)) \ (0. X) by A1;
then x \ (0. X) = ((y \ (0. X)) \ (0. X)) \ (0. X) by A1;
then x = ((y \ (0. X)) \ (0. X)) \ (0. X) by A1;
then x = (y \ (0. X)) \ (0. X) by A1;
then x = y \ (0. X) by A1;
hence x = y by A1; ::_thesis: verum
end;
then A3: X is being_BCI-4 by Def7;
now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_
(_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_)
let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )
thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; ::_thesis: (x \ (x \ y)) \ y = 0. X
((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) = 0. X by A1;
then (x \ (x \ y)) \ (y \ (0. X)) = 0. X by A1;
hence (x \ (x \ y)) \ y = 0. X by A1; ::_thesis: verum
end;
then X is weakly-positive-implicative BCI-algebra by A1, A2, A3, Th1, Th84;
hence X is positive-implicative BCI-algebra by Lm26; ::_thesis: verum
end;