:: BCIALG_3 semantic presentation
begin
definition
let IT be non empty BCIStr_0 ;
attrIT is commutative means :Def1: :: BCIALG_3:def 1
for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x);
end;
:: deftheorem Def1 defines commutative BCIALG_3:def_1_:_
for IT being non empty BCIStr_0 holds
( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );
registration
cluster BCI-EXAMPLE -> commutative ;
coherence
BCI-EXAMPLE is commutative
proof
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_1 ::_thesis: x \ (x \ y) = y \ (y \ x)
thus x \ (x \ y) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative for BCIStr_0 ;
existence
ex b1 being BCK-algebra st b1 is commutative
proof
take BCI-EXAMPLE ; ::_thesis: BCI-EXAMPLE is commutative
thus BCI-EXAMPLE is commutative ; ::_thesis: verum
end;
end;
theorem Th1: :: BCIALG_3:1
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies X is commutative BCK-algebra )
proof
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x)
x \ (x \ y) = y \ (y \ x) by A1, Def1;
then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by BCIALG_1:def_5;
hence x \ (x \ y) <= y \ (y \ x) by BCIALG_1:def_11; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: X is commutative BCK-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x)
y \ (y \ x) <= x \ (x \ y) by A2;
then A3: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X by BCIALG_1:def_11;
x \ (x \ y) <= y \ (y \ x) by A2;
then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by BCIALG_1:def_11;
hence x \ (x \ y) = y \ (y \ x) by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is commutative BCK-algebra by Def1; ::_thesis: verum
end;
theorem Th2: :: BCIALG_3:2
for X being BCK-algebra
for x, y being Element of X holds
( x \ (x \ y) <= y & x \ (x \ y) <= x )
proof
let X be BCK-algebra; ::_thesis: for x, y being Element of X holds
( x \ (x \ y) <= y & x \ (x \ y) <= x )
let x, y be Element of X; ::_thesis: ( x \ (x \ y) <= y & x \ (x \ y) <= x )
A1: (0. X) \ (x \ y) = (x \ y) `
.= 0. X by BCIALG_1:def_8 ;
((x \ (x \ y)) \ ((0. X) \ (x \ y))) \ (x \ (0. X)) = 0. X by BCIALG_1:def_3;
then ((x \ (x \ y)) \ (0. X)) \ x = 0. X by A1, BCIALG_1:2;
then ( (x \ (x \ y)) \ y = 0. X & (x \ (x \ y)) \ x = 0. X ) by BCIALG_1:1, BCIALG_1:2;
hence ( x \ (x \ y) <= y & x \ (x \ y) <= x ) by BCIALG_1:def_11; ::_thesis: verum
end;
theorem Th3: :: BCIALG_3:3
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies X is commutative BCK-algebra )
proof
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
let x, y be Element of X; ::_thesis: x \ y = x \ (y \ (y \ x))
x \ y = x \ (x \ (x \ y)) by BCIALG_1:8
.= x \ (y \ (y \ x)) by A1, Def1 ;
hence x \ y = x \ (y \ (y \ x)) ; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: X is commutative BCK-algebra
for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x)
x \ (x \ (y \ (y \ x))) <= y \ (y \ x) by Th2;
hence x \ (x \ y) <= y \ (y \ x) by A2; ::_thesis: verum
end;
hence X is commutative BCK-algebra by Th1; ::_thesis: verum
end;
theorem Th4: :: BCIALG_3:4
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies X is commutative BCK-algebra )
proof
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y)))
y \ (y \ x) = y \ (y \ (x \ (x \ y))) by A1, Th3;
hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A1, Def1; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: X is commutative BCK-algebra
for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x)
x \ (x \ y) <= x by Th2;
then A3: y \ x <= y \ (x \ (x \ y)) by BCIALG_1:5;
x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2;
hence x \ (x \ y) <= y \ (y \ x) by A3, BCIALG_1:5; ::_thesis: verum
end;
hence X is commutative BCK-algebra by Th1; ::_thesis: verum
end;
theorem Th5: :: BCIALG_3:5
for X being BCK-algebra holds
( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds
x = y \ (y \ x) )
thus ( X is commutative BCK-algebra implies for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds
x = y \ (y \ x) ) implies X is commutative BCK-algebra )
proof
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X st x <= y holds
x = y \ (y \ x)
let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) )
assume x <= y ; ::_thesis: x = y \ (y \ x)
then x \ y = 0. X by BCIALG_1:def_11;
then y \ (y \ x) = x \ (0. X) by A1, Def1
.= x by BCIALG_1:2 ;
hence x = y \ (y \ x) ; ::_thesis: verum
end;
assume A2: for x, y being Element of X st x <= y holds
x = y \ (y \ x) ; ::_thesis: X is commutative BCK-algebra
for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x)
(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7
.= (x \ y) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ (x \ y) <= x by BCIALG_1:def_11;
then A3: y \ x <= y \ (x \ (x \ y)) by BCIALG_1:5;
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then x \ (x \ y) <= y by BCIALG_1:def_11;
then x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2;
hence x \ (x \ y) <= y \ (y \ x) by A3, BCIALG_1:5; ::_thesis: verum
end;
hence X is commutative BCK-algebra by Th1; ::_thesis: verum
end;
theorem Th6: :: BCIALG_3:6
for X being non empty BCIStr_0 holds
( X is commutative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is commutative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) )
thus ( X is commutative BCK-algebra implies for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) ::_thesis: ( ( for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) implies X is commutative BCK-algebra )
proof
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) )
let x, y, z be Element of X; ::_thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) )
(x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def1;
then A2: (x \ z) \ (x \ y) = (y \ (y \ x)) \ z by A1, BCIALG_1:7
.= (y \ z) \ (y \ x) by A1, BCIALG_1:7 ;
(0. X) \ y = y `
.= 0. X by A1, BCIALG_1:def_8 ;
hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) by A1, A2, BCIALG_1:2; ::_thesis: verum
end;
assume A3: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ; ::_thesis: X is commutative BCK-algebra
A4: for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x)
x \ (x \ y) = (x \ ((0. X) \ y)) \ (x \ y) by A3
.= (y \ ((0. X) \ y)) \ (y \ x) by A3
.= y \ (y \ x) by A3 ;
hence x \ (x \ y) = y \ (y \ x) ; ::_thesis: verum
end;
A5: for x, y being Element of X holds x \ (0. X) = x
proof
let x, y be Element of X; ::_thesis: x \ (0. X) = x
(0. X) \ ((0. X) \ (0. X)) = 0. X by A3;
hence x \ (0. X) = x by A3; ::_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 ( x \ y = 0. X & y \ x = 0. X ) ; ::_thesis: x = y
then (x \ (0. X)) \ (0. X) = (y \ (0. X)) \ (0. X) by A3;
then x \ (0. X) = (y \ (0. X)) \ (0. X) by A5
.= y \ (0. X) by A5 ;
hence x = y \ (0. X) by A5
.= y by A5 ;
::_thesis: verum
end;
then A6: X is being_BCI-4 by BCIALG_1:def_7;
A7: for x being Element of X holds x \ x = 0. X
proof
let x be Element of X; ::_thesis: x \ x = 0. X
x = x \ (0. X) by A5;
then x \ x = ((0. X) \ (0. X)) \ ((0. X) \ x) by A3
.= (0. X) \ ((0. X) \ x) by A5
.= 0. X by A3 ;
hence x \ x = 0. X ; ::_thesis: verum
end;
A8: for x being Element of X holds (0. X) \ x = 0. X
proof
let x be Element of X; ::_thesis: (0. X) \ x = 0. X
0. X = ((0. X) \ x) \ ((0. X) \ x) by A7
.= (0. X) \ x by A3 ;
hence (0. X) \ x = 0. X ; ::_thesis: verum
end;
A9: for x, y, z being Element of X holds ((x \ y) \ (x \ z)) \ (z \ y) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ y) \ (x \ z)) \ (z \ y) = 0. X
((x \ y) \ (x \ z)) \ (z \ y) = ((z \ y) \ (z \ x)) \ (z \ y) by A3
.= ((z \ y) \ (z \ x)) \ ((z \ y) \ (0. X)) by A5
.= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3
.= (0. X) \ ((0. X) \ (z \ y)) by A8
.= 0. X by A8 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ; ::_thesis: verum
end;
A10: for x, y being Element of X holds (x \ (x \ y)) \ y = 0. X
proof
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ y = 0. X
0. X = ((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) by A9
.= (x \ (x \ y)) \ (y \ (0. X)) by A5
.= (x \ (x \ y)) \ y by A5 ;
hence (x \ (x \ y)) \ y = 0. X ; ::_thesis: verum
end;
A11: X is being_I by A7, BCIALG_1:def_5;
for x being Element of X holds x ` = 0. X by A8;
hence X is commutative BCK-algebra by A4, A9, A10, A11, A6, Def1, BCIALG_1:1, BCIALG_1:def_8; ::_thesis: verum
end;
theorem :: BCIALG_3:7
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X st x \ y = x holds
y \ x = y
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y being Element of X st x \ y = x holds
y \ x = y )
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X st x \ y = x holds
y \ x = y
let x, y be Element of X; ::_thesis: ( x \ y = x implies y \ x = y )
assume x \ y = x ; ::_thesis: y \ x = y
then y \ (y \ x) = x \ x by A1, Def1
.= 0. X by BCIALG_1:def_5 ;
then y \ x = y \ (0. X) by BCIALG_1:8
.= y by BCIALG_1:2 ;
hence y \ x = y ; ::_thesis: verum
end;
theorem Th8: :: BCIALG_3:8
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x )
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x
let x, y, a be Element of X; ::_thesis: ( y <= a implies (a \ x) \ (a \ y) = y \ x )
assume y <= a ; ::_thesis: (a \ x) \ (a \ y) = y \ x
then A2: y \ a = 0. X by BCIALG_1:def_11;
(a \ x) \ (a \ y) = (a \ (a \ y)) \ x by BCIALG_1:7
.= (y \ (0. X)) \ x by A1, A2, Def1
.= y \ x by BCIALG_1:2 ;
hence (a \ x) \ (a \ y) = y \ x ; ::_thesis: verum
end;
theorem :: BCIALG_3:9
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) )
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X )
A2: for x, y being Element of X st y \ (y \ x) = 0. X holds
x \ y = x
proof
let x, y be Element of X; ::_thesis: ( y \ (y \ x) = 0. X implies x \ y = x )
assume A3: y \ (y \ x) = 0. X ; ::_thesis: x \ y = x
x \ y = x \ (x \ (x \ y)) by BCIALG_1:8
.= x \ (0. X) by A1, A3, Def1
.= x by BCIALG_1:2 ;
hence x \ y = x ; ::_thesis: verum
end;
for x, y being Element of X st x \ y = x holds
y \ (y \ x) = 0. X
proof
let x, y be Element of X; ::_thesis: ( x \ y = x implies y \ (y \ x) = 0. X )
assume x \ y = x ; ::_thesis: y \ (y \ x) = 0. X
then y \ (y \ x) = x \ x by A1, Def1
.= 0. X by BCIALG_1:def_5 ;
hence y \ (y \ x) = 0. X ; ::_thesis: verum
end;
hence for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) by A2; ::_thesis: verum
end;
theorem :: BCIALG_3:10
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )
proof
let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) )
assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )
let x, y be Element of X; ::_thesis: ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )
A2: (x \ y) \ ((x \ y) \ x) = x \ (x \ (x \ y)) by A1, Def1
.= x \ y by BCIALG_1:8 ;
x \ (y \ (y \ x)) = x \ (x \ (x \ y)) by A1, Def1
.= x \ y by BCIALG_1:8 ;
hence ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A2; ::_thesis: verum
end;
theorem :: BCIALG_3:11
for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by Th8;
definition
let X be BCI-algebra;
let a be Element of X;
attra is being_greatest means :Def2: :: BCIALG_3:def 2
for x being Element of X holds x \ a = 0. X;
attra is being_positive means :: BCIALG_3:def 3
(0. X) \ a = 0. X;
end;
:: deftheorem Def2 defines being_greatest BCIALG_3:def_2_:_
for X being BCI-algebra
for a being Element of X holds
( a is being_greatest iff for x being Element of X holds x \ a = 0. X );
:: deftheorem defines being_positive BCIALG_3:def_3_:_
for X being BCI-algebra
for a being Element of X holds
( a is being_positive iff (0. X) \ a = 0. X );
begin
definition
let IT be BCI-algebra;
attrIT is BCI-commutative means :Def4: :: BCIALG_3:def 4
for x, y being Element of IT st x \ y = 0. IT holds
x = y \ (y \ x);
attrIT is BCI-weakly-commutative means :Def5: :: BCIALG_3:def 5
for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x);
end;
:: deftheorem Def4 defines BCI-commutative BCIALG_3:def_4_:_
for IT being BCI-algebra holds
( IT is BCI-commutative iff for x, y being Element of IT st x \ y = 0. IT holds
x = y \ (y \ x) );
:: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def_5_:_
for IT being BCI-algebra holds
( IT is BCI-weakly-commutative iff for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x) );
registration
cluster BCI-EXAMPLE -> BCI-commutative BCI-weakly-commutative ;
coherence
( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative )
proof
set IT = BCI-EXAMPLE ;
thus BCI-EXAMPLE is BCI-commutative ::_thesis: BCI-EXAMPLE is BCI-weakly-commutative
proof
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_4 ::_thesis: ( x \ y = 0. BCI-EXAMPLE implies x = y \ (y \ x) )
thus ( x \ y = 0. BCI-EXAMPLE implies x = y \ (y \ x) ) by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_5 ::_thesis: (x \ (x \ y)) \ ((0. BCI-EXAMPLE) \ (x \ y)) = y \ (y \ x)
thus (x \ (x \ y)) \ ((0. BCI-EXAMPLE) \ (x \ y)) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 BCI-commutative BCI-weakly-commutative for BCIStr_0 ;
existence
ex b1 being BCI-algebra st
( b1 is BCI-commutative & b1 is BCI-weakly-commutative )
proof
take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative )
thus ( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative ) ; ::_thesis: verum
end;
end;
theorem :: BCIALG_3:12
for X being BCI-algebra st ex a being Element of X st a is being_greatest holds
X is BCK-algebra
proof
let X be BCI-algebra; ::_thesis: ( ex a being Element of X st a is being_greatest implies X is BCK-algebra )
given a being Element of X such that A1: a is being_greatest ; ::_thesis: X is BCK-algebra
for x being Element of X holds x ` = 0. X
proof
let x be Element of X; ::_thesis: x ` = 0. X
x \ a = 0. X by A1, Def2;
then x ` = (x \ x) \ a by BCIALG_1:7
.= 0. X by A1, Def2 ;
hence x ` = 0. X ; ::_thesis: verum
end;
hence X is BCK-algebra by BCIALG_1:def_8; ::_thesis: verum
end;
theorem :: BCIALG_3:13
for X being BCI-algebra st X is p-Semisimple holds
( X is BCI-commutative & X is BCI-weakly-commutative )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies ( X is BCI-commutative & X is BCI-weakly-commutative ) )
assume A1: X is p-Semisimple ; ::_thesis: ( X is BCI-commutative & X is BCI-weakly-commutative )
A2: for x, y being Element of X holds (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)
(0. X) \ (x \ y) = ((0. X) \ (0. X)) \ (x \ y) by BCIALG_1:def_5
.= ((0. X) \ x) \ ((0. X) \ y) by A1, BCIALG_1:64
.= (y \ x) \ ((0. X) \ (0. X)) by A1, BCIALG_1:58
.= (y \ x) \ (0. X) by BCIALG_1:def_5
.= y \ x by BCIALG_1:2 ;
hence (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) by A1, BCIALG_1:def_26; ::_thesis: verum
end;
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x) by A1, BCIALG_1:def_26;
hence ( X is BCI-commutative & X is BCI-weakly-commutative ) by A2, Def4, Def5; ::_thesis: verum
end;
theorem :: BCIALG_3:14
for X being commutative BCK-algebra holds
( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra )
proof
let X be commutative BCK-algebra; ::_thesis: ( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra )
A1: for x, y being Element of X holds (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)
A2: (0. X) \ (x \ y) = (x \ y) `
.= 0. X by BCIALG_1:def_8 ;
x \ (x \ y) = y \ (y \ x) by Def1;
hence (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) by A2, BCIALG_1:2; ::_thesis: verum
end;
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x)
then x <= y by BCIALG_1:def_11;
hence x = y \ (y \ x) by Th5; ::_thesis: verum
end;
hence ( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra ) by A1, Def4, Def5; ::_thesis: verum
end;
theorem :: BCIALG_3:15
for X being BCK-algebra st X is BCI-weakly-commutative BCI-algebra holds
X is BCI-commutative
proof
let X be BCK-algebra; ::_thesis: ( X is BCI-weakly-commutative BCI-algebra implies X is BCI-commutative )
assume A1: X is BCI-weakly-commutative BCI-algebra ; ::_thesis: X is BCI-commutative
let x, y be Element of X; :: according to BCIALG_3:def_4 ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x)
then (x \ (0. X)) \ ((0. X) \ (0. X)) = y \ (y \ x) by A1, Def5;
then (x \ (0. X)) \ (0. X) = y \ (y \ x) by BCIALG_1:def_5;
then x \ (0. X) = y \ (y \ x) by BCIALG_1:2;
hence x = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum
end;
theorem Th16: :: BCIALG_3:16
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
A1: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies X is BCI-commutative )
proof
assume A2: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: X is BCI-commutative
let x, y be Element of X; :: according to BCIALG_3:def_4 ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x)
then x \ (x \ y) = x by BCIALG_1:2;
hence x = y \ (y \ x) by A2; ::_thesis: verum
end;
( X is BCI-commutative implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
assume A3: X is BCI-commutative ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y)))
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A3, Def4; ::_thesis: verum
end;
hence ( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) by A1; ::_thesis: verum
end;
theorem Th17: :: BCIALG_3:17
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )
proof
let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )
A1: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ) implies X is BCI-commutative )
proof
assume A2: for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ; ::_thesis: X is BCI-commutative
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
A3: (y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
assume A4: x \ y = 0. X ; ::_thesis: x = y \ (y \ x)
then 0. X = (0. X) \ (x \ y) by BCIALG_1:2
.= (x \ (0. X)) \ (y \ (y \ x)) by A2, A4
.= x \ (y \ (y \ x)) by BCIALG_1:2 ;
hence x = y \ (y \ x) by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCI-commutative by Def4; ::_thesis: verum
end;
( X is BCI-commutative implies for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) )
proof
assume A5: X is BCI-commutative ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y)
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y)
(x \ (x \ y)) \ (y \ (y \ x)) = (y \ (y \ (x \ (x \ y)))) \ (y \ (y \ x)) by A5, Th16
.= (y \ (y \ (y \ x))) \ (y \ (x \ (x \ y))) by BCIALG_1:7
.= (y \ x) \ (y \ (x \ (x \ y))) by BCIALG_1:8
.= (y \ (y \ (x \ (x \ y)))) \ x by BCIALG_1:7
.= (x \ (x \ y)) \ x by A5, Th16
.= (x \ x) \ (x \ y) by BCIALG_1:7 ;
hence (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) by BCIALG_1:def_5; ::_thesis: verum
end;
hence ( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ) by A1; ::_thesis: verum
end;
theorem :: BCIALG_3:18
for X being BCI-algebra holds
( X is BCI-commutative iff for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) )
proof
let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) )
thus ( X is BCI-commutative implies for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) ::_thesis: ( ( for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) implies X is BCI-commutative )
proof
assume A1: X is BCI-commutative ; ::_thesis: for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x)
let a be Element of AtomSet X; ::_thesis: for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x)
let x, y be Element of BranchV a; ::_thesis: x \ (x \ y) = y \ (y \ x)
y \ x in BranchV (a \ a) by BCIALG_1:39;
then ex z1 being Element of X st
( y \ x = z1 & a \ a <= z1 ) ;
then 0. X <= y \ x by BCIALG_1:def_5;
then (0. X) \ (y \ x) = 0. X by BCIALG_1:def_11;
then A2: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X by A1, Th17;
x \ y in BranchV (a \ a) by BCIALG_1:39;
then ex z being Element of X st
( x \ y = z & a \ a <= z ) ;
then 0. X <= x \ y by BCIALG_1:def_5;
then (0. X) \ (x \ y) = 0. X by BCIALG_1:def_11;
then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by A1, Th17;
hence x \ (x \ y) = y \ (y \ x) by A2, BCIALG_1:def_7; ::_thesis: verum
end;
assume A3: for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ; ::_thesis: X is BCI-commutative
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
set aa = (0. X) \ ((0. X) \ x);
(((0. X) \ ((0. X) \ x)) `) ` = (0. X) \ ((0. X) \ x) by BCIALG_1:8;
then A4: (0. X) \ ((0. X) \ x) in AtomSet X by BCIALG_1:29;
A5: ((0. X) \ ((0. X) \ x)) \ x = ((0. X) \ x) \ ((0. X) \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then A6: (0. X) \ ((0. X) \ x) <= x by BCIALG_1:def_11;
assume A7: x \ y = 0. X ; ::_thesis: x = y \ (y \ x)
then ((0. X) \ ((0. X) \ x)) \ y = 0. X by A5, BCIALG_1:3;
then (0. X) \ ((0. X) \ x) <= y by BCIALG_1:def_11;
then consider aa being Element of AtomSet X such that
A8: ( aa <= x & aa <= y ) by A4, A6;
( x in BranchV aa & y in BranchV aa ) by A8;
then x \ (x \ y) = y \ (y \ x) by A3;
hence x = y \ (y \ x) by A7, BCIALG_1:2; ::_thesis: verum
end;
hence X is BCI-commutative by Def4; ::_thesis: verum
end;
theorem :: BCIALG_3:19
for X being non empty BCIStr_0 holds
( X is BCI-commutative 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 \ (y \ (x \ (x \ y))) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is BCI-commutative 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 \ (y \ (x \ (x \ y))) ) )
( ( 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 \ (y \ (x \ (x \ y))) ) ) implies X is BCI-commutative BCI-algebra )
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 \ (y \ (x \ (x \ y))) ) ; ::_thesis: X is BCI-commutative BCI-algebra
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
A2: x \ y = 0. X and
A3: y \ x = 0. X ; ::_thesis: x = y
A4: x \ (x \ y) = x by A1, A2;
y \ (y \ (x \ (x \ y))) = y \ (0. X) by A1, A2, A3
.= y by A1 ;
hence x = y by A1, A4; ::_thesis: verum
end;
then X is being_BCI-4 by BCIALG_1:def_7;
hence X is BCI-commutative BCI-algebra by A1, Th16, BCIALG_1:11; ::_thesis: verum
end;
hence ( X is BCI-commutative 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 \ (y \ (x \ (x \ y))) ) ) by Th16, BCIALG_1:1, BCIALG_1:2; ::_thesis: verum
end;
theorem :: BCIALG_3:20
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y )
proof
let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y )
A1: ( ( for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y ) implies X is BCI-commutative )
proof
assume A2: for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y ; ::_thesis: X is BCI-commutative
for x, z being Element of X st x \ z = 0. X holds
x = z \ (z \ x)
proof
let x, z be Element of X; ::_thesis: ( x \ z = 0. X implies x = z \ (z \ x) )
set y = z \ (z \ x);
(z \ (z \ (z \ x))) \ (z \ x) = (z \ x) \ (z \ x) by BCIALG_1:8
.= 0. X by BCIALG_1:def_5 ;
then A3: z \ (z \ (z \ x)) <= z \ x by BCIALG_1:def_11;
assume x \ z = 0. X ; ::_thesis: x = z \ (z \ x)
then x <= z by BCIALG_1:def_11;
then x <= z \ (z \ x) by A2, A3;
then A4: x \ (z \ (z \ x)) = 0. X by BCIALG_1:def_11;
(z \ (z \ x)) \ x = (z \ x) \ (z \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
hence x = z \ (z \ x) by A4, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCI-commutative by Def4; ::_thesis: verum
end;
( X is BCI-commutative implies for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y )
proof
assume A5: X is BCI-commutative ; ::_thesis: for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y
for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y
proof
let x, y, z be Element of X; ::_thesis: ( x <= z & z \ y <= z \ x implies x <= y )
assume that
A6: x <= z and
A7: z \ y <= z \ x ; ::_thesis: x <= y
x \ z = 0. X by A6, BCIALG_1:def_11;
then A8: x = z \ (z \ x) by A5, Def4;
(z \ y) \ (z \ x) = 0. X by A7, BCIALG_1:def_11;
then 0. X = x \ y by A8, BCIALG_1:7;
hence x <= y by BCIALG_1:def_11; ::_thesis: verum
end;
hence for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y ; ::_thesis: verum
end;
hence ( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds
x <= y ) by A1; ::_thesis: verum
end;
theorem :: BCIALG_3:21
for X being BCI-algebra holds
( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) )
proof
let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) )
thus ( X is BCI-commutative implies for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) ) ::_thesis: ( ( for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) ) implies X is BCI-commutative )
proof
assume A1: X is BCI-commutative ; ::_thesis: for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z)
for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z)
proof
let x, y, z be Element of X; ::_thesis: ( x <= y & x <= z implies x <= y \ (y \ z) )
assume that
A2: x <= y and
A3: x <= z ; ::_thesis: x <= y \ (y \ z)
A4: x \ z = 0. X by A3, BCIALG_1:def_11;
x \ y = 0. X by A2, BCIALG_1:def_11;
then A5: x = y \ (y \ x) by A1, Def4;
then x \ (y \ (y \ z)) = (y \ (y \ (y \ z))) \ (y \ x) by BCIALG_1:7
.= (y \ z) \ (y \ x) by BCIALG_1:8
.= 0. X by A4, A5, BCIALG_1:7 ;
hence x <= y \ (y \ z) by BCIALG_1:def_11; ::_thesis: verum
end;
hence for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) ; ::_thesis: verum
end;
assume A6: for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) ; ::_thesis: X is BCI-commutative
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
x \ x = 0. X by BCIALG_1:def_5;
then A7: x <= x by BCIALG_1:def_11;
assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x)
then x <= y by BCIALG_1:def_11;
then x <= y \ (y \ x) by A6, A7;
then A8: x \ (y \ (y \ x)) = 0. X by BCIALG_1:def_11;
(y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
hence x = y \ (y \ x) by A8, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCI-commutative by Def4; ::_thesis: verum
end;
begin
definition
let IT be BCK-algebra;
attrIT is bounded means :: BCIALG_3:def 6
ex a being Element of IT st a is being_greatest ;
end;
:: deftheorem defines bounded BCIALG_3:def_6_:_
for IT being BCK-algebra holds
( IT is bounded iff ex a being Element of IT st a is being_greatest );
registration
cluster BCI-EXAMPLE -> bounded ;
coherence
BCI-EXAMPLE is bounded
proof
set IT = BCI-EXAMPLE ;
set a = the Element of BCI-EXAMPLE;
BCI-EXAMPLE is bounded
proof
take the Element of BCI-EXAMPLE ; :: according to BCIALG_3:def_6 ::_thesis: the Element of BCI-EXAMPLE is being_greatest
for x being Element of BCI-EXAMPLE holds x \ the Element of BCI-EXAMPLE = 0. BCI-EXAMPLE by STRUCT_0:def_10;
hence the Element of BCI-EXAMPLE is being_greatest by Def2; ::_thesis: verum
end;
hence BCI-EXAMPLE is bounded ; ::_thesis: verum
end;
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded for BCIStr_0 ;
existence
ex b1 being BCK-algebra st
( b1 is bounded & b1 is commutative )
proof
take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative )
thus ( BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative ) ; ::_thesis: verum
end;
end;
definition
let IT be bounded BCK-algebra;
attrIT is involutory means :Def7: :: BCIALG_3:def 7
for a being Element of IT st a is being_greatest holds
for x being Element of IT holds a \ (a \ x) = x;
end;
:: deftheorem Def7 defines involutory BCIALG_3:def_7_:_
for IT being bounded BCK-algebra holds
( IT is involutory iff for a being Element of IT st a is being_greatest holds
for x being Element of IT holds a \ (a \ x) = x );
theorem Th22: :: BCIALG_3:22
for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )
proof
let X be bounded BCK-algebra; ::_thesis: ( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )
thus ( X is involutory implies for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) ::_thesis: ( ( for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) implies X is involutory )
proof
assume A1: X is involutory ; ::_thesis: for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)
let a be Element of X; ::_thesis: ( a is being_greatest implies for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )
assume A2: a is being_greatest ; ::_thesis: for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x)
proof
let x, y be Element of X; ::_thesis: x \ y = (a \ y) \ (a \ x)
x \ y = (a \ (a \ x)) \ y by A1, A2, Def7
.= (a \ y) \ (a \ x) by BCIALG_1:7 ;
hence x \ y = (a \ y) \ (a \ x) ; ::_thesis: verum
end;
hence for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ; ::_thesis: verum
end;
assume A3: for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ; ::_thesis: X is involutory
let a be Element of X; :: according to BCIALG_3:def_7 ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x )
assume A4: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x
now__::_thesis:_for_x_being_Element_of_X_holds_a_\_(a_\_x)_=_x
let x be Element of X; ::_thesis: a \ (a \ x) = x
(a \ (a \ x)) \ (0. X) = (a \ (0. X)) \ (a \ x) by BCIALG_1:7
.= x \ (0. X) by A3, A4
.= x by BCIALG_1:2 ;
hence a \ (a \ x) = x by BCIALG_1:2; ::_thesis: verum
end;
hence for x being Element of X holds a \ (a \ x) = x ; ::_thesis: verum
end;
theorem Th23: :: BCIALG_3:23
for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) )
proof
let X be bounded BCK-algebra; ::_thesis: ( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) )
thus ( X is involutory implies for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ) ::_thesis: ( ( for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ) implies X is involutory )
proof
assume A1: X is involutory ; ::_thesis: for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x)
let a be Element of X; ::_thesis: ( a is being_greatest implies for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) )
assume A2: a is being_greatest ; ::_thesis: for x, y being Element of X holds x \ (a \ y) = y \ (a \ x)
let x, y be Element of X; ::_thesis: x \ (a \ y) = y \ (a \ x)
( x \ (a \ y) = (a \ (a \ y)) \ (a \ x) & y \ (a \ x) = (a \ (a \ x)) \ (a \ y) ) by A1, A2, Th22;
hence x \ (a \ y) = y \ (a \ x) by BCIALG_1:7; ::_thesis: verum
end;
assume A3: for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ; ::_thesis: X is involutory
let a be Element of X; :: according to BCIALG_3:def_7 ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x )
assume A4: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x
let x be Element of X; ::_thesis: a \ (a \ x) = x
a \ (a \ x) = x \ (a \ a) by A3, A4
.= x \ (0. X) by BCIALG_1:def_5
.= x by BCIALG_1:2 ;
hence a \ (a \ x) = x ; ::_thesis: verum
end;
theorem :: BCIALG_3:24
for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x )
proof
let X be bounded BCK-algebra; ::_thesis: ( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x )
thus ( X is involutory implies for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x ) ::_thesis: ( ( for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x ) implies X is involutory )
proof
assume A1: X is involutory ; ::_thesis: for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x
let a be Element of X; ::_thesis: ( a is being_greatest implies for x, y being Element of X st x <= a \ y holds
y <= a \ x )
assume A2: a is being_greatest ; ::_thesis: for x, y being Element of X st x <= a \ y holds
y <= a \ x
let x, y be Element of X; ::_thesis: ( x <= a \ y implies y <= a \ x )
assume x <= a \ y ; ::_thesis: y <= a \ x
then x \ (a \ y) = 0. X by BCIALG_1:def_11;
then y \ (a \ x) = 0. X by A1, A2, Th23;
hence y <= a \ x by BCIALG_1:def_11; ::_thesis: verum
end;
assume A3: for a being Element of X st a is being_greatest holds
for x, y being Element of X st x <= a \ y holds
y <= a \ x ; ::_thesis: X is involutory
let a be Element of X; :: according to BCIALG_3:def_7 ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x )
assume A4: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x
let x be Element of X; ::_thesis: a \ (a \ x) = x
(a \ x) \ (a \ x) = 0. X by BCIALG_1:def_5;
then a \ x <= a \ x by BCIALG_1:def_11;
then x <= a \ (a \ x) by A3, A4;
then A5: x \ (a \ (a \ x)) = 0. X by BCIALG_1:def_11;
(a \ (a \ x)) \ x = (a \ x) \ (a \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
hence a \ (a \ x) = x by A5, BCIALG_1:def_7; ::_thesis: verum
end;
definition
let IT be BCK-algebra;
let a be Element of IT;
attra is being_Iseki means :Def8: :: BCIALG_3:def 8
for x being Element of IT holds
( x \ a = 0. IT & a \ x = a );
end;
:: deftheorem Def8 defines being_Iseki BCIALG_3:def_8_:_
for IT being BCK-algebra
for a being Element of IT holds
( a is being_Iseki iff for x being Element of IT holds
( x \ a = 0. IT & a \ x = a ) );
definition
let IT be BCK-algebra;
attrIT is Iseki_extension means :: BCIALG_3:def 9
ex a being Element of IT st a is being_Iseki ;
end;
:: deftheorem defines Iseki_extension BCIALG_3:def_9_:_
for IT being BCK-algebra holds
( IT is Iseki_extension iff ex a being Element of IT st a is being_Iseki );
registration
cluster BCI-EXAMPLE -> Iseki_extension ;
coherence
BCI-EXAMPLE is Iseki_extension
proof
set IT = BCI-EXAMPLE ;
BCI-EXAMPLE is Iseki_extension
proof
set a = the Element of BCI-EXAMPLE;
take the Element of BCI-EXAMPLE ; :: according to BCIALG_3:def_9 ::_thesis: the Element of BCI-EXAMPLE is being_Iseki
for x being Element of BCI-EXAMPLE holds
( x \ the Element of BCI-EXAMPLE = 0. BCI-EXAMPLE & the Element of BCI-EXAMPLE \ x = the Element of BCI-EXAMPLE ) by STRUCT_0:def_10;
hence the Element of BCI-EXAMPLE is being_Iseki by Def8; ::_thesis: verum
end;
hence BCI-EXAMPLE is Iseki_extension ; ::_thesis: verum
end;
end;
definition
let X be BCK-algebra;
mode Commutative-Ideal of X -> non empty Subset of X means :Def10: :: BCIALG_3:def 10
( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & z in it holds
x \ (y \ (y \ x)) in it ) );
existence
ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & z in b1 holds
x \ (y \ (y \ x)) in b1 ) )
proof
set X1 = BCK-part X;
A1: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X
proof
let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume that
(x \ y) \ z in BCK-part X and
z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def_8 ;
then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11;
hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum
end;
0. X in BCK-part X by BCIALG_1:19;
hence ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & z in b1 holds
x \ (y \ (y \ x)) in b1 ) ) by A1; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines Commutative-Ideal BCIALG_3:def_10_:_
for X being BCK-algebra
for b2 being non empty Subset of X holds
( b2 is Commutative-Ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & z in b2 holds
x \ (y \ (y \ x)) in b2 ) ) );
theorem :: BCIALG_3:25
for X being BCK-algebra
for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT
proof
let X be BCK-algebra; ::_thesis: for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT
let IT be non empty Subset of X; ::_thesis: ( IT is Commutative-Ideal of X implies for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT )
assume A1: IT is Commutative-Ideal of X ; ::_thesis: for x, y being Element of X st x \ y in IT holds
x \ (y \ (y \ x)) in IT
let x, y be Element of X; ::_thesis: ( x \ y in IT implies x \ (y \ (y \ x)) in IT )
assume x \ y in IT ; ::_thesis: x \ (y \ (y \ x)) in IT
then A2: (x \ y) \ (0. X) in IT by BCIALG_1:2;
thus x \ (y \ (y \ x)) in IT by A1, A2, Def10; ::_thesis: verum
end;
theorem Th26: :: BCIALG_3:26
for X being BCK-algebra
for IT being non empty Subset of X
for X being BCK-algebra st IT is Commutative-Ideal of X holds
IT is Ideal of X
proof
let X be BCK-algebra; ::_thesis: for IT being non empty Subset of X
for X being BCK-algebra st IT is Commutative-Ideal of X holds
IT is Ideal of X
let IT be non empty Subset of X; ::_thesis: for X being BCK-algebra st IT is Commutative-Ideal of X holds
IT is Ideal of X
let X be BCK-algebra; ::_thesis: ( IT is Commutative-Ideal of X implies IT is Ideal of X )
assume A1: IT is Commutative-Ideal of X ; ::_thesis: IT is Ideal of X
A2: for x, y being Element of X st x \ y in IT & y in IT holds
x in IT
proof
let x, y be Element of X; ::_thesis: ( x \ y in IT & y in IT implies x in IT )
assume that
A3: x \ y in IT and
A4: y in IT ; ::_thesis: x in IT
A5: x \ ((0. X) \ ((0. X) \ x)) = x \ ((0. X) \ (x `))
.= x \ ((0. X) \ (0. X)) by BCIALG_1:def_8
.= x \ (0. X) by BCIALG_1:def_5
.= x by BCIALG_1:2 ;
(x \ (0. X)) \ y in IT by A3, BCIALG_1:2;
hence x in IT by A1, A4, A5, Def10; ::_thesis: verum
end;
0. X in IT by A1, Def10;
hence IT is Ideal of X by A1, A2, BCIALG_1:def_18; ::_thesis: verum
end;
theorem :: BCIALG_3:27
for X being BCK-algebra
for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT
proof
let X be BCK-algebra; ::_thesis: for IT being non empty Subset of X st IT is Commutative-Ideal of X holds
for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT
let IT be non empty Subset of X; ::_thesis: ( IT is Commutative-Ideal of X implies for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT )
assume IT is Commutative-Ideal of X ; ::_thesis: for x, y being Element of X st x \ (x \ y) in IT holds
(y \ (y \ x)) \ (x \ y) in IT
then A1: IT is Ideal of X by Th26;
let x, y be Element of X; ::_thesis: ( x \ (x \ y) in IT implies (y \ (y \ x)) \ (x \ y) in IT )
((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) = ((y \ (x \ y)) \ (y \ x)) \ (x \ (x \ y)) by BCIALG_1:7
.= 0. X by BCIALG_1:11 ;
then A2: (y \ (y \ x)) \ (x \ y) <= x \ (x \ y) by BCIALG_1:def_11;
assume x \ (x \ y) in IT ; ::_thesis: (y \ (y \ x)) \ (x \ y) in IT
hence (y \ (y \ x)) \ (x \ y) in IT by A1, A2, BCIALG_1:46; ::_thesis: verum
end;
begin
definition
let IT be BCK-algebra;
attrIT is BCK-positive-implicative means :Def11: :: BCIALG_3:def 11
for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z);
attrIT is BCK-implicative means :Def12: :: BCIALG_3:def 12
for x, y being Element of IT holds x \ (y \ x) = x;
end;
:: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def_11_:_
for IT being BCK-algebra holds
( IT is BCK-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z) );
:: deftheorem Def12 defines BCK-implicative BCIALG_3:def_12_:_
for IT being BCK-algebra holds
( IT is BCK-implicative iff for x, y being Element of IT holds x \ (y \ x) = x );
registration
cluster BCI-EXAMPLE -> BCK-positive-implicative BCK-implicative ;
coherence
( BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative )
proof
set IT = BCI-EXAMPLE ;
thus BCI-EXAMPLE is BCK-positive-implicative ::_thesis: BCI-EXAMPLE is BCK-implicative
proof
let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_11 ::_thesis: (x \ y) \ z = (x \ z) \ (y \ z)
thus (x \ y) \ z = (x \ z) \ (y \ z) by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_12 ::_thesis: x \ (y \ x) = x
thus x \ (y \ x) = x by STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded Iseki_extension BCK-positive-implicative BCK-implicative for BCIStr_0 ;
existence
ex b1 being BCK-algebra st
( b1 is Iseki_extension & b1 is BCK-positive-implicative & b1 is BCK-implicative & b1 is bounded & b1 is commutative )
proof
take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is Iseki_extension & BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative & BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative )
thus ( BCI-EXAMPLE is Iseki_extension & BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative & BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative ) ; ::_thesis: verum
end;
end;
theorem Th28: :: BCIALG_3:28
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ y = (x \ y) \ y ) ::_thesis: ( ( for x, y being Element of X holds x \ y = (x \ y) \ y ) implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = (x \ y) \ y
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
(x \ y) \ y = (x \ y) \ (y \ y) by A1, Def11
.= (x \ y) \ (0. X) by BCIALG_1:def_5
.= x \ y by BCIALG_1:2 ;
hence x \ y = (x \ y) \ y ; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ y = (x \ y) \ y ; ::_thesis: X is BCK-positive-implicative BCK-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ (y \ z)
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ (y \ z)
(y \ z) \ y = (y \ y) \ z by BCIALG_1:7
.= z ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then y \ z <= y by BCIALG_1:def_11;
then (x \ z) \ y <= (x \ z) \ (y \ z) by BCIALG_1:5;
then ((x \ z) \ y) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:def_11;
then A3: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7;
((x \ z) \ (y \ z)) \ ((x \ y) \ z) = (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) by A2
.= (((x \ z) \ z) \ (y \ z)) \ ((x \ z) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_3 ;
hence (x \ y) \ z = (x \ z) \ (y \ z) by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-positive-implicative BCK-algebra by Def11; ::_thesis: verum
end;
theorem Th29: :: BCIALG_3:29
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) ::_thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
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)))
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then x \ (x \ y) <= y by BCIALG_1:def_11;
then A2: (x \ (x \ y)) \ (y \ (y \ x)) <= y \ (y \ (y \ x)) by BCIALG_1:5;
(x \ (x \ y)) \ (x \ (x \ (y \ (y \ x)))) = (x \ (x \ (x \ (y \ (y \ x))))) \ (x \ y) by BCIALG_1:7
.= (x \ (y \ (y \ x))) \ (x \ y) by BCIALG_1:8
.= (x \ (x \ y)) \ (y \ (y \ x)) by BCIALG_1:7 ;
then (x \ (x \ y)) \ (x \ (x \ (y \ (y \ x)))) <= y \ x by A2, BCIALG_1:8;
then ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) \ (y \ x) = 0. X by BCIALG_1:def_11;
then A3: ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by BCIALG_1:7;
(y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then y \ (y \ x) <= x by BCIALG_1:def_11;
then (y \ (y \ x)) \ (y \ x) <= x \ (y \ x) by BCIALG_1:5;
then y \ (y \ x) <= x \ (y \ x) by A1, Th28;
then A4: (y \ (y \ x)) \ (x \ (y \ x)) = 0. X by BCIALG_1:def_11;
(x \ (x \ (y \ (y \ x)))) \ (y \ (y \ x)) = (x \ (y \ (y \ x))) \ (x \ (y \ (y \ x))) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ x)) = 0. X by A4, BCIALG_1:3;
then x \ (x \ (y \ (y \ x))) <= x \ (y \ x) by BCIALG_1:def_11;
then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) <= (x \ (y \ x)) \ (x \ (y \ (y \ x))) by BCIALG_1:5;
then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) <= (x \ (x \ (y \ (y \ x)))) \ (y \ x) by BCIALG_1:7;
then x \ (x \ (y \ (y \ x))) <= (x \ (x \ (y \ (y \ x)))) \ (y \ x) by A1, Th28;
then A5: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) = 0. X by BCIALG_1:def_11;
(y \ (y \ x)) \ y = (y \ y) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then y \ (y \ x) <= y by BCIALG_1:def_11;
then x \ y <= x \ (y \ (y \ x)) by BCIALG_1:5;
then x \ (x \ (y \ (y \ x))) <= x \ (x \ y) by BCIALG_1:5;
then (x \ (x \ (y \ (y \ x)))) \ (y \ x) <= (x \ (x \ y)) \ (y \ x) by BCIALG_1:5;
then ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by BCIALG_1:def_11;
then (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by A5, BCIALG_1:3;
hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ; ::_thesis: verum
end;
assume A6: for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ; ::_thesis: X is BCK-positive-implicative BCK-algebra
for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
A7: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8
.= (x \ y) \ (0. X) by BCIALG_1:def_5
.= x \ y by BCIALG_1:2 ;
((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) by BCIALG_1:7
.= ((x \ y) \ (y `)) \ (x \ (x \ y)) by BCIALG_1:def_5
.= ((x \ y) \ (0. X)) \ (x \ (x \ y)) by BCIALG_1:def_8
.= (x \ y) \ (x \ (x \ y)) by BCIALG_1:2
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
hence x \ y = (x \ y) \ y by A6, A7; ::_thesis: verum
end;
hence X is BCK-positive-implicative BCK-algebra by Th28; ::_thesis: verum
end;
theorem :: BCIALG_3:30
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ) implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y))
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ (x \ (x \ y))
A2: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) by BCIALG_1:7
.= ((x \ y) \ (y `)) \ (x \ (x \ y)) by BCIALG_1:def_5
.= ((x \ y) \ (0. X)) \ (x \ (x \ y)) by BCIALG_1:def_8
.= (x \ y) \ (x \ (x \ y)) by BCIALG_1:2 ;
(x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8
.= (x \ y) \ (0. X) by BCIALG_1:def_5
.= x \ y by BCIALG_1:2 ;
hence x \ y = (x \ y) \ (x \ (x \ y)) by A1, A2, Th29; ::_thesis: verum
end;
assume A3: for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ; ::_thesis: X is BCK-positive-implicative BCK-algebra
for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
(x \ y) \ (x \ (x \ y)) = (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
hence x \ y = (x \ y) \ y by A3; ::_thesis: verum
end;
hence X is BCK-positive-implicative BCK-algebra by Th28; ::_thesis: verum
end;
theorem :: BCIALG_3:31
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z
let x, y, z be Element of X; ::_thesis: (x \ z) \ (y \ z) <= (x \ y) \ z
((x \ z) \ (y \ z)) \ ((x \ y) \ z) = ((x \ z) \ (y \ z)) \ ((x \ z) \ (y \ z)) by A1, Def11
.= 0. X by BCIALG_1:def_5 ;
hence (x \ z) \ (y \ z) <= (x \ y) \ z by BCIALG_1:def_11; ::_thesis: verum
end;
assume A2: for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ; ::_thesis: X is BCK-positive-implicative BCK-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ (y \ z)
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ (y \ z)
(y \ z) \ y = (y \ y) \ z by BCIALG_1:7
.= z ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then y \ z <= y by BCIALG_1:def_11;
then x \ y <= x \ (y \ z) by BCIALG_1:5;
then (x \ y) \ z <= (x \ (y \ z)) \ z by BCIALG_1:5;
then ((x \ y) \ z) \ ((x \ (y \ z)) \ z) = 0. X by BCIALG_1:def_11;
then A3: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7;
(x \ z) \ (y \ z) <= (x \ y) \ z by A2;
then ((x \ z) \ (y \ z)) \ ((x \ y) \ z) = 0. X by BCIALG_1:def_11;
hence (x \ y) \ z = (x \ z) \ (y \ z) by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-positive-implicative BCK-algebra by Def11; ::_thesis: verum
end;
theorem :: BCIALG_3:32
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ y <= (x \ y) \ y ) ::_thesis: ( ( for x, y being Element of X holds x \ y <= (x \ y) \ y ) implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y <= (x \ y) \ y
let x, y be Element of X; ::_thesis: x \ y <= (x \ y) \ y
(x \ y) \ ((x \ y) \ y) = ((x \ y) \ y) \ ((x \ y) \ y) by A1, Th28
.= 0. X by BCIALG_1:def_5 ;
hence x \ y <= (x \ y) \ y by BCIALG_1:def_11; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ y <= (x \ y) \ y ; ::_thesis: X is BCK-positive-implicative BCK-algebra
for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
x \ y <= (x \ y) \ y by A2;
then A3: (x \ y) \ ((x \ y) \ y) = 0. X by BCIALG_1:def_11;
((x \ y) \ y) \ (x \ y) = ((x \ y) \ (x \ y)) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ y = (x \ y) \ y by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-positive-implicative BCK-algebra by Th28; ::_thesis: verum
end;
theorem :: BCIALG_3:33
for X being BCK-algebra holds
( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ) implies X is BCK-positive-implicative BCK-algebra )
proof
assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x)
let x, y be Element of X; ::_thesis: x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x)
(x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x)))) \ (x \ (x \ (y \ (y \ x)))) by A1, Th29
.= 0. X by BCIALG_1:def_5 ;
hence x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) by BCIALG_1:def_11; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ; ::_thesis: X is BCK-positive-implicative BCK-algebra
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)))
x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) by A2;
then A3: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by BCIALG_1:def_11;
((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by BCIALG_1:10;
hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-positive-implicative BCK-algebra by Th29; ::_thesis: verum
end;
theorem Th34: :: BCIALG_3:34
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) )
thus ( X is BCK-implicative BCK-algebra implies ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) ) ::_thesis: ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra )
A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x)
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then x \ (x \ y) <= y by BCIALG_1:def_11;
then (x \ (x \ y)) \ (y \ x) <= y \ (y \ x) by BCIALG_1:5;
then (x \ (y \ x)) \ (x \ y) <= y \ (y \ x) by BCIALG_1:7;
hence x \ (x \ y) <= y \ (y \ x) by A1, Def12; ::_thesis: verum
end;
for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
(x \ y) \ (y \ (x \ y)) = x \ y by A1, Def12;
hence x \ y = (x \ y) \ y by A1, Def12; ::_thesis: verum
end;
hence ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) by A2, Th1, Th28; ::_thesis: verum
end;
assume that
A3: X is commutative BCK-algebra and
A4: X is BCK-positive-implicative BCK-algebra ; ::_thesis: X is BCK-implicative BCK-algebra
for x, y being Element of X holds x \ (y \ x) = x
proof
let x, y be Element of X; ::_thesis: x \ (y \ x) = x
x \ (x \ (x \ (y \ x))) = x \ (y \ x) by BCIALG_1:8;
then A5: x \ (y \ x) = x \ ((y \ x) \ ((y \ x) \ x)) by A3, Def1;
(y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by A4, Th28
.= 0. X by BCIALG_1:def_5 ;
hence x \ (y \ x) = x by A5, BCIALG_1:2; ::_thesis: verum
end;
hence X is BCK-implicative BCK-algebra by Def12; ::_thesis: verum
end;
theorem Th35: :: BCIALG_3:35
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) )
thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ) implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
X is commutative BCK-algebra by A1, Th34;
then (x \ (x \ y)) \ (x \ y) = (y \ (y \ x)) \ (x \ y) by Def1
.= (y \ (x \ y)) \ (y \ x) by BCIALG_1:7 ;
hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, Def12; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ; ::_thesis: X is BCK-implicative BCK-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y
proof
let x, y be Element of X; ::_thesis: (x \ y) \ y = x \ y
A3: (x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:8
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
A4: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
(x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ x) by A2;
hence (x \ y) \ y = x \ y by A3, A4, BCIALG_1:2; ::_thesis: verum
end;
then A5: X is BCK-positive-implicative BCK-algebra by Th28;
for x, y being Element of X st x <= y holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) )
assume x <= y ; ::_thesis: x = y \ (y \ x)
then A6: x \ y = 0. X by BCIALG_1:def_11;
then y \ (y \ x) = (x \ (x \ y)) \ (0. X) by A2
.= x \ (0. X) by A6, BCIALG_1:2 ;
hence x = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum
end;
then X is commutative BCK-algebra by Th5;
hence X is BCK-implicative BCK-algebra by A5, Th34; ::_thesis: verum
end;
theorem :: BCIALG_3:36
for X being non empty BCIStr_0 holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) )
proof
let X be non empty BCIStr_0 ; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) )
thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) ::_thesis: ( ( for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) )
then A2: X is commutative BCK-algebra by Th34;
let x, y, z be Element of X; ::_thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) )
A3: x \ ((0. X) \ y) = x \ (y `)
.= x \ (0. X) by A1, BCIALG_1:def_8
.= x by A1, BCIALG_1:2 ;
((y \ z) \ (y \ x)) \ (x \ y) = ((y \ z) \ (x \ y)) \ (y \ x) by A1, BCIALG_1:7
.= ((y \ (x \ y)) \ z) \ (y \ x) by A1, BCIALG_1:7
.= (y \ z) \ (y \ x) by A1, Def12
.= (y \ (y \ x)) \ z by A1, BCIALG_1:7
.= (x \ (x \ y)) \ z by A2, Def1
.= (x \ z) \ (x \ y) by A1, BCIALG_1:7 ;
hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) by A3; ::_thesis: verum
end;
assume A4: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ; ::_thesis: X is BCK-implicative BCK-algebra
A5: for x, y being Element of X holds x \ (0. X) = x
proof
let x, y be Element of X; ::_thesis: x \ (0. X) = x
(0. X) \ ((0. X) \ (0. X)) = 0. X by A4;
hence x \ (0. X) = x by A4; ::_thesis: verum
end;
A6: 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 ( 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 A4
.= (y \ (0. X)) \ (0. X) by A5 ;
then x \ (0. X) = (y \ (0. X)) \ (0. X) by A5
.= y \ (0. X) by A5 ;
hence x = y \ (0. X) by A5
.= y by A5 ;
::_thesis: verum
end;
A7: for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = (y \ (y \ x)) \ (x \ y)
x \ (x \ y) = (x \ (0. X)) \ (x \ y) by A5
.= ((y \ (0. X)) \ (y \ x)) \ (x \ y) by A4 ;
hence x \ (x \ y) = (y \ (y \ x)) \ (x \ y) by A5; ::_thesis: verum
end;
A8: for y being Element of X holds y \ y = 0. X
proof
let y be Element of X; ::_thesis: y \ y = 0. X
(0. X) \ ((0. X) \ y) = (y \ (y \ (0. X))) \ ((0. X) \ y) by A7
.= (y \ y) \ ((0. X) \ y) by A5
.= y \ y by A4 ;
hence y \ y = 0. X by A4; ::_thesis: verum
end;
A9: for x being Element of X holds (0. X) \ x = 0. X
proof
let x be Element of X; ::_thesis: (0. X) \ x = 0. X
((0. X) \ x) \ ((0. X) \ x) = (0. X) \ x by A4;
hence (0. X) \ x = 0. X by A8; ::_thesis: verum
end;
A10: for x, y being Element of X holds (x \ y) \ x = 0. X
proof
let x, y be Element of X; ::_thesis: (x \ y) \ x = 0. X
(x \ y) \ x = (x \ y) \ (x \ (0. X)) by A5
.= (((0. X) \ y) \ ((0. X) \ x)) \ (x \ (0. X)) by A4
.= ((0. X) \ ((0. X) \ x)) \ (x \ (0. X)) by A9
.= (0. X) \ (x \ (0. X)) by A9 ;
hence (x \ y) \ x = 0. X by A9; ::_thesis: verum
end;
A11: for x, y, z being Element of X holds ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X
(((y \ z) \ (y \ x)) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A10;
hence ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A4; ::_thesis: verum
end;
A12: for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ (y \ x)
proof
let x, y, z be Element of X; ::_thesis: (x \ z) \ (x \ y) = (y \ z) \ (y \ x)
( ((y \ z) \ (y \ x)) \ ((x \ z) \ (x \ y)) = 0. X & ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X ) by A11;
hence (x \ z) \ (x \ y) = (y \ z) \ (y \ x) by A6; ::_thesis: verum
end;
then A13: X is commutative BCK-algebra by A4, Th6;
for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
x \ (x \ y) = y \ (y \ x) by A13, Def1;
hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A7; ::_thesis: verum
end;
hence X is BCK-implicative BCK-algebra by A4, A12, Th6, Th35; ::_thesis: verum
end;
Lm1: for X being bounded BCK-algebra st X is BCK-implicative holds
for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x
proof
let X be bounded BCK-algebra; ::_thesis: ( X is BCK-implicative implies for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x )
assume X is BCK-implicative ; ::_thesis: for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x
then A1: X is commutative BCK-algebra by Th34;
let a be Element of X; ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x )
assume A2: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x
let x be Element of X; ::_thesis: a \ (a \ x) = x
a \ (a \ x) = x \ (x \ a) by A1, Def1
.= x \ (0. X) by A2, Def2 ;
hence a \ (a \ x) = x by BCIALG_1:2; ::_thesis: verum
end;
theorem Th37: :: BCIALG_3:37
for X being bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )
proof
let X be bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )
let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) ) )
assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )
thus ( X is BCK-implicative implies ( X is involutory & X is BCK-positive-implicative ) ) ::_thesis: ( X is involutory & X is BCK-positive-implicative implies X is BCK-implicative )
proof
assume A2: X is BCK-implicative ; ::_thesis: ( X is involutory & X is BCK-positive-implicative )
then for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x by Lm1;
hence ( X is involutory & X is BCK-positive-implicative ) by A2, Def7, Th34; ::_thesis: verum
end;
assume that
A3: X is involutory and
A4: X is BCK-positive-implicative ; ::_thesis: X is BCK-implicative
for x, y being Element of X holds x \ (y \ x) = x
proof
let x, y be Element of X; ::_thesis: x \ (y \ x) = x
y \ a = 0. X by A1, Def2;
then y <= a by BCIALG_1:def_11;
then A5: y \ x <= a \ x by BCIALG_1:5;
x \ (a \ x) = (a \ (a \ x)) \ (a \ x) by A1, A3, Def7
.= a \ (a \ x) by A4, Th28
.= x by A1, A3, Def7 ;
then x <= x \ (y \ x) by A5, BCIALG_1:5;
then A6: x \ (x \ (y \ x)) = 0. X by BCIALG_1:def_11;
(x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ (y \ x) = x by A6, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-implicative by Def12; ::_thesis: verum
end;
theorem :: BCIALG_3:38
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X )
thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ) implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X
let x, y be Element of X; ::_thesis: x \ (x \ (y \ x)) = 0. X
x \ (x \ (y \ x)) = x \ x by A1, Def12;
hence x \ (x \ (y \ x)) = 0. X by BCIALG_1:def_5; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ; ::_thesis: X is BCK-implicative BCK-algebra
for x, y being Element of X holds x \ (y \ x) = x
proof
let x, y be Element of X; ::_thesis: x \ (y \ x) = x
A3: (x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
x \ (x \ (y \ x)) = 0. X by A2;
hence x \ (y \ x) = x by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-implicative BCK-algebra by Def12; ::_thesis: verum
end;
theorem :: BCIALG_3:39
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) )
thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y)))
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y)))
X is commutative BCK-algebra by A1, Th34;
then y \ (y \ (x \ (x \ y))) = y \ (y \ (y \ (y \ x))) by Def1
.= y \ (y \ x) by BCIALG_1:8 ;
hence (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A1, Th35; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: X is BCK-implicative BCK-algebra
A3: for x, y being Element of X holds (x \ y) \ y = x \ y
proof
let x, y be Element of X; ::_thesis: (x \ y) \ y = x \ y
A4: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8
.= (x \ y) \ (0. X) by BCIALG_1:def_5
.= x \ y by BCIALG_1:2 ;
(x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:8
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
hence (x \ y) \ y = x \ y by A2, A4; ::_thesis: verum
end;
for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y)))
x \ (x \ y) = (x \ (x \ y)) \ (x \ y) by A3;
hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2; ::_thesis: verum
end;
then A5: X is commutative BCK-algebra by Th4;
for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
(x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2
.= y \ (y \ (y \ (y \ x))) by A5, Def1 ;
hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by BCIALG_1:8; ::_thesis: verum
end;
hence X is BCK-implicative BCK-algebra by Th35; ::_thesis: verum
end;
theorem Th40: :: BCIALG_3:40
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) )
thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ) implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z)
then A2: X is commutative BCK-algebra by Th34;
let x, y, z be Element of X; ::_thesis: (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z)
A3: (x \ z) \ (x \ y) = (x \ (x \ y)) \ z by BCIALG_1:7
.= (y \ (y \ x)) \ z by A2, Def1 ;
X is BCK-positive-implicative BCK-algebra by A1, Th34;
hence (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) by A3, Def11; ::_thesis: verum
end;
assume A4: for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ; ::_thesis: X is BCK-implicative BCK-algebra
A5: for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x)
(x \ (0. X)) \ (x \ y) = (y \ (0. X)) \ ((y \ x) \ (0. X)) by A4;
then (x \ (0. X)) \ (x \ y) = y \ ((y \ x) \ (0. X)) by BCIALG_1:2;
then (x \ (0. X)) \ (x \ y) = y \ (y \ x) by BCIALG_1:2;
hence x \ (x \ y) = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum
end;
for x, y being Element of X holds (y \ (y \ x)) \ (y \ x) = x \ (x \ y)
proof
let x, y be Element of X; ::_thesis: (y \ (y \ x)) \ (y \ x) = x \ (x \ y)
(x \ (y \ x)) \ (x \ y) = (y \ (y \ x)) \ ((y \ x) \ (y \ x)) by A4;
then (x \ (y \ x)) \ (x \ y) = (y \ (y \ x)) \ (0. X) by BCIALG_1:def_5;
then (x \ (y \ x)) \ (x \ y) = y \ (y \ x) by BCIALG_1:2;
then (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by BCIALG_1:7;
then (y \ (y \ x)) \ (y \ x) = y \ (y \ x) by A5;
hence (y \ (y \ x)) \ (y \ x) = x \ (x \ y) by A5; ::_thesis: verum
end;
then for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ;
hence X is BCK-implicative BCK-algebra by Th35; ::_thesis: verum
end;
theorem :: BCIALG_3:41
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) )
thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) ::_thesis: ( ( for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z))
then A2: X is BCK-positive-implicative BCK-algebra by Th34;
for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z))
proof
let x, y, z be Element of X; ::_thesis: x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z))
(x \ (0. X)) \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by A1, Th40;
then x \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2
.= (y \ z) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2 ;
then x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ x) by BCIALG_1:2
.= (y \ z) \ ((y \ x) \ z) by BCIALG_1:7 ;
hence x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) by A2, Def11; ::_thesis: verum
end;
hence for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ; ::_thesis: verum
end;
assume A3: for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ; ::_thesis: X is BCK-implicative BCK-algebra
for x, y being Element of X holds x \ (y \ x) = x
proof
let x, y be Element of X; ::_thesis: x \ (y \ x) = x
x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (x \ x)) by A3;
then x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (0. X)) by BCIALG_1:def_5;
then x \ (x \ (y \ x)) = (y \ x) \ (y \ x) by BCIALG_1:2;
then A4: x \ (x \ (y \ x)) = 0. X by BCIALG_1:def_5;
(x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ (y \ x) = x by A4, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-implicative BCK-algebra by Def12; ::_thesis: verum
end;
theorem :: BCIALG_3:42
for X being BCK-algebra holds
( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) )
proof
let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) )
thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ) implies X is BCK-implicative BCK-algebra )
proof
assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y)
then A2: X is commutative BCK-algebra by Th34;
for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y)
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = (y \ (y \ x)) \ (x \ y)
(x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, Th35;
then (y \ (y \ x)) \ (x \ y) = y \ (y \ x) by A2, Def1;
hence x \ (x \ y) = (y \ (y \ x)) \ (x \ y) by A2, Def1; ::_thesis: verum
end;
hence for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ; ::_thesis: verum
end;
assume A3: for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ; ::_thesis: X is BCK-implicative BCK-algebra
for x, y being Element of X st x <= y holds
x = y \ (y \ x)
proof
let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) )
assume x <= y ; ::_thesis: x = y \ (y \ x)
then x \ y = 0. X by BCIALG_1:def_11;
then x \ (0. X) = (y \ (y \ x)) \ (0. X) by A3;
then x \ (0. X) = y \ (y \ x) by BCIALG_1:2;
hence x = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum
end;
then A4: X is commutative BCK-algebra by Th5;
for x, y being Element of X holds x \ y = (x \ y) \ y
proof
let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y
A5: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
x \ (x \ (x \ y)) = ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by A3;
then x \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by A5, BCIALG_1:2
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
hence x \ y = (x \ y) \ y by BCIALG_1:8; ::_thesis: verum
end;
then X is BCK-positive-implicative BCK-algebra by Th28;
hence X is BCK-implicative BCK-algebra by A4, Th34; ::_thesis: verum
end;
theorem Th43: :: BCIALG_3:43
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )
proof
let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )
let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) )
assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )
thus ( X is BCK-implicative implies for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) ::_thesis: ( ( for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) implies X is BCK-implicative )
proof
assume A2: X is BCK-implicative ; ::_thesis: for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X
let x be Element of X; ::_thesis: (a \ x) \ ((a \ x) \ x) = 0. X
(a \ x) \ ((a \ x) \ x) = x \ (x \ (a \ x)) by Def1
.= x \ x by A2, Def12 ;
hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def_5; ::_thesis: verum
end;
assume A3: for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ; ::_thesis: X is BCK-implicative
for x, y being Element of X holds x \ (y \ x) = x
proof
let x, y be Element of X; ::_thesis: x \ (y \ x) = x
(a \ x) \ ((a \ x) \ x) = 0. X by A3;
then A4: x \ (x \ (a \ x)) = 0. X by Def1;
y \ a = 0. X by A1, Def2;
then y <= a by BCIALG_1:def_11;
then y \ x <= a \ x by BCIALG_1:5;
then A5: x \ (a \ x) <= x \ (y \ x) by BCIALG_1:5;
(x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7
.= (a \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ (a \ x) = x by A4, BCIALG_1:def_7;
then A6: x \ (x \ (y \ x)) = 0. X by A5, BCIALG_1:def_11;
(x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ (y \ x) = x by A6, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-implicative by Def12; ::_thesis: verum
end;
theorem :: BCIALG_3:44
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x )
proof
let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x )
let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x ) )
assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x )
thus ( X is BCK-implicative implies for x being Element of X holds x \ (a \ x) = x ) ::_thesis: ( ( for x being Element of X holds x \ (a \ x) = x ) implies X is BCK-implicative )
proof
assume A2: X is BCK-implicative ; ::_thesis: for x being Element of X holds x \ (a \ x) = x
for x being Element of X holds x \ (a \ x) = x
proof
let x be Element of X; ::_thesis: x \ (a \ x) = x
(a \ x) \ ((a \ x) \ x) = 0. X by A1, A2, Th43;
then A3: x \ (x \ (a \ x)) = 0. X by Def1;
(x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7
.= (a \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ (a \ x) = x by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence for x being Element of X holds x \ (a \ x) = x ; ::_thesis: verum
end;
assume A4: for x being Element of X holds x \ (a \ x) = x ; ::_thesis: X is BCK-implicative
for x, y being Element of X holds x \ (y \ x) = x
proof
let x, y be Element of X; ::_thesis: x \ (y \ x) = x
A5: (x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7
.= (a \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
y \ a = 0. X by A1, Def2;
then y <= a by BCIALG_1:def_11;
then y \ x <= a \ x by BCIALG_1:5;
then A6: x \ (a \ x) <= x \ (y \ x) by BCIALG_1:5;
x \ (x \ (a \ x)) = x \ x by A4
.= 0. X by BCIALG_1:def_5 ;
then x \ (a \ x) = x by A5, BCIALG_1:def_7;
then A7: x \ (x \ (y \ x)) = 0. X by A6, BCIALG_1:def_11;
(x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ (y \ x) = x by A7, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCK-implicative by Def12; ::_thesis: verum
end;
theorem :: BCIALG_3:45
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x )
proof
let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x )
let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x ) )
assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x )
thus ( X is BCK-implicative implies for x being Element of X holds (a \ x) \ x = a \ x ) ::_thesis: ( ( for x being Element of X holds (a \ x) \ x = a \ x ) implies X is BCK-implicative )
proof
assume A2: X is BCK-implicative ; ::_thesis: for x being Element of X holds (a \ x) \ x = a \ x
let x be Element of X; ::_thesis: (a \ x) \ x = a \ x
A3: ((a \ x) \ x) \ (a \ x) = ((a \ x) \ (a \ x)) \ x by BCIALG_1:7
.= x ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
(a \ x) \ ((a \ x) \ x) = 0. X by A1, A2, Th43;
hence (a \ x) \ x = a \ x by A3, BCIALG_1:def_7; ::_thesis: verum
end;
assume A4: for x being Element of X holds (a \ x) \ x = a \ x ; ::_thesis: X is BCK-implicative
let x, y be Element of X; :: according to BCIALG_3:def_12 ::_thesis: x \ (y \ x) = x
(a \ x) \ ((a \ x) \ x) = (a \ x) \ (a \ x) by A4
.= 0. X by BCIALG_1:def_5 ;
then A5: x \ (x \ (a \ x)) = 0. X by Def1;
y \ a = 0. X by A1, Def2;
then y <= a by BCIALG_1:def_11;
then y \ x <= a \ x by BCIALG_1:5;
then A6: x \ (a \ x) <= x \ (y \ x) by BCIALG_1:5;
(x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7
.= (a \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ (a \ x) = x by A5, BCIALG_1:def_7;
then A7: x \ (x \ (y \ x)) = 0. X by A6, BCIALG_1:def_11;
(x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x \ (y \ x) = x by A7, BCIALG_1:def_7; ::_thesis: verum
end;
theorem Th46: :: BCIALG_3:46
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y )
proof
let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y )
let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) )
assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y )
thus ( X is BCK-implicative implies for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) ::_thesis: ( ( for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) implies X is BCK-implicative )
proof
assume A2: X is BCK-implicative ; ::_thesis: for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y
let x, y be Element of X; ::_thesis: (a \ y) \ ((a \ y) \ x) = x \ y
X is involutory by A1, A2, Th37;
then A3: x \ (a \ y) = y \ (a \ x) by A1, Th23;
A4: (a \ y) \ ((a \ y) \ x) = x \ (x \ (a \ y)) by Def1;
(y \ (a \ x)) \ y = (y \ y) \ (a \ x) by BCIALG_1:7
.= (a \ x) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ (a \ y) <= y by A3, BCIALG_1:def_11;
then x \ y <= (a \ y) \ ((a \ y) \ x) by A4, BCIALG_1:5;
then A5: (x \ y) \ ((a \ y) \ ((a \ y) \ x)) = 0. X by BCIALG_1:def_11;
X is BCK-positive-implicative BCK-algebra by A2, Th34;
then a \ y = (a \ y) \ y by Th28;
then ((a \ y) \ ((a \ y) \ x)) \ (x \ y) = 0. X by BCIALG_1:1;
hence (a \ y) \ ((a \ y) \ x) = x \ y by A5, BCIALG_1:def_7; ::_thesis: verum
end;
assume A6: for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ; ::_thesis: X is BCK-implicative
for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X
proof
let x be Element of X; ::_thesis: (a \ x) \ ((a \ x) \ x) = 0. X
(a \ x) \ ((a \ x) \ x) = x \ x by A6;
hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def_5; ::_thesis: verum
end;
hence X is BCK-implicative by A1, Th43; ::_thesis: verum
end;
theorem Th47: :: BCIALG_3:47
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) )
proof
let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) )
let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) )
assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) )
thus ( X is BCK-implicative implies for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) ::_thesis: ( ( for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) implies X is BCK-implicative )
proof
assume A2: X is BCK-implicative ; ::_thesis: for x, y being Element of X holds y \ (y \ x) = x \ (a \ y)
let x, y be Element of X; ::_thesis: y \ (y \ x) = x \ (a \ y)
y \ (y \ x) = x \ (x \ y) by Def1
.= x \ ((a \ y) \ ((a \ y) \ x)) by A1, A2, Th46
.= x \ (x \ (x \ (a \ y))) by Def1 ;
hence y \ (y \ x) = x \ (a \ y) by BCIALG_1:8; ::_thesis: verum
end;
assume A3: for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ; ::_thesis: X is BCK-implicative
for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y
proof
let x, y be Element of X; ::_thesis: (a \ y) \ ((a \ y) \ x) = x \ y
(a \ y) \ ((a \ y) \ x) = x \ (a \ (a \ y)) by A3
.= x \ (y \ (y \ a)) by Def1
.= x \ (y \ (0. X)) by A1, Def2 ;
hence (a \ y) \ ((a \ y) \ x) = x \ y by BCIALG_1:2; ::_thesis: verum
end;
hence X is BCK-implicative by A1, Th46; ::_thesis: verum
end;
theorem :: BCIALG_3:48
for X being commutative bounded BCK-algebra
for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
proof
let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) )
assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
thus ( X is BCK-implicative implies for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) implies X is BCK-implicative )
proof
assume A2: X is BCK-implicative ; ::_thesis: for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z)
let x, y, z be Element of X; ::_thesis: (x \ (y \ z)) \ (x \ y) <= x \ (a \ z)
X is BCK-positive-implicative BCK-algebra by A2, Th34;
then A3: ((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ y) \ z) = ((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ z) \ (y \ z)) by Def11
.= 0. X by BCIALG_1:1 ;
((x \ y) \ z) \ (x \ y) = ((x \ y) \ (x \ y)) \ z by BCIALG_1:7
.= z ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then A4: ((x \ (y \ z)) \ (x \ (x \ z))) \ (x \ y) = 0. X by A3, BCIALG_1:3;
((x \ (y \ z)) \ (x \ y)) \ (x \ (a \ z)) = ((x \ (y \ z)) \ (x \ y)) \ (z \ (z \ x)) by A1, A2, Th47
.= ((x \ (y \ z)) \ (x \ y)) \ (x \ (x \ z)) by Def1
.= 0. X by A4, BCIALG_1:7 ;
hence (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) by BCIALG_1:def_11; ::_thesis: verum
end;
assume A5: for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ; ::_thesis: X is BCK-implicative
for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X
proof
let x be Element of X; ::_thesis: (a \ x) \ ((a \ x) \ x) = 0. X
(x \ (x \ x)) \ (x \ x) <= x \ (a \ x) by A5;
then (x \ (0. X)) \ (x \ x) <= x \ (a \ x) by BCIALG_1:def_5;
then x \ (x \ x) <= x \ (a \ x) by BCIALG_1:2;
then x \ (0. X) <= x \ (a \ x) by BCIALG_1:def_5;
then x <= x \ (a \ x) by BCIALG_1:2;
then x \ (x \ (a \ x)) = 0. X by BCIALG_1:def_11;
hence (a \ x) \ ((a \ x) \ x) = 0. X by Def1; ::_thesis: verum
end;
hence X is BCK-implicative by A1, Th43; ::_thesis: verum
end;