:: BCIALG_4 semantic presentation
begin
definition
attrc1 is strict ;
struct BCIStr_1 -> BCIStr_0 , ZeroStr ;
aggrBCIStr_1(# carrier, ExternalDiff, InternalDiff, ZeroF #) -> BCIStr_1 ;
sel ExternalDiff c1 -> BinOp of the carrier of c1;
end;
registration
cluster non empty strict for BCIStr_1 ;
existence
ex b1 being BCIStr_1 st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set m = the BinOp of the non empty set ;
set u = the Element of the non empty set ;
take BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) ; ::_thesis: ( not BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty & BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict )
thus not the carrier of BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict
thus BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict ; ::_thesis: verum
end;
end;
definition
let A be BCIStr_1 ;
let x, y be Element of A;
funcx * y -> Element of A equals :: BCIALG_4:def 1
the ExternalDiff of A . (x,y);
coherence
the ExternalDiff of A . (x,y) is Element of A ;
end;
:: deftheorem defines * BCIALG_4:def_1_:_
for A being BCIStr_1
for x, y being Element of A holds x * y = the ExternalDiff of A . (x,y);
definition
let IT be non empty BCIStr_1 ;
attrIT is with_condition_S means :Def2: :: BCIALG_4:def 2
for x, y, z being Element of IT holds (x \ y) \ z = x \ (y * z);
end;
:: deftheorem Def2 defines with_condition_S BCIALG_4:def_2_:_
for IT being non empty BCIStr_1 holds
( IT is with_condition_S iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y * z) );
definition
func BCI_S-EXAMPLE -> BCIStr_1 equals :: BCIALG_4:def 3
BCIStr_1(# 1,op2,op2,op0 #);
coherence
BCIStr_1(# 1,op2,op2,op0 #) is BCIStr_1 ;
end;
:: deftheorem defines BCI_S-EXAMPLE BCIALG_4:def_3_:_
BCI_S-EXAMPLE = BCIStr_1(# 1,op2,op2,op0 #);
registration
cluster BCI_S-EXAMPLE -> 1 -element strict ;
coherence
( BCI_S-EXAMPLE is strict & BCI_S-EXAMPLE is 1 -element ) by STRUCT_0:def_19, CARD_1:49;
end;
Lm1: ( BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )
proof
thus BCI_S-EXAMPLE is being_B ::_thesis: ( BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )
proof
let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_3 ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI_S-EXAMPLE
thus ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI_S-EXAMPLE is being_C ::_thesis: ( BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )
proof
let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_4 ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI_S-EXAMPLE
thus ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI_S-EXAMPLE is being_I ::_thesis: ( BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )
proof
let x be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_5 ::_thesis: x \ x = 0. BCI_S-EXAMPLE
thus x \ x = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI_S-EXAMPLE is being_BCI-4 ::_thesis: ( BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )
proof
let x, y be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_7 ::_thesis: ( not x \ y = 0. BCI_S-EXAMPLE or not y \ x = 0. BCI_S-EXAMPLE or x = y )
thus ( not x \ y = 0. BCI_S-EXAMPLE or not y \ x = 0. BCI_S-EXAMPLE or x = y ) by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI_S-EXAMPLE is being_BCK-5 ::_thesis: BCI_S-EXAMPLE is with_condition_S
proof
let x be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_8 ::_thesis: x ` = 0. BCI_S-EXAMPLE
thus x ` = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_2 ::_thesis: (x \ y) \ z = x \ (y * z)
thus (x \ y) \ z = x \ (y * z) by STRUCT_0:def_10; ::_thesis: verum
end;
registration
cluster BCI_S-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ;
coherence
( BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S ) by Lm1;
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 strict with_condition_S for BCIStr_1 ;
existence
ex b1 being non empty BCIStr_1 st
( b1 is strict & b1 is being_B & b1 is being_C & b1 is being_I & b1 is being_BCI-4 & b1 is with_condition_S ) by Lm1;
end;
definition
mode BCI-Algebra_with_Condition(S) is non empty being_B being_C being_I being_BCI-4 with_condition_S BCIStr_1 ;
end;
definition
let X be BCI-Algebra_with_Condition(S);
let x, y be Element of X;
func Condition_S (x,y) -> non empty Subset of X equals :: BCIALG_4:def 4
{ t where t is Element of X : t \ x <= y } ;
coherence
{ t where t is Element of X : t \ x <= y } is non empty Subset of X
proof
set a = (0. X) \ (((0. X) \ x) \ y);
set Y = { t where t is Element of X : t \ x <= y } ;
A1: now__::_thesis:_for_y1_being_set_st_y1_in__{__t_where_t_is_Element_of_X_:_t_\_x_<=_y__}__holds_
y1_in_the_carrier_of_X
let y1 be set ; ::_thesis: ( y1 in { t where t is Element of X : t \ x <= y } implies y1 in the carrier of X )
assume y1 in { t where t is Element of X : t \ x <= y } ; ::_thesis: y1 in the carrier of X
then ex x1 being Element of X st
( y1 = x1 & x1 \ x <= y ) ;
hence y1 in the carrier of X ; ::_thesis: verum
end;
(((0. X) \ (((0. X) \ x) \ y)) \ x) \ y = (((0. X) \ x) \ (((0. X) \ x) \ y)) \ y by BCIALG_1:7
.= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ y by BCIALG_1:2
.= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ (y \ (0. X)) by BCIALG_1:2
.= 0. X by BCIALG_1:1 ;
then ((0. X) \ (((0. X) \ x) \ y)) \ x <= y by BCIALG_1:def_11;
then (0. X) \ (((0. X) \ x) \ y) in { t where t is Element of X : t \ x <= y } ;
hence { t where t is Element of X : t \ x <= y } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines Condition_S BCIALG_4:def_4_:_
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds Condition_S (x,y) = { t where t is Element of X : t \ x <= y } ;
theorem :: BCIALG_4:1
for X being BCI-Algebra_with_Condition(S)
for x, y, u, v being Element of X st u in Condition_S (x,y) & v <= u holds
v in Condition_S (x,y)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, u, v being Element of X st u in Condition_S (x,y) & v <= u holds
v in Condition_S (x,y)
let x, y, u, v be Element of X; ::_thesis: ( u in Condition_S (x,y) & v <= u implies v in Condition_S (x,y) )
assume that
A1: u in Condition_S (x,y) and
A2: v <= u ; ::_thesis: v in Condition_S (x,y)
v \ x <= u \ x by A2, BCIALG_1:5;
then A3: (v \ x) \ (u \ x) = 0. X by BCIALG_1:def_11;
ex u1 being Element of X st
( u = u1 & u1 \ x <= y ) by A1;
then (u \ x) \ y = 0. X by BCIALG_1:def_11;
then (v \ x) \ y = 0. X by A3, BCIALG_1:3;
then v \ x <= y by BCIALG_1:def_11;
hence v in Condition_S (x,y) ; ::_thesis: verum
end;
theorem :: BCIALG_4:2
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
let x, y be Element of X; ::_thesis: ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
((x * y) \ x) \ y = (x * y) \ (x * y) by Def2
.= 0. X by BCIALG_1:def_5 ;
then (x * y) \ x <= y by BCIALG_1:def_11;
then x * y in { t where t is Element of X : t \ x <= y } ;
then consider u being Element of Condition_S (x,y) such that
A1: u = x * y ;
take u ; ::_thesis: for z being Element of Condition_S (x,y) holds z <= u
for z being Element of Condition_S (x,y) holds z <= u
proof
let z be Element of Condition_S (x,y); ::_thesis: z <= u
z in { t where t is Element of X : t \ x <= y } ;
then consider z1 being Element of X such that
A2: z = z1 and
A3: z1 \ x <= y ;
z \ u = (z1 \ x) \ y by A1, A2, Def2
.= 0. X by A3, BCIALG_1:def_11 ;
hence z <= u by BCIALG_1:def_11; ::_thesis: verum
end;
hence for z being Element of Condition_S (x,y) holds z <= u ; ::_thesis: verum
end;
Lm2: for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) )
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) )
let x, y be Element of X; ::_thesis: ( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) )
A1: for t being Element of X st t \ x <= y holds
t <= x * y
proof
let t be Element of X; ::_thesis: ( t \ x <= y implies t <= x * y )
assume A2: t \ x <= y ; ::_thesis: t <= x * y
t \ (x * y) = (t \ x) \ y by Def2
.= 0. X by A2, BCIALG_1:def_11 ;
hence t <= x * y by BCIALG_1:def_11; ::_thesis: verum
end;
((x * y) \ x) \ y = (x * y) \ (x * y) by Def2
.= 0. X by BCIALG_1:def_5 ;
hence ( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) by A1, BCIALG_1:def_11; ::_thesis: verum
end;
Lm3: for X being non empty BCIStr_1 st X is BCI-algebra & ( for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) holds
X is BCI-Algebra_with_Condition(S)
proof
let X be non empty BCIStr_1 ; ::_thesis: ( X is BCI-algebra & ( for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) implies X is BCI-Algebra_with_Condition(S) )
assume that
A1: X is BCI-algebra and
A2: for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ; ::_thesis: X is BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = x \ (y * z)
(y * z) \ y <= z by A2;
then A3: ((y * z) \ y) \ z = 0. X by BCIALG_1:def_11;
(x \ ((x \ y) \ z)) \ y = (x \ y) \ ((x \ y) \ z) by A1, BCIALG_1:7
.= ((x \ y) \ (0. X)) \ ((x \ y) \ z) by A1, BCIALG_1:2 ;
then ((x \ ((x \ y) \ z)) \ y) \ (z \ (0. X)) = 0. X by A1, BCIALG_1:11;
then (x \ ((x \ y) \ z)) \ y <= z \ (0. X) by BCIALG_1:def_11;
then (x \ ((x \ y) \ z)) \ y <= z by A1, BCIALG_1:2;
then x \ ((x \ y) \ z) <= y * z by A2;
then (x \ ((x \ y) \ z)) \ (y * z) = 0. X by BCIALG_1:def_11;
then A4: (x \ (y * z)) \ ((x \ y) \ z) = 0. X by A1, BCIALG_1:7;
((x \ y) \ (x \ (y * z))) \ ((y * z) \ y) = 0. X by A1, BCIALG_1:11;
then ((x \ y) \ (x \ (y * z))) \ z = 0. X by A1, A3, BCIALG_1:3;
then ((x \ y) \ z) \ (x \ (y * z)) = 0. X by A1, BCIALG_1:7;
hence (x \ y) \ z = x \ (y * z) by A1, A4, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is BCI-Algebra_with_Condition(S) by A1, Def2; ::_thesis: verum
end;
theorem :: BCIALG_4:3
for X being non empty BCIStr_1 holds
( ( X is BCI-algebra & ( for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) ) iff X is BCI-Algebra_with_Condition(S) ) by Lm2, Lm3;
theorem :: BCIALG_4:4
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
let x, y be Element of X; ::_thesis: ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
proof
(x * y) \ x <= y by Lm2;
then x * y in Condition_S (x,y) ;
then consider a being Element of Condition_S (x,y) such that
A1: a = x * y ;
take a ; ::_thesis: for z being Element of Condition_S (x,y) holds z <= a
for t1 being Element of Condition_S (x,y) holds t1 <= a
proof
let t1 be Element of Condition_S (x,y); ::_thesis: t1 <= a
t1 in { t where t is Element of X : t \ x <= y } ;
then ex t2 being Element of X st
( t2 = t1 & t2 \ x <= y ) ;
hence t1 <= a by A1, Lm2; ::_thesis: verum
end;
hence for z being Element of Condition_S (x,y) holds z <= a ; ::_thesis: verum
end;
hence ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a ; ::_thesis: verum
end;
definition
let X be p-Semisimple BCI-algebra;
func Adjoint_pGroup X -> strict AbGroup means :: BCIALG_4:def 5
( the carrier of it = the carrier of X & ( for x, y being Element of X holds the addF of it . (x,y) = x \ ((0. X) \ y) ) & 0. it = 0. X );
existence
ex b1 being strict AbGroup st
( the carrier of b1 = the carrier of X & ( for x, y being Element of X holds the addF of b1 . (x,y) = x \ ((0. X) \ y) ) & 0. b1 = 0. X )
proof
reconsider A0 = 0. X as Element of X ;
defpred S1[ Element of X, Element of X, Element of X] means ex x, y being Element of X st
( $1 = x & $2 = y & $3 = x \ ((0. X) \ y) );
A1: for a, b being Element of X ex c being Element of X st S1[a,b,c]
proof
let a, b be Element of X; ::_thesis: ex c being Element of X st S1[a,b,c]
reconsider x = a, y = b as Element of X ;
reconsider c = x \ ((0. X) \ y) as Element of X ;
take c ; ::_thesis: S1[a,b,c]
thus S1[a,b,c] ; ::_thesis: verum
end;
consider h being BinOp of the carrier of X such that
A2: for a, b being Element of X holds S1[a,b,h . (a,b)] from BINOP_1:sch_3(A1);
set G = addLoopStr(# the carrier of X,h,A0 #);
A3: for x, y being Element of X holds h . (x,y) = x \ ((0. X) \ y)
proof
let x, y be Element of X; ::_thesis: h . (x,y) = x \ ((0. X) \ y)
ex x9, y9 being Element of X st
( x = x9 & y = y9 & h . (x,y) = x9 \ ((0. X) \ y9) ) by A2;
hence h . (x,y) = x \ ((0. X) \ y) ; ::_thesis: verum
end;
A4: for a being Element of X ex b, x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )
proof
let a be Element of X; ::_thesis: ex b, x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )
reconsider x = a as Element of X ;
reconsider b = (0. X) \ x as Element of X ;
A5: b \ ((0. X) \ x) = 0. X by BCIALG_1:def_5;
take b ; ::_thesis: ex x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X )
x \ ((0. X) \ b) = x \ ((x `) `)
.= x \ x by BCIALG_1:54
.= 0. X by BCIALG_1:def_5 ;
hence ex x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) by A5; ::_thesis: verum
end;
( addLoopStr(# the carrier of X,h,A0 #) is Abelian & addLoopStr(# the carrier of X,h,A0 #) is add-associative & addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable )
proof
thus addLoopStr(# the carrier of X,h,A0 #) is Abelian ::_thesis: ( addLoopStr(# the carrier of X,h,A0 #) is add-associative & addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable )
proof
let a, b be Element of addLoopStr(# the carrier of X,h,A0 #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a
reconsider x = a, y = b as Element of X ;
thus a + b = x \ ((0. X) \ y) by A3
.= y \ ((0. X) \ x) by BCIALG_1:57
.= b + a by A3 ; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_3 ::_thesis: ( addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable )
let a, b, c be Element of addLoopStr(# the carrier of X,h,A0 #); ::_thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of X ;
thus (a + b) + c = h . ((x \ ((0. X) \ y)),z) by A3
.= (x \ ((0. X) \ y)) \ ((0. X) \ z) by A3
.= (y \ ((0. X) \ x)) \ ((0. X) \ z) by BCIALG_1:57
.= (y \ ((0. X) \ z)) \ ((0. X) \ x) by BCIALG_1:7
.= x \ ((0. X) \ (y \ ((0. X) \ z))) by BCIALG_1:57
.= h . (x,(y \ ((0. X) \ z))) by A3
.= a + (b + c) by A3 ; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_4 ::_thesis: addLoopStr(# the carrier of X,h,A0 #) is right_complementable
let a be Element of addLoopStr(# the carrier of X,h,A0 #); ::_thesis: a + (0. addLoopStr(# the carrier of X,h,A0 #)) = a
reconsider x = a as Element of X ;
thus a + (0. addLoopStr(# the carrier of X,h,A0 #)) = x \ ((0. X) \ (0. X)) by A3
.= x \ (0. X) by BCIALG_1:2
.= a by BCIALG_1:2 ; ::_thesis: verum
end;
let a be Element of addLoopStr(# the carrier of X,h,A0 #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
consider b being Element of X such that
A6: ex x being Element of X st
( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) by A4;
reconsider b = b as Element of addLoopStr(# the carrier of X,h,A0 #) ;
take b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. addLoopStr(# the carrier of X,h,A0 #)
thus a + b = 0. addLoopStr(# the carrier of X,h,A0 #) by A3, A6; ::_thesis: verum
end;
then reconsider G = addLoopStr(# the carrier of X,h,A0 #) as strict AbGroup ;
take G ; ::_thesis: ( the carrier of G = the carrier of X & ( for x, y being Element of X holds the addF of G . (x,y) = x \ ((0. X) \ y) ) & 0. G = 0. X )
thus ( the carrier of G = the carrier of X & ( for x, y being Element of X holds the addF of G . (x,y) = x \ ((0. X) \ y) ) & 0. G = 0. X ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict AbGroup st the carrier of b1 = the carrier of X & ( for x, y being Element of X holds the addF of b1 . (x,y) = x \ ((0. X) \ y) ) & 0. b1 = 0. X & the carrier of b2 = the carrier of X & ( for x, y being Element of X holds the addF of b2 . (x,y) = x \ ((0. X) \ y) ) & 0. b2 = 0. X holds
b1 = b2
proof
thus for G1, G2 being strict AbGroup st the carrier of G1 = the carrier of X & ( for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) ) & 0. G1 = 0. X & the carrier of G2 = the carrier of X & ( for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) ) & 0. G2 = 0. X holds
G1 = G2 ::_thesis: verum
proof
let G1, G2 be strict AbGroup; ::_thesis: ( the carrier of G1 = the carrier of X & ( for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) ) & 0. G1 = 0. X & the carrier of G2 = the carrier of X & ( for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) ) & 0. G2 = 0. X implies G1 = G2 )
assume that
A7: the carrier of G1 = the carrier of X and
A8: for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) and
A9: ( 0. G1 = 0. X & the carrier of G2 = the carrier of X ) and
A10: for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) and
A11: 0. G2 = 0. X ; ::_thesis: G1 = G2
now__::_thesis:_for_a,_b_being_Element_of_G1_holds_the_addF_of_G1_._(a,b)_=_the_addF_of_G2_._(a,b)
let a, b be Element of G1; ::_thesis: the addF of G1 . (a,b) = the addF of G2 . (a,b)
reconsider x = a, y = b as Element of X by A7;
thus the addF of G1 . (a,b) = x \ ((0. X) \ y) by A8
.= the addF of G2 . (a,b) by A10 ; ::_thesis: verum
end;
hence G1 = G2 by A7, A9, A11, BINOP_1:2; ::_thesis: verum
end;
end;
end;
:: deftheorem defines Adjoint_pGroup BCIALG_4:def_5_:_
for X being p-Semisimple BCI-algebra
for b2 being strict AbGroup holds
( b2 = Adjoint_pGroup X iff ( the carrier of b2 = the carrier of X & ( for x, y being Element of X holds the addF of b2 . (x,y) = x \ ((0. X) \ y) ) & 0. b2 = 0. X ) );
theorem Th5: :: BCIALG_4:5
for X being BCI-algebra holds
( X is p-Semisimple iff for x, y being Element of X st x \ y = 0. X holds
x = y )
proof
let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y being Element of X st x \ y = 0. X holds
x = y )
thus ( X is p-Semisimple implies for x, y being Element of X st x \ y = 0. X holds
x = y ) ::_thesis: ( ( for x, y being Element of X st x \ y = 0. X holds
x = y ) implies X is p-Semisimple )
proof
assume A1: X is p-Semisimple ; ::_thesis: for x, y being Element of X st x \ y = 0. X holds
x = y
for x, y being Element of X st x \ y = 0. X holds
x = y
proof
let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y )
assume A2: x \ y = 0. X ; ::_thesis: x = y
(0. X) \ (x \ y) = (y \ x) \ ((0. X) `) by A1, BCIALG_1:66
.= (y \ x) \ (0. X) by BCIALG_1:def_5
.= y \ x by BCIALG_1:2 ;
then y \ x = 0. X by A2, BCIALG_1:def_5;
hence x = y by A2, BCIALG_1:def_7; ::_thesis: verum
end;
hence for x, y being Element of X st x \ y = 0. X holds
x = y ; ::_thesis: verum
end;
assume A3: for x, y being Element of X st x \ y = 0. X holds
x = y ; ::_thesis: X is p-Semisimple
for x, y being Element of X holds x \ (x \ y) = y
proof
let x, y be Element of X; ::_thesis: x \ (x \ y) = y
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
hence x \ (x \ y) = y by A3; ::_thesis: verum
end;
hence X is p-Semisimple by BCIALG_1:def_26; ::_thesis: verum
end;
theorem :: BCIALG_4:6
for X being BCI-Algebra_with_Condition(S) st X is p-Semisimple holds
for x, y being Element of X holds x * y = x \ ((0. X) \ y)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: ( X is p-Semisimple implies for x, y being Element of X holds x * y = x \ ((0. X) \ y) )
assume A1: X is p-Semisimple ; ::_thesis: for x, y being Element of X holds x * y = x \ ((0. X) \ y)
for x, y being Element of X holds x * y = x \ ((0. X) \ y)
proof
let x, y be Element of X; ::_thesis: x * y = x \ ((0. X) \ y)
set z1 = x \ ((0. X) \ y);
set z2 = x * y;
((x \ ((0. X) \ y)) \ x) \ y = ((x \ x) \ ((0. X) \ y)) \ y by BCIALG_1:7
.= ((0. X) \ ((0. X) \ y)) \ y by BCIALG_1:def_5
.= ((0. X) \ y) \ ((0. X) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
then (x \ ((0. X) \ y)) \ x <= y by BCIALG_1:def_11;
then x \ ((0. X) \ y) <= x * y by Lm2;
then A2: (x \ ((0. X) \ y)) \ (x * y) = 0. X by BCIALG_1:def_11;
A3: for t being Element of X st t \ x <= y holds
t <= x \ ((0. X) \ y)
proof
let t be Element of X; ::_thesis: ( t \ x <= y implies t <= x \ ((0. X) \ y) )
assume t \ x <= y ; ::_thesis: t <= x \ ((0. X) \ y)
then (t \ x) \ y = 0. X by BCIALG_1:def_11;
then t \ (x \ ((0. X) \ y)) = t \ (x \ ((0. X) \ (t \ x))) by A1, Th5
.= t \ (x \ (x \ (t \ (0. X)))) by A1, BCIALG_1:57
.= t \ (t \ (0. X)) by A1, BCIALG_1:61
.= t \ t by BCIALG_1:2
.= 0. X by BCIALG_1:def_5 ;
hence t <= x \ ((0. X) \ y) by BCIALG_1:def_11; ::_thesis: verum
end;
(x * y) \ x <= y by Lm2;
then x * y <= x \ ((0. X) \ y) by A3;
then (x * y) \ (x \ ((0. X) \ y)) = 0. X by BCIALG_1:def_11;
hence x * y = x \ ((0. X) \ y) by A2, BCIALG_1:def_7; ::_thesis: verum
end;
hence for x, y being Element of X holds x * y = x \ ((0. X) \ y) ; ::_thesis: verum
end;
theorem Th7: :: BCIALG_4:7
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds x * y = y * x
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds x * y = y * x
let x, y be Element of X; ::_thesis: x * y = y * x
(y * x) \ y <= x by Lm2;
then ((y * x) \ y) \ x = 0. X by BCIALG_1:def_11;
then ((y * x) \ x) \ y = 0. X by BCIALG_1:7;
then (y * x) \ x <= y by BCIALG_1:def_11;
then y * x <= x * y by Lm2;
then A1: (y * x) \ (x * y) = 0. X by BCIALG_1:def_11;
(x * y) \ x <= y by Lm2;
then ((x * y) \ x) \ y = 0. X by BCIALG_1:def_11;
then ((x * y) \ y) \ x = 0. X by BCIALG_1:7;
then (x * y) \ y <= x by BCIALG_1:def_11;
then x * y <= y * x by Lm2;
then (x * y) \ (y * x) = 0. X by BCIALG_1:def_11;
hence x * y = y * x by A1, BCIALG_1:def_7; ::_thesis: verum
end;
theorem Th8: :: BCIALG_4:8
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X st x <= y holds
( x * z <= y * z & z * x <= z * y )
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X st x <= y holds
( x * z <= y * z & z * x <= z * y )
let x, y, z be Element of X; ::_thesis: ( x <= y implies ( x * z <= y * z & z * x <= z * y ) )
assume x <= y ; ::_thesis: ( x * z <= y * z & z * x <= z * y )
then (x * z) \ y <= (x * z) \ x by BCIALG_1:5;
then A1: ((x * z) \ y) \ ((x * z) \ x) = 0. X by BCIALG_1:def_11;
(x * z) \ x <= z by Lm2;
then ((x * z) \ x) \ z = 0. X by BCIALG_1:def_11;
then ((x * z) \ y) \ z = 0. X by A1, BCIALG_1:3;
then A2: (x * z) \ y <= z by BCIALG_1:def_11;
( x * z = z * x & y * z = z * y ) by Th7;
hence ( x * z <= y * z & z * x <= z * y ) by A2, Lm2; ::_thesis: verum
end;
theorem Th9: :: BCIALG_4:9
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds
( (0. X) * x = x & x * (0. X) = x )
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds
( (0. X) * x = x & x * (0. X) = x )
let x be Element of X; ::_thesis: ( (0. X) * x = x & x * (0. X) = x )
(x \ (0. X)) \ x = (x \ x) \ (0. X) by BCIALG_1:7
.= (0. X) \ (0. X) by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_5 ;
then x \ (0. X) <= x by BCIALG_1:def_11;
then x <= (0. X) * x by Lm2;
then A1: x \ ((0. X) * x) = 0. X by BCIALG_1:def_11;
((0. X) * x) \ (0. X) <= x by Lm2;
then (0. X) * x <= x by BCIALG_1:2;
then ((0. X) * x) \ x = 0. X by BCIALG_1:def_11;
then (0. X) * x = x by A1, BCIALG_1:def_7;
hence ( (0. X) * x = x & x * (0. X) = x ) by Th7; ::_thesis: verum
end;
theorem Th10: :: BCIALG_4:10
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds (x * y) * z = x * (y * z)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x * y) * z = x * (y * z)
let x, y, z be Element of X; ::_thesis: (x * y) * z = x * (y * z)
A1: (z * (x * y)) \ z <= x * y by Lm2;
(((x * y) * z) \ x) \ z = (((x * y) * z) \ z) \ x by BCIALG_1:7
.= ((z * (x * y)) \ z) \ x by Th7 ;
then (((x * y) * z) \ x) \ z <= (x * y) \ x by A1, BCIALG_1:5;
then A2: ((((x * y) * z) \ x) \ z) \ ((x * y) \ x) = 0. X by BCIALG_1:def_11;
A3: (x * (z * y)) \ x <= z * y by Lm2;
(((z * y) * x) \ z) \ x = (((z * y) * x) \ x) \ z by BCIALG_1:7
.= ((x * (z * y)) \ x) \ z by Th7 ;
then (((z * y) * x) \ z) \ x <= (z * y) \ z by A3, BCIALG_1:5;
then A4: ((((z * y) * x) \ z) \ x) \ ((z * y) \ z) = 0. X by BCIALG_1:def_11;
(z * y) \ z <= y by Lm2;
then ((z * y) \ z) \ y = 0. X by BCIALG_1:def_11;
then ((((z * y) * x) \ z) \ x) \ y = 0. X by A4, BCIALG_1:3;
then (((z * y) * x) \ z) \ x <= y by BCIALG_1:def_11;
then ((z * y) * x) \ z <= x * y by Lm2;
then (z * y) * x <= z * (x * y) by Lm2;
then (y * z) * x <= z * (x * y) by Th7;
then x * (y * z) <= z * (x * y) by Th7;
then x * (y * z) <= (x * y) * z by Th7;
then A5: (x * (y * z)) \ ((x * y) * z) = 0. X by BCIALG_1:def_11;
(x * y) \ x <= y by Lm2;
then ((x * y) \ x) \ y = 0. X by BCIALG_1:def_11;
then ((((x * y) * z) \ x) \ z) \ y = 0. X by A2, BCIALG_1:3;
then (((x * y) * z) \ x) \ z <= y by BCIALG_1:def_11;
then ((x * y) * z) \ x <= z * y by Lm2;
then (x * y) * z <= x * (z * y) by Lm2;
then (x * y) * z <= x * (y * z) by Th7;
then ((x * y) * z) \ (x * (y * z)) = 0. X by BCIALG_1:def_11;
hence (x * y) * z = x * (y * z) by A5, BCIALG_1:def_7; ::_thesis: verum
end;
theorem Th11: :: BCIALG_4:11
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds (x * y) * z = (x * z) * y
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x * y) * z = (x * z) * y
let x, y, z be Element of X; ::_thesis: (x * y) * z = (x * z) * y
(x * y) * z = x * (y * z) by Th10
.= (y * z) * x by Th7
.= y * (z * x) by Th10
.= (z * x) * y by Th7 ;
hence (x * y) * z = (x * z) * y by Th7; ::_thesis: verum
end;
theorem Th12: :: BCIALG_4:12
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = x \ (y * z)
(x \ ((x \ y) \ z)) \ y = (x \ y) \ ((x \ y) \ z) by BCIALG_1:7
.= ((x \ y) \ (0. X)) \ ((x \ y) \ z) by BCIALG_1:2 ;
then ((x \ ((x \ y) \ z)) \ y) \ (z \ (0. X)) = 0. X by BCIALG_1:11;
then (x \ ((x \ y) \ z)) \ y <= z \ (0. X) by BCIALG_1:def_11;
then (x \ ((x \ y) \ z)) \ y <= z by BCIALG_1:2;
then x \ ((x \ y) \ z) <= y * z by Lm2;
then (x \ ((x \ y) \ z)) \ (y * z) = 0. X by BCIALG_1:def_11;
then A1: (x \ (y * z)) \ ((x \ y) \ z) = 0. X by BCIALG_1:7;
(y * z) \ y <= z by Lm2;
then ( ((x \ y) \ (x \ (y * z))) \ ((y * z) \ y) = 0. X & ((y * z) \ y) \ z = 0. X ) by BCIALG_1:11, BCIALG_1:def_11;
then ((x \ y) \ (x \ (y * z))) \ z = 0. X by BCIALG_1:3;
then ((x \ y) \ z) \ (x \ (y * z)) = 0. X by BCIALG_1:7;
hence (x \ y) \ z = x \ (y * z) by A1, BCIALG_1:def_7; ::_thesis: verum
end;
theorem Th13: :: BCIALG_4:13
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds y <= x * (y \ x)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds y <= x * (y \ x)
let x, y be Element of X; ::_thesis: y <= x * (y \ x)
(y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5;
then y \ x <= y \ x by BCIALG_1:def_11;
hence y <= x * (y \ x) by Lm2; ::_thesis: verum
end;
theorem :: BCIALG_4:14
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds (x * z) \ (y * z) <= x \ y
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x * z) \ (y * z) <= x \ y
let x, y, z be Element of X; ::_thesis: (x * z) \ (y * z) <= x \ y
x <= y * (x \ y) by Th13;
then x * z <= (y * (x \ y)) * z by Th8;
then x * z <= (y * z) * (x \ y) by Th11;
then (x * z) \ (y * z) <= ((y * z) * (x \ y)) \ (y * z) by BCIALG_1:5;
then A1: ((x * z) \ (y * z)) \ (((y * z) * (x \ y)) \ (y * z)) = 0. X by BCIALG_1:def_11;
((y * z) * (x \ y)) \ (y * z) <= x \ y by Lm2;
then (((y * z) * (x \ y)) \ (y * z)) \ (x \ y) = 0. X by BCIALG_1:def_11;
then ((x * z) \ (y * z)) \ (x \ y) = 0. X by A1, BCIALG_1:3;
hence (x * z) \ (y * z) <= x \ y by BCIALG_1:def_11; ::_thesis: verum
end;
theorem :: BCIALG_4:15
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds
( x \ y <= z iff x <= y * z )
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds
( x \ y <= z iff x <= y * z )
A1: for x, y, z being Element of X st x <= y * z holds
x \ y <= z
proof
let x, y, z be Element of X; ::_thesis: ( x <= y * z implies x \ y <= z )
assume x <= y * z ; ::_thesis: x \ y <= z
then x \ (y * z) = 0. X by BCIALG_1:def_11;
then (x \ y) \ z = 0. X by Th12;
hence x \ y <= z by BCIALG_1:def_11; ::_thesis: verum
end;
for x, y, z being Element of X st x \ y <= z holds
x <= y * z
proof
let x, y, z be Element of X; ::_thesis: ( x \ y <= z implies x <= y * z )
assume x \ y <= z ; ::_thesis: x <= y * z
then (x \ y) \ z = 0. X by BCIALG_1:def_11;
then x \ (y * z) = 0. X by Th12;
hence x <= y * z by BCIALG_1:def_11; ::_thesis: verum
end;
hence for x, y, z being Element of X holds
( x \ y <= z iff x <= y * z ) by A1; ::_thesis: verum
end;
theorem :: BCIALG_4:16
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds x \ y <= (x \ z) * (z \ y)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds x \ y <= (x \ z) * (z \ y)
let x, y, z be Element of X; ::_thesis: x \ y <= (x \ z) * (z \ y)
((x \ y) \ (x \ z)) \ (z \ y) = 0. X by BCIALG_1:11;
then (x \ y) \ ((x \ z) * (z \ y)) = 0. X by Th12;
hence x \ y <= (x \ z) * (z \ y) by BCIALG_1:def_11; ::_thesis: verum
end;
Lm4: for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is commutative
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: the ExternalDiff of X is commutative
now__::_thesis:_for_a,_b_being_Element_of_X_holds_the_ExternalDiff_of_X_._(a,b)_=_the_ExternalDiff_of_X_._(b,a)
let a, b be Element of X; ::_thesis: the ExternalDiff of X . (a,b) = the ExternalDiff of X . (b,a)
thus the ExternalDiff of X . (a,b) = a * b
.= b * a by Th7
.= the ExternalDiff of X . (b,a) ; ::_thesis: verum
end;
hence the ExternalDiff of X is commutative by BINOP_1:def_2; ::_thesis: verum
end;
Lm5: for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is associative
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: the ExternalDiff of X is associative
now__::_thesis:_for_a,_b,_c_being_Element_of_X_holds_the_ExternalDiff_of_X_._(a,(_the_ExternalDiff_of_X_._(b,c)))_=_the_ExternalDiff_of_X_._((_the_ExternalDiff_of_X_._(a,b)),c)
let a, b, c be Element of X; ::_thesis: the ExternalDiff of X . (a,( the ExternalDiff of X . (b,c))) = the ExternalDiff of X . (( the ExternalDiff of X . (a,b)),c)
thus the ExternalDiff of X . (a,( the ExternalDiff of X . (b,c))) = a * (b * c)
.= (a * b) * c by Th10
.= the ExternalDiff of X . (( the ExternalDiff of X . (a,b)),c) ; ::_thesis: verum
end;
hence the ExternalDiff of X is associative by BINOP_1:def_3; ::_thesis: verum
end;
registration
let X be BCI-Algebra_with_Condition(S);
cluster the ExternalDiff of X -> commutative associative ;
coherence
( the ExternalDiff of X is commutative & the ExternalDiff of X is associative ) by Lm4, Lm5;
end;
theorem Th17: :: BCIALG_4:17
for X being BCI-Algebra_with_Condition(S) holds 0. X is_a_unity_wrt the ExternalDiff of X
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: 0. X is_a_unity_wrt the ExternalDiff of X
now__::_thesis:_for_a_being_Element_of_X_holds_
(_the_ExternalDiff_of_X_._((0._X),a)_=_a_&_the_ExternalDiff_of_X_._(a,(0._X))_=_a_)
let a be Element of X; ::_thesis: ( the ExternalDiff of X . ((0. X),a) = a & the ExternalDiff of X . (a,(0. X)) = a )
thus the ExternalDiff of X . ((0. X),a) = (0. X) * a
.= a by Th9 ; ::_thesis: the ExternalDiff of X . (a,(0. X)) = a
thus the ExternalDiff of X . (a,(0. X)) = a * (0. X)
.= a by Th9 ; ::_thesis: verum
end;
hence 0. X is_a_unity_wrt the ExternalDiff of X by BINOP_1:3; ::_thesis: verum
end;
theorem :: BCIALG_4:18
for X being BCI-Algebra_with_Condition(S) holds the_unity_wrt the ExternalDiff of X = 0. X
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: the_unity_wrt the ExternalDiff of X = 0. X
reconsider e = 0. X as Element of X ;
e is_a_unity_wrt the ExternalDiff of X by Th17;
hence the_unity_wrt the ExternalDiff of X = 0. X by BINOP_1:def_8; ::_thesis: verum
end;
theorem Th19: :: BCIALG_4:19
for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is having_a_unity
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: the ExternalDiff of X is having_a_unity
reconsider e = 0. X as Element of X ;
e is_a_unity_wrt the ExternalDiff of X by Th17;
hence the ExternalDiff of X is having_a_unity by SETWISEO:def_2; ::_thesis: verum
end;
definition
let X be BCI-Algebra_with_Condition(S);
func power X -> Function of [: the carrier of X,NAT:], the carrier of X means :Def6: :: BCIALG_4:def 6
for h being Element of X holds
( it . (h,0) = 0. X & ( for n being Element of NAT holds it . (h,(n + 1)) = (it . (h,n)) * h ) );
existence
ex b1 being Function of [: the carrier of X,NAT:], the carrier of X st
for h being Element of X holds
( b1 . (h,0) = 0. X & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) )
proof
defpred S1[ set , set ] means ex g0 being Function of NAT, the carrier of X ex h being Element of X st
( $1 = h & g0 = $2 & g0 . 0 = 0. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * h ) );
A1: for x being set st x in the carrier of X holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of X implies ex y being set st S1[x,y] )
assume x in the carrier of X ; ::_thesis: ex y being set st S1[x,y]
then reconsider b = x as Element of X ;
deffunc H1( Nat, Element of X) -> Element of X = $2 * b;
consider g0 being Function of NAT, the carrier of X such that
A2: g0 . 0 = 0. X and
A3: for n being Nat holds g0 . (n + 1) = H1(n,g0 . n) from NAT_1:sch_12();
reconsider y = g0 as set ;
take y ; ::_thesis: S1[x,y]
take g0 ; ::_thesis: ex h being Element of X st
( x = h & g0 = y & g0 . 0 = 0. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * h ) )
take b ; ::_thesis: ( x = b & g0 = y & g0 . 0 = 0. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * b ) )
thus ( x = b & g0 = y & g0 . 0 = 0. X ) by A2; ::_thesis: for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * b
let n be Element of NAT ; ::_thesis: g0 . (n + 1) = (g0 . n) * b
thus g0 . (n + 1) = (g0 . n) * b by A3; ::_thesis: verum
end;
consider f being Function such that
dom f = the carrier of X and
A4: for x being set st x in the carrier of X holds
S1[x,f . x] from CLASSES1:sch_1(A1);
defpred S2[ Element of X, Element of NAT , set ] means ex g0 being Function of NAT, the carrier of X st
( g0 = f . $1 & $3 = g0 . $2 );
A5: for a being Element of X
for n being Element of NAT ex b being Element of X st S2[a,n,b]
proof
let a be Element of X; ::_thesis: for n being Element of NAT ex b being Element of X st S2[a,n,b]
let n be Element of NAT ; ::_thesis: ex b being Element of X st S2[a,n,b]
consider g0 being Function of NAT, the carrier of X, h being Element of X such that
a = h and
A6: g0 = f . a and
g0 . 0 = 0. X and
for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * h by A4;
take g0 . n ; ::_thesis: S2[a,n,g0 . n]
take g0 ; ::_thesis: ( g0 = f . a & g0 . n = g0 . n )
thus ( g0 = f . a & g0 . n = g0 . n ) by A6; ::_thesis: verum
end;
consider F being Function of [: the carrier of X,NAT:], the carrier of X such that
A7: for a being Element of X
for n being Element of NAT holds S2[a,n,F . (a,n)] from BINOP_1:sch_3(A5);
take F ; ::_thesis: for h being Element of X holds
( F . (h,0) = 0. X & ( for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h ) )
let h be Element of X; ::_thesis: ( F . (h,0) = 0. X & ( for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h ) )
A8: ex g2 being Function of NAT, the carrier of X ex b being Element of X st
( h = b & g2 = f . h & g2 . 0 = 0. X & ( for n being Element of NAT holds g2 . (n + 1) = (g2 . n) * b ) ) by A4;
ex g1 being Function of NAT, the carrier of X st
( g1 = f . h & F . (h,0) = g1 . 0 ) by A7;
hence F . (h,0) = 0. X by A8; ::_thesis: for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h
let n be Element of NAT ; ::_thesis: F . (h,(n + 1)) = (F . (h,n)) * h
A9: ex g2 being Function of NAT, the carrier of X ex b being Element of X st
( h = b & g2 = f . h & g2 . 0 = 0. X & ( for n being Element of NAT holds g2 . (n + 1) = (g2 . n) * b ) ) by A4;
( ex g0 being Function of NAT, the carrier of X st
( g0 = f . h & F . (h,n) = g0 . n ) & ex g1 being Function of NAT, the carrier of X st
( g1 = f . h & F . (h,(n + 1)) = g1 . (n + 1) ) ) by A7;
hence F . (h,(n + 1)) = (F . (h,n)) * h by A9; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [: the carrier of X,NAT:], the carrier of X st ( for h being Element of X holds
( b1 . (h,0) = 0. X & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) & ( for h being Element of X holds
( b2 . (h,0) = 0. X & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds
b1 = b2
proof
let f, g be Function of [: the carrier of X,NAT:], the carrier of X; ::_thesis: ( ( for h being Element of X holds
( f . (h,0) = 0. X & ( for n being Element of NAT holds f . (h,(n + 1)) = (f . (h,n)) * h ) ) ) & ( for h being Element of X holds
( g . (h,0) = 0. X & ( for n being Element of NAT holds g . (h,(n + 1)) = (g . (h,n)) * h ) ) ) implies f = g )
assume that
A10: for h being Element of X holds
( f . (h,0) = 0. X & ( for n being Element of NAT holds f . (h,(n + 1)) = (f . (h,n)) * h ) ) and
A11: for h being Element of X holds
( g . (h,0) = 0. X & ( for n being Element of NAT holds g . (h,(n + 1)) = (g . (h,n)) * h ) ) ; ::_thesis: f = g
now__::_thesis:_for_h_being_Element_of_X
for_n_being_Element_of_NAT_holds_f_._(h,n)_=_g_._(h,n)
let h be Element of X; ::_thesis: for n being Element of NAT holds f . (h,n) = g . (h,n)
let n be Element of NAT ; ::_thesis: f . (h,n) = g . (h,n)
defpred S1[ Element of NAT ] means f . [h,$1] = g . [h,$1];
A12: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A13: S1[n] ; ::_thesis: S1[n + 1]
A14: g . [h,n] = g . (h,n) ;
f . [h,(n + 1)] = f . (h,(n + 1))
.= (f . (h,n)) * h by A10
.= g . (h,(n + 1)) by A11, A13, A14
.= g . [h,(n + 1)] ;
hence S1[n + 1] ; ::_thesis: verum
end;
f . [h,0] = f . (h,0)
.= 0. X by A10
.= g . (h,0) by A11
.= g . [h,0] ;
then A15: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A12);
hence f . (h,n) = g . (h,n) ; ::_thesis: verum
end;
hence f = g by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines power BCIALG_4:def_6_:_
for X being BCI-Algebra_with_Condition(S)
for b2 being Function of [: the carrier of X,NAT:], the carrier of X holds
( b2 = power X iff for h being Element of X holds
( b2 . (h,0) = 0. X & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) );
definition
let X be BCI-Algebra_with_Condition(S);
let x be Element of X;
let n be Element of NAT ;
funcx |^ n -> Element of X equals :: BCIALG_4:def 7
(power X) . (x,n);
correctness
coherence
(power X) . (x,n) is Element of X;
;
end;
:: deftheorem defines |^ BCIALG_4:def_7_:_
for X being BCI-Algebra_with_Condition(S)
for x being Element of X
for n being Element of NAT holds x |^ n = (power X) . (x,n);
theorem :: BCIALG_4:20
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 0 = 0. X by Def6;
theorem :: BCIALG_4:21
for n being Element of NAT
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ (n + 1) = (x |^ n) * x by Def6;
theorem Th22: :: BCIALG_4:22
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 1 = x
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds x |^ 1 = x
let x be Element of X; ::_thesis: x |^ 1 = x
thus x |^ 1 = x |^ (0 + 1)
.= (x |^ 0) * x by Def6
.= (0. X) * x by Def6
.= x by Th9 ; ::_thesis: verum
end;
theorem Th23: :: BCIALG_4:23
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 2 = x * x
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds x |^ 2 = x * x
let x be Element of X; ::_thesis: x |^ 2 = x * x
thus x |^ 2 = x |^ (1 + 1)
.= (x |^ 1) * x by Def6
.= x * x by Th22 ; ::_thesis: verum
end;
theorem :: BCIALG_4:24
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 3 = (x * x) * x
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds x |^ 3 = (x * x) * x
let x be Element of X; ::_thesis: x |^ 3 = (x * x) * x
thus x |^ 3 = x |^ (2 + 1)
.= (x |^ 2) * x by Def6
.= (x * x) * x by Th23 ; ::_thesis: verum
end;
theorem Th25: :: BCIALG_4:25
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ 2 = 0. X
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: (0. X) |^ 2 = 0. X
(0. X) * (0. X) = ((0. X) * (0. X)) \ (0. X) by BCIALG_1:2;
then (0. X) * (0. X) <= 0. X by Lm2;
then A1: ((0. X) * (0. X)) \ (0. X) = 0. X by BCIALG_1:def_11;
0. X <= (0. X) * ((0. X) \ (0. X)) by Th13;
then 0. X <= (0. X) * (0. X) by BCIALG_1:def_5;
then (0. X) \ ((0. X) * (0. X)) = 0. X by BCIALG_1:def_11;
then (0. X) * (0. X) = 0. X by A1, BCIALG_1:def_7;
hence (0. X) |^ 2 = 0. X by Th23; ::_thesis: verum
end;
Lm6: for n being Element of NAT
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X
proof
let n be Element of NAT ; ::_thesis: for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X
let X be BCI-Algebra_with_Condition(S); ::_thesis: (0. X) |^ (n + 1) = 0. X
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(0. X) |^ (m + 1) = 0. X;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
(0._X)_|^_(m_+_1)_=_0._X_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
(0._X)_|^_(m_+_1)_=_0._X
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(0. X) |^ (m + 1) = 0. X ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(0. X) |^ (m + 1) = 0. X )
assume A1: for m being Element of NAT st m = k & m <= n holds
(0. X) |^ (m + 1) = 0. X ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
(0. X) |^ (m + 1) = 0. X
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (0. X) |^ (m + 1) = 0. X )
assume that
A2: m = k + 1 and
A3: m <= n ; ::_thesis: (0. X) |^ (m + 1) = 0. X
k <= n by A2, A3, NAT_1:13;
then A4: (0. X) |^ (k + 1) = 0. X by A1;
A5: (0. X) |^ 2 = 0. X by Th25;
(0. X) |^ (m + 1) = ((0. X) |^ (k + 1)) * (0. X) by A2, Def6;
hence (0. X) |^ (m + 1) = 0. X by A5, A4, Th23; ::_thesis: verum
end;
then A6: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A7: S1[ 0 ] by Th22;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6);
hence (0. X) |^ (n + 1) = 0. X ; ::_thesis: verum
end;
theorem :: BCIALG_4:26
for n being Element of NAT
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X
proof
let n be Element of NAT ; ::_thesis: for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X
let X be BCI-Algebra_with_Condition(S); ::_thesis: (0. X) |^ n = 0. X
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(0. X) |^ m = 0. X;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1] by Lm6;
A2: S1[ 0 ] by Def6;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1);
hence (0. X) |^ n = 0. X ; ::_thesis: verum
end;
theorem :: BCIALG_4:27
for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds ((x \ a) \ a) \ a = x \ (a |^ 3)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a being Element of X holds ((x \ a) \ a) \ a = x \ (a |^ 3)
let x, a be Element of X; ::_thesis: ((x \ a) \ a) \ a = x \ (a |^ 3)
(x \ a) \ a = x \ (a * a) by Th12;
then ((x \ a) \ a) \ a = x \ ((a * a) * a) by Th12
.= x \ ((a |^ 2) * a) by Th23
.= x \ (a |^ (2 + 1)) by Def6 ;
hence ((x \ a) \ a) \ a = x \ (a |^ 3) ; ::_thesis: verum
end;
Lm7: for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds (x,a) to_power 0 = x \ (a |^ 0)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a being Element of X holds (x,a) to_power 0 = x \ (a |^ 0)
let x, a be Element of X; ::_thesis: (x,a) to_power 0 = x \ (a |^ 0)
x \ (a |^ 0) = x \ (0. X) by Def6
.= x by BCIALG_1:2 ;
hence (x,a) to_power 0 = x \ (a |^ 0) by BCIALG_2:1; ::_thesis: verum
end;
theorem :: BCIALG_4:28
for n being Element of NAT
for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n)
proof
let n be Element of NAT ; ::_thesis: for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n)
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n)
let x, a be Element of X; ::_thesis: (x,a) to_power n = x \ (a |^ n)
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(x,a) to_power m = x \ (a |^ m);
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
(x,a)_to_power_m_=_x_\_(a_|^_m)_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
(x,a)_to_power_m_=_x_\_(a_|^_m)
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(x,a) to_power m = x \ (a |^ m) ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(x,a) to_power m = x \ (a |^ m) )
assume A1: for m being Element of NAT st m = k & m <= n holds
(x,a) to_power m = x \ (a |^ m) ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
(x,a) to_power m = x \ (a |^ m)
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (x,a) to_power m = x \ (a |^ m) )
assume that
A2: m = k + 1 and
A3: m <= n ; ::_thesis: (x,a) to_power m = x \ (a |^ m)
A4: ( (x,a) to_power m = ((x,a) to_power k) \ a & k <= n ) by A2, A3, BCIALG_2:4, NAT_1:13;
x \ (a |^ m) = x \ ((a |^ k) * a) by A2, Def6
.= (x \ (a |^ k)) \ a by Th12 ;
hence (x,a) to_power m = x \ (a |^ m) by A1, A4; ::_thesis: verum
end;
then A5: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A6: S1[ 0 ] by Lm7;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5);
hence (x,a) to_power n = x \ (a |^ n) ; ::_thesis: verum
end;
definition
let X be non empty BCIStr_1 ;
let F be FinSequence of the carrier of X;
func Product_S F -> Element of X equals :: BCIALG_4:def 8
the ExternalDiff of X "**" F;
correctness
coherence
the ExternalDiff of X "**" F is Element of X;
;
end;
:: deftheorem defines Product_S BCIALG_4:def_8_:_
for X being non empty BCIStr_1
for F being FinSequence of the carrier of X holds Product_S F = the ExternalDiff of X "**" F;
theorem :: BCIALG_4:29
for X being non empty BCIStr_1
for d being Element of X holds the ExternalDiff of X "**" <*d*> = d
proof
let X be non empty BCIStr_1 ; ::_thesis: for d being Element of X holds the ExternalDiff of X "**" <*d*> = d
let d be Element of X; ::_thesis: the ExternalDiff of X "**" <*d*> = d
A1: len <*d*> = 1 by FINSEQ_1:39;
then ex f being Function of NAT, the carrier of X st
( f . 1 = <*d*> . 1 & ( for n being Element of NAT st 0 <> n & n < len <*d*> holds
f . (n + 1) = the ExternalDiff of X . ((f . n),(<*d*> . (n + 1))) ) & the ExternalDiff of X "**" <*d*> = f . (len <*d*>) ) by FINSOP_1:def_1;
hence the ExternalDiff of X "**" <*d*> = d by A1, FINSEQ_1:def_8; ::_thesis: verum
end;
theorem :: BCIALG_4:30
for X being BCI-Algebra_with_Condition(S)
for F1, F2 being FinSequence of the carrier of X holds Product_S (F1 ^ F2) = (Product_S F1) * (Product_S F2) by Th19, FINSOP_1:5;
theorem :: BCIALG_4:31
for X being BCI-Algebra_with_Condition(S)
for F being FinSequence of the carrier of X
for a being Element of X holds Product_S (F ^ <*a*>) = (Product_S F) * a by Th19, FINSOP_1:4;
theorem :: BCIALG_4:32
for X being BCI-Algebra_with_Condition(S)
for F being FinSequence of the carrier of X
for a being Element of X holds Product_S (<*a*> ^ F) = a * (Product_S F) by Th19, FINSOP_1:6;
theorem Th33: :: BCIALG_4:33
for X being BCI-Algebra_with_Condition(S)
for a1, a2 being Element of X holds Product_S <*a1,a2*> = a1 * a2
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for a1, a2 being Element of X holds Product_S <*a1,a2*> = a1 * a2
let a1, a2 be Element of X; ::_thesis: Product_S <*a1,a2*> = a1 * a2
thus Product_S <*a1,a2*> = (Product_S <*a1*>) * a2 by Th19, FINSOP_1:4
.= a1 * a2 by FINSOP_1:11 ; ::_thesis: verum
end;
theorem Th34: :: BCIALG_4:34
for X being BCI-Algebra_with_Condition(S)
for a1, a2, a3 being Element of X holds Product_S <*a1,a2,a3*> = (a1 * a2) * a3
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for a1, a2, a3 being Element of X holds Product_S <*a1,a2,a3*> = (a1 * a2) * a3
let a1, a2, a3 be Element of X; ::_thesis: Product_S <*a1,a2,a3*> = (a1 * a2) * a3
thus Product_S <*a1,a2,a3*> = (Product_S <*a1,a2*>) * a3 by Th19, FINSOP_1:4
.= (a1 * a2) * a3 by FINSOP_1:12 ; ::_thesis: verum
end;
theorem :: BCIALG_4:35
for X being BCI-Algebra_with_Condition(S)
for x, a1, a2 being Element of X holds (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a1, a2 being Element of X holds (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)
let x, a1, a2 be Element of X; ::_thesis: (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)
(x \ a1) \ a2 = x \ (a1 * a2) by Th12;
hence (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>) by Th33; ::_thesis: verum
end;
theorem :: BCIALG_4:36
for X being BCI-Algebra_with_Condition(S)
for x, a1, a2, a3 being Element of X holds ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a1, a2, a3 being Element of X holds ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)
let x, a1, a2, a3 be Element of X; ::_thesis: ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)
((x \ a1) \ a2) \ a3 = (x \ (a1 * a2)) \ a3 by Th12
.= x \ ((a1 * a2) * a3) by Th12 ;
hence ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>) by Th34; ::_thesis: verum
end;
theorem :: BCIALG_4:37
for X being BCI-Algebra_with_Condition(S)
for a, b being Element of AtomSet X
for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
proof
let X be BCI-Algebra_with_Condition(S); ::_thesis: for a, b being Element of AtomSet X
for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
let a, b be Element of AtomSet X; ::_thesis: for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
let ma be Element of X; ::_thesis: ( ( for x being Element of BranchV a holds x <= ma ) implies ex mb being Element of X st
for y being Element of BranchV b holds y <= mb )
assume A1: for x being Element of BranchV a holds x <= ma ; ::_thesis: ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
proof
set mb = (b * ((0. X) \ a)) * ma;
for y being Element of BranchV b holds y <= (b * ((0. X) \ a)) * ma
proof
a \ a = 0. X by BCIALG_1:def_5;
then a <= a by BCIALG_1:def_11;
then a in { yy2 where yy2 is Element of X : a <= yy2 } ;
then A2: a is Element of BranchV a ;
let y be Element of BranchV b; ::_thesis: y <= (b * ((0. X) \ a)) * ma
0. X in AtomSet X ;
then consider x0 being Element of AtomSet X such that
A3: x0 = 0. X ;
y in { yy where yy is Element of X : b <= yy } ;
then ex yy being Element of X st
( y = yy & b <= yy ) ;
then b \ b <= y \ b by BCIALG_1:5;
then y \ b in { yy1 where yy1 is Element of X : b \ b <= yy1 } ;
then A4: y \ b is Element of BranchV (b \ b) ;
A5: (b \ b) \ (x0 \ a) = x0 \ (x0 \ a) by A3, BCIALG_1:def_5
.= a by BCIALG_1:24 ;
x0 \ x0 = 0. X by BCIALG_1:def_5;
then x0 <= x0 by BCIALG_1:def_11;
then x0 in { yy2 where yy2 is Element of X : x0 <= yy2 } ;
then x0 is Element of BranchV x0 ;
then x0 \ a is Element of BranchV (x0 \ a) by A2, BCIALG_1:39;
then (y \ b) \ (x0 \ a) is Element of BranchV a by A4, A5, BCIALG_1:39;
then A6: (y \ b) \ (x0 \ a) <= ma by A1;
y \ ((b * ((0. X) \ a)) * ma) = (y \ (b * ((0. X) \ a))) \ ma by Th12
.= ((y \ b) \ (x0 \ a)) \ ma by A3, Th12
.= 0. X by A6, BCIALG_1:def_11 ;
hence y <= (b * ((0. X) \ a)) * ma by BCIALG_1:def_11; ::_thesis: verum
end;
hence ex mb being Element of X st
for y being Element of BranchV b holds y <= mb ; ::_thesis: verum
end;
hence ex mb being Element of X st
for y being Element of BranchV b holds y <= mb ; ::_thesis: verum
end;
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 strict with_condition_S for BCIStr_1 ;
existence
ex b1 being BCI-Algebra_with_Condition(S) st
( b1 is strict & b1 is being_BCK-5 ) by Lm1;
end;
definition
mode BCK-Algebra_with_Condition(S) is being_BCK-5 BCI-Algebra_with_Condition(S);
end;
theorem Th38: :: BCIALG_4:38
for X being BCK-Algebra_with_Condition(S)
for x, y being Element of X holds
( x <= x * y & y <= x * y )
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds
( x <= x * y & y <= x * y )
for x, y being Element of X holds
( x <= x * y & y <= x * y )
proof
let x, y be Element of X; ::_thesis: ( x <= x * y & y <= x * y )
A1: (x \ x) \ y = y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
A2: (y \ y) \ x = x ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
A3: (x \ x) \ y = x \ (x * y) by Th12;
(y \ y) \ x = y \ (y * x) by Th12
.= y \ (x * y) by Th7 ;
hence ( x <= x * y & y <= x * y ) by A3, A1, A2, BCIALG_1:def_11; ::_thesis: verum
end;
hence for x, y being Element of X holds
( x <= x * y & y <= x * y ) ; ::_thesis: verum
end;
theorem :: BCIALG_4:39
for X being BCK-Algebra_with_Condition(S)
for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X
for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x * y) \ (y * z)) \ (z * x) = 0. X
(y * x) \ y <= x by Lm2;
then A1: ((y * x) \ y) \ z <= x \ z by BCIALG_1:5;
x * y = y * x by Th7;
then (x * y) \ (y * z) <= x \ z by A1, Th12;
then A2: ((x * y) \ (y * z)) \ (z * x) <= (x \ z) \ (z * x) by BCIALG_1:5;
(x \ z) \ (z * x) = ((x \ z) \ z) \ x by Th12
.= ((x \ z) \ x) \ z by BCIALG_1:7
.= ((x \ x) \ z) \ z by BCIALG_1:7
.= (z `) \ z by BCIALG_1:def_5
.= z ` by BCIALG_1:def_8
.= 0. X by BCIALG_1:def_8 ;
then (((x * y) \ (y * z)) \ (z * x)) \ (0. X) = 0. X by A2, BCIALG_1:def_11;
hence ((x * y) \ (y * z)) \ (z * x) = 0. X by BCIALG_1:2; ::_thesis: verum
end;
hence for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X ; ::_thesis: verum
end;
theorem :: BCIALG_4:40
for X being BCK-Algebra_with_Condition(S)
for x, y being Element of X holds (x \ y) * (y \ x) <= x * y
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds (x \ y) * (y \ x) <= x * y
for x, y being Element of X holds (x \ y) * (y \ x) <= x * y
proof
let x, y be Element of X; ::_thesis: (x \ y) * (y \ x) <= x * y
((x \ y) * (y \ x)) \ (x \ y) <= y \ x by Lm2;
then A1: (((x \ y) * (y \ x)) \ (x \ y)) \ y <= (y \ x) \ y by BCIALG_1:5;
(y \ x) \ y = (y \ y) \ x by BCIALG_1:7
.= x ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then ((x \ y) * (y \ x)) \ ((x \ y) * y) <= 0. X by A1, Th12;
then (((x \ y) * (y \ x)) \ ((x \ y) * y)) \ (0. X) = 0. X by BCIALG_1:def_11;
then A2: ((x \ y) * (y \ x)) \ ((x \ y) * y) = 0. X by BCIALG_1:2;
(y * (x \ y)) \ y <= x \ y by Lm2;
then A3: ((y * (x \ y)) \ y) \ x <= (x \ y) \ x by BCIALG_1:5;
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then (y * (x \ y)) \ (y * x) <= 0. X by A3, Th12;
then ((y * (x \ y)) \ (y * x)) \ (0. X) = 0. X by BCIALG_1:def_11;
then A4: (y * (x \ y)) \ (y * x) = 0. X by BCIALG_1:2;
(x \ y) * y = y * (x \ y) by Th7;
then ((x \ y) * (y \ x)) \ (y * x) = 0. X by A2, A4, BCIALG_1:3;
then (x \ y) * (y \ x) <= y * x by BCIALG_1:def_11;
hence (x \ y) * (y \ x) <= x * y by Th7; ::_thesis: verum
end;
hence for x, y being Element of X holds (x \ y) * (y \ x) <= x * y ; ::_thesis: verum
end;
theorem :: BCIALG_4:41
for X being BCK-Algebra_with_Condition(S)
for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x
for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x
proof
let x be Element of X; ::_thesis: (x \ (0. X)) * ((0. X) \ x) = x
A1: (0. X) \ x = x `
.= 0. X by BCIALG_1:def_8 ;
x \ (0. X) = x by BCIALG_1:2;
hence (x \ (0. X)) * ((0. X) \ x) = x by A1, Th9; ::_thesis: verum
end;
hence for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x ; ::_thesis: verum
end;
definition
let IT be BCK-Algebra_with_Condition(S);
attrIT is commutative means :Def9: :: BCIALG_4:def 9
for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x);
end;
:: deftheorem Def9 defines commutative BCIALG_4:def_9_:_
for IT being BCK-Algebra_with_Condition(S) holds
( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative for BCIStr_1 ;
existence
ex b1 being BCK-Algebra_with_Condition(S) st b1 is commutative
proof
reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ;
IT is commutative
proof
let x, y be Element of IT; :: according to BCIALG_4:def_9 ::_thesis: x \ (x \ y) = y \ (y \ x)
thus x \ (x \ y) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum
end;
hence ex b1 being BCK-Algebra_with_Condition(S) st b1 is commutative ; ::_thesis: verum
end;
end;
theorem :: BCIALG_4:42
for X being non empty BCIStr_1 holds
( X is commutative BCK-Algebra_with_Condition(S) 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) \ z = x \ (y * z) ) )
proof
let X be non empty BCIStr_1 ; ::_thesis: ( X is commutative BCK-Algebra_with_Condition(S) 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) \ z = x \ (y * z) ) )
thus ( X is commutative BCK-Algebra_with_Condition(S) 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) \ z = x \ (y * z) ) ) ::_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) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) )
proof
assume A1: X is commutative BCK-Algebra_with_Condition(S) ; ::_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) \ z = x \ (y * z) )
let x, y, z be Element of X; ::_thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) )
(x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def9;
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) & (x \ y) \ z = x \ (y * z) ) by A1, A2, Th12, BCIALG_1:2; ::_thesis: verum
end;
thus ( ( for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) ) ::_thesis: verum
proof
assume A3: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ; ::_thesis: X is commutative BCK-Algebra_with_Condition(S)
A4: 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;
A5: 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 A4
.= y \ (0. X) by A4 ;
hence x = y \ (0. X) by A4
.= y by A4 ;
::_thesis: verum
end;
A6: 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 A4;
then x \ x = ((0. X) \ (0. X)) \ ((0. X) \ x) by A3
.= (0. X) \ ((0. X) \ x) by A4
.= 0. X by A3 ;
hence x \ x = 0. X ; ::_thesis: verum
end;
A7: 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 A6
.= (0. X) \ x by A3 ;
hence (0. X) \ x = 0. X ; ::_thesis: verum
end;
A8: 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 A4
.= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3
.= (0. X) \ ((0. X) \ (z \ y)) by A7
.= 0. X by A7 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ; ::_thesis: verum
end;
A9: for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
proof
let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X & y \ z = 0. X implies x \ z = 0. X )
assume that
A10: x \ y = 0. X and
A11: y \ z = 0. X ; ::_thesis: x \ z = 0. X
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A8;
then (x \ z) \ (x \ y) = 0. X by A4, A11;
hence x \ z = 0. X by A4, A10; ::_thesis: verum
end;
A12: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
(((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ z) = 0. X by A8;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ (z \ (0. X))) = 0. X by A4;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (((x \ (0. X)) \ (x \ z)) \ (z \ (0. X))) = 0. X by A4;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (0. X) = 0. X by A8;
then A13: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A4;
((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by A8;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A9, A13; ::_thesis: verum
end;
A14: 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;
A15: for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
proof
let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X implies ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) )
assume A16: x \ y = 0. X ; ::_thesis: ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
( ((z \ y) \ (z \ x)) \ (x \ y) = 0. X & ((x \ z) \ (x \ y)) \ (y \ z) = 0. X ) by A8;
hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A4, A16; ::_thesis: verum
end;
A17: for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A8;
then ((x \ y) \ (z \ y)) \ ((x \ y) \ ((x \ y) \ (x \ z))) = 0. X by A15;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (((x \ y) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A15;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ ((((x \ y) \ (0. X)) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A4;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ ((((x \ y) \ (0. X)) \ ((x \ y) \ (x \ z))) \ ((x \ z) \ (0. X))) = 0. X by A4;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (0. X) = 0. X by A8;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A4; ::_thesis: verum
end;
for x being Element of X holds x ` = 0. X by A7;
hence X is commutative BCK-Algebra_with_Condition(S) by A3, A6, A5, A14, A12, A17, Def2, Def9, BCIALG_1:def_3, BCIALG_1:def_4, BCIALG_1:def_5, BCIALG_1:def_7, BCIALG_1:def_8; ::_thesis: verum
end;
end;
theorem :: BCIALG_4:43
for X being commutative BCK-Algebra_with_Condition(S)
for a being Element of X st a is greatest holds
for x, y being Element of X holds x * y = a \ ((a \ x) \ y)
proof
let X be commutative BCK-Algebra_with_Condition(S); ::_thesis: for a being Element of X st a is greatest holds
for x, y being Element of X holds x * y = a \ ((a \ x) \ y)
let a be Element of X; ::_thesis: ( a is greatest implies for x, y being Element of X holds x * y = a \ ((a \ x) \ y) )
assume A1: a is greatest ; ::_thesis: for x, y being Element of X holds x * y = a \ ((a \ x) \ y)
for x, y being Element of X holds x * y = a \ ((a \ x) \ y)
proof
let x, y be Element of X; ::_thesis: x * y = a \ ((a \ x) \ y)
A2: x * y <= a by A1, BCIALG_2:def_5;
a \ ((a \ x) \ y) = a \ (a \ (x * y)) by Th12
.= (x * y) \ ((x * y) \ a) by Def9
.= (x * y) \ (0. X) by A2, BCIALG_1:def_11 ;
hence x * y = a \ ((a \ x) \ y) by BCIALG_1:2; ::_thesis: verum
end;
hence for x, y being Element of X holds x * y = a \ ((a \ x) \ y) ; ::_thesis: verum
end;
definition
let X be BCI-algebra;
let a be Element of X;
func Initial_section a -> non empty Subset of X equals :: BCIALG_4:def 10
{ t where t is Element of X : t <= a } ;
coherence
{ t where t is Element of X : t <= a } is non empty Subset of X
proof
set Y = { t where t is Element of X : t <= a } ;
A1: now__::_thesis:_for_y1_being_set_st_y1_in__{__t_where_t_is_Element_of_X_:_t_<=_a__}__holds_
y1_in_the_carrier_of_X
let y1 be set ; ::_thesis: ( y1 in { t where t is Element of X : t <= a } implies y1 in the carrier of X )
assume y1 in { t where t is Element of X : t <= a } ; ::_thesis: y1 in the carrier of X
then ex x1 being Element of X st
( y1 = x1 & x1 <= a ) ;
hence y1 in the carrier of X ; ::_thesis: verum
end;
a \ a = 0. X by BCIALG_1:def_5;
then a <= a by BCIALG_1:def_11;
then a in { t where t is Element of X : t <= a } ;
hence { t where t is Element of X : t <= a } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines Initial_section BCIALG_4:def_10_:_
for X being BCI-algebra
for a being Element of X holds Initial_section a = { t where t is Element of X : t <= a } ;
theorem :: BCIALG_4:44
for X being commutative BCK-Algebra_with_Condition(S)
for a, b, c being Element of X st Condition_S (a,b) c= Initial_section c holds
for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)
proof
let X be commutative BCK-Algebra_with_Condition(S); ::_thesis: for a, b, c being Element of X st Condition_S (a,b) c= Initial_section c holds
for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)
let a, b, c be Element of X; ::_thesis: ( Condition_S (a,b) c= Initial_section c implies for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) )
assume A1: Condition_S (a,b) c= Initial_section c ; ::_thesis: for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)
for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)
proof
set u = c \ ((c \ a) \ b);
let x be Element of Condition_S (a,b); ::_thesis: x <= c \ ((c \ a) \ b)
A2: (c \ (c \ x)) \ x = (c \ x) \ (c \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def_5 ;
x in { t2 where t2 is Element of X : t2 <= c } by A1, TARSKI:def_3;
then consider x2 being Element of X such that
A3: x = x2 and
A4: x2 <= c ;
A5: x \ (c \ (c \ x)) = x \ (x \ (x \ c)) by Def9
.= x2 \ c by A3, BCIALG_1:8
.= 0. X by A4, BCIALG_1:def_11 ;
then A6: ( ((c \ (c \ x)) \ (c \ ((c \ a) \ b))) \ (((c \ a) \ b) \ (c \ x)) = 0. X & x \ (c \ ((c \ a) \ b)) = (c \ (c \ x)) \ (c \ ((c \ a) \ b)) ) by A2, BCIALG_1:1, BCIALG_1:def_7;
x in { t1 where t1 is Element of X : t1 \ a <= b } ;
then A7: ex x1 being Element of X st
( x = x1 & x1 \ a <= b ) ;
((c \ a) \ b) \ (c \ x) = ((c \ a) \ (c \ x)) \ b by BCIALG_1:7
.= ((c \ (c \ x)) \ a) \ b by BCIALG_1:7
.= (x \ a) \ b by A5, A2, BCIALG_1:def_7
.= 0. X by A7, BCIALG_1:def_11 ;
then x \ (c \ ((c \ a) \ b)) = 0. X by A6, BCIALG_1:2;
hence x <= c \ ((c \ a) \ b) by BCIALG_1:def_11; ::_thesis: verum
end;
hence for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) ; ::_thesis: verum
end;
definition
let IT be BCK-Algebra_with_Condition(S);
attrIT is positive-implicative means :Def11: :: BCIALG_4:def 11
for x, y being Element of IT holds (x \ y) \ y = x \ y;
end;
:: deftheorem Def11 defines positive-implicative BCIALG_4:def_11_:_
for IT being BCK-Algebra_with_Condition(S) holds
( IT is positive-implicative iff for x, y being Element of IT holds (x \ y) \ y = x \ y );
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative for BCIStr_1 ;
existence
ex b1 being BCK-Algebra_with_Condition(S) st b1 is positive-implicative
proof
reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ;
IT is positive-implicative
proof
let x, y be Element of IT; :: according to BCIALG_4:def_11 ::_thesis: (x \ y) \ y = x \ y
thus (x \ y) \ y = x \ y by STRUCT_0:def_10; ::_thesis: verum
end;
hence ex b1 being BCK-Algebra_with_Condition(S) st b1 is positive-implicative ; ::_thesis: verum
end;
end;
theorem Th45: :: BCIALG_4:45
for X being BCK-Algebra_with_Condition(S) holds
( X is positive-implicative iff for x being Element of X holds x * x = x )
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x being Element of X holds x * x = x )
A1: ( X is positive-implicative implies for x being Element of X holds x * x = x )
proof
assume A2: X is positive-implicative ; ::_thesis: for x being Element of X holds x * x = x
let x be Element of X; ::_thesis: x * x = x
A3: (x * x) \ x <= x by Lm2;
(x * x) \ x = ((x * x) \ x) \ x by A2, Def11;
then (x * x) \ x <= x \ x by A3, BCIALG_1:5;
then ( x \ x = 0. X & ((x * x) \ x) \ (x \ x) = 0. X ) by BCIALG_1:def_5, BCIALG_1:def_11;
then A4: (x * x) \ x = 0. X by BCIALG_1:2;
x \ (x * x) = (x \ x) \ x by Th12
.= x ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x * x = x by A4, BCIALG_1:def_7; ::_thesis: verum
end;
( ( for x being Element of X holds x * x = x ) implies X is positive-implicative )
proof
assume A5: for x being Element of X holds x * x = x ; ::_thesis: X is positive-implicative
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
x \ (y * y) = x \ y by A5;
hence (x \ y) \ y = x \ y by Th12; ::_thesis: verum
end;
hence X is positive-implicative by Def11; ::_thesis: verum
end;
hence ( X is positive-implicative iff for x being Element of X holds x * x = x ) by A1; ::_thesis: verum
end;
theorem Th46: :: BCIALG_4:46
for X being BCK-Algebra_with_Condition(S) holds
( X is positive-implicative iff for x, y being Element of X st x <= y holds
x * y = y )
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x, y being Element of X st x <= y holds
x * y = y )
A1: ( X is positive-implicative implies for x, y being Element of X st x <= y holds
x * y = y )
proof
assume A2: X is positive-implicative ; ::_thesis: for x, y being Element of X st x <= y holds
x * y = y
let x, y be Element of X; ::_thesis: ( x <= y implies x * y = y )
A3: (y * x) \ y <= x by Lm2;
(x * y) \ y = (y * x) \ y by Th7
.= ((y * x) \ y) \ y by A2, Def11 ;
then (x * y) \ y <= x \ y by A3, BCIALG_1:5;
then A4: ((x * y) \ y) \ (x \ y) = 0. X by BCIALG_1:def_11;
A5: y \ (x * y) = y \ (y * x) by Th7
.= (y \ y) \ x by Th12
.= x ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
assume x <= y ; ::_thesis: x * y = y
then x \ y = 0. X by BCIALG_1:def_11;
then (x * y) \ y = 0. X by A4, BCIALG_1:2;
hence x * y = y by A5, BCIALG_1:def_7; ::_thesis: verum
end;
( ( for x, y being Element of X st x <= y holds
x * y = y ) implies X is positive-implicative )
proof
assume A6: for x, y being Element of X st x <= y holds
x * y = y ; ::_thesis: X is positive-implicative
for x being Element of X holds x * x = x
proof
let x be Element of X; ::_thesis: x * x = x
x \ x = 0. X by BCIALG_1:def_5;
then x <= x by BCIALG_1:def_11;
hence x * x = x by A6; ::_thesis: verum
end;
hence X is positive-implicative by Th45; ::_thesis: verum
end;
hence ( X is positive-implicative iff for x, y being Element of X st x <= y holds
x * y = y ) by A1; ::_thesis: verum
end;
theorem Th47: :: BCIALG_4:47
for X being BCK-Algebra_with_Condition(S) holds
( X is positive-implicative iff for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) )
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) )
A1: ( X is positive-implicative implies for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) )
proof
assume A2: X is positive-implicative ; ::_thesis: for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z)
let x, y, z be Element of X; ::_thesis: (x * y) \ z = (x \ z) * (y \ z)
(((x * y) \ z) \ (x \ z)) \ ((x * y) \ x) = 0. X by BCIALG_1:def_3;
then ((x * y) \ z) \ (x \ z) <= (x * y) \ x by BCIALG_1:def_11;
then (((x * y) \ z) \ (x \ z)) \ z <= ((x * y) \ x) \ z by BCIALG_1:5;
then A3: ((((x * y) \ z) \ (x \ z)) \ z) \ (((x * y) \ x) \ z) = 0. X by BCIALG_1:def_11;
(x * y) \ x <= y by Lm2;
then ((x * y) \ x) \ z <= y \ z by BCIALG_1:5;
then A4: (((x * y) \ x) \ z) \ (y \ z) = 0. X by BCIALG_1:def_11;
(x * y) \ z = (x * y) \ (z * z) by A2, Th45
.= ((x * y) \ z) \ z by Th12 ;
then ((x * y) \ z) \ (x \ z) = (((x * y) \ z) \ (x \ z)) \ z by BCIALG_1:7;
then (((x * y) \ z) \ (x \ z)) \ (y \ z) = 0. X by A3, A4, BCIALG_1:3;
then A5: ((x * y) \ z) \ ((x \ z) * (y \ z)) = 0. X by Th12;
y <= x * y by Th38;
then y \ z <= (x * y) \ z by BCIALG_1:5;
then ((x * y) \ z) * (y \ z) <= ((x * y) \ z) * ((x * y) \ z) by Th8;
then A6: (((x * y) \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by BCIALG_1:def_11;
x <= x * y by Th38;
then x \ z <= (x * y) \ z by BCIALG_1:5;
then (x \ z) * (y \ z) <= ((x * y) \ z) * (y \ z) by Th8;
then ((x \ z) * (y \ z)) \ (((x * y) \ z) * (y \ z)) = 0. X by BCIALG_1:def_11;
then ((x \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by A6, BCIALG_1:3;
then ((x \ z) * (y \ z)) \ ((x * y) \ z) = 0. X by A2, Th45;
hence (x * y) \ z = (x \ z) * (y \ z) by A5, BCIALG_1:def_7; ::_thesis: verum
end;
( ( for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ) implies X is positive-implicative )
proof
assume A7: for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ; ::_thesis: X is positive-implicative
for x being Element of X holds x * x = x
proof
let x be Element of X; ::_thesis: x * x = x
(x * x) \ x = (x \ x) * (x \ x) by A7;
then (x * x) \ x = (0. X) * (x \ x) by BCIALG_1:def_5;
then (x * x) \ x = (0. X) * (0. X) by BCIALG_1:def_5;
then A8: (x * x) \ x = 0. X by Th9;
x \ (x * x) = (x \ x) \ x by Th12
.= x ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
hence x * x = x by A8, BCIALG_1:def_7; ::_thesis: verum
end;
hence X is positive-implicative by Th45; ::_thesis: verum
end;
hence ( X is positive-implicative iff for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ) by A1; ::_thesis: verum
end;
theorem Th48: :: BCIALG_4:48
for X being BCK-Algebra_with_Condition(S) holds
( X is positive-implicative iff for x, y being Element of X holds x * y = x * (y \ x) )
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x, y being Element of X holds x * y = x * (y \ x) )
A1: ( X is positive-implicative implies for x, y being Element of X holds x * y = x * (y \ x) )
proof
assume A2: X is positive-implicative ; ::_thesis: for x, y being Element of X holds x * y = x * (y \ x)
let x, y be Element of X; ::_thesis: x * y = x * (y \ x)
(y \ x) \ y = (y \ y) \ x by BCIALG_1:7
.= x ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then y \ x <= y by BCIALG_1:def_11;
then x * (y \ x) <= x * y by Th8;
then A3: (x * (y \ x)) \ (x * y) = 0. X by BCIALG_1:def_11;
(x * y) \ x = (x \ x) * (y \ x) by A2, Th47
.= (0. X) * (y \ x) by BCIALG_1:def_5
.= y \ x by Th9 ;
then ((x * y) \ x) \ (y \ x) = 0. X by BCIALG_1:def_5;
then (x * y) \ (x * (y \ x)) = 0. X by Th12;
hence x * y = x * (y \ x) by A3, BCIALG_1:def_7; ::_thesis: verum
end;
( ( for x, y being Element of X holds x * y = x * (y \ x) ) implies X is positive-implicative )
proof
assume A4: for x, y being Element of X holds x * y = x * (y \ x) ; ::_thesis: X is positive-implicative
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
y * y = y * (y \ y) by A4
.= y * (0. X) by BCIALG_1:def_5
.= y by Th9 ;
hence (x \ y) \ y = x \ y by Th12; ::_thesis: verum
end;
hence X is positive-implicative by Def11; ::_thesis: verum
end;
hence ( X is positive-implicative iff for x, y being Element of X holds x * y = x * (y \ x) ) by A1; ::_thesis: verum
end;
theorem Th49: :: BCIALG_4:49
for X being positive-implicative BCK-Algebra_with_Condition(S)
for x, y being Element of X holds x = (x \ y) * (x \ (x \ y))
proof
let X be positive-implicative BCK-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds x = (x \ y) * (x \ (x \ y))
for x, y being Element of X holds x = (x \ y) * (x \ (x \ y))
proof
let x, y be Element of X; ::_thesis: x = (x \ y) * (x \ (x \ y))
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_8 ;
then x \ y <= x by BCIALG_1:def_11;
then x = (x \ y) * x by Th46;
hence x = (x \ y) * (x \ (x \ y)) by Th48; ::_thesis: verum
end;
hence for x, y being Element of X holds x = (x \ y) * (x \ (x \ y)) ; ::_thesis: verum
end;
definition
let IT be non empty BCIStr_1 ;
attrIT is being_SB-1 means :Def12: :: BCIALG_4:def 12
for x being Element of IT holds x * x = x;
attrIT is being_SB-2 means :Def13: :: BCIALG_4:def 13
for x, y being Element of IT holds x * y = y * x;
attrIT is being_SB-4 means :Def14: :: BCIALG_4:def 14
for x, y being Element of IT holds (x \ y) * y = x * y;
end;
:: deftheorem Def12 defines being_SB-1 BCIALG_4:def_12_:_
for IT being non empty BCIStr_1 holds
( IT is being_SB-1 iff for x being Element of IT holds x * x = x );
:: deftheorem Def13 defines being_SB-2 BCIALG_4:def_13_:_
for IT being non empty BCIStr_1 holds
( IT is being_SB-2 iff for x, y being Element of IT holds x * y = y * x );
:: deftheorem Def14 defines being_SB-4 BCIALG_4:def_14_:_
for IT being non empty BCIStr_1 holds
( IT is being_SB-4 iff for x, y being Element of IT holds (x \ y) * y = x * y );
Lm8: ( BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )
proof
thus BCI_S-EXAMPLE is being_SB-1 ::_thesis: ( BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )
proof
let x be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_12 ::_thesis: x * x = x
thus x * x = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI_S-EXAMPLE is being_SB-2 ::_thesis: ( BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )
proof
let x, y be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_13 ::_thesis: x * y = y * x
thus x * y = y * x by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI_S-EXAMPLE is being_SB-4 ::_thesis: ( BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )
proof
let x, y be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_14 ::_thesis: (x \ y) * y = x * y
thus (x \ y) * y = x * y by STRUCT_0:def_10; ::_thesis: verum
end;
thus BCI_S-EXAMPLE is being_I ; ::_thesis: BCI_S-EXAMPLE is with_condition_S
let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_2 ::_thesis: (x \ y) \ z = x \ (y * z)
thus (x \ y) \ z = x \ (y * z) by STRUCT_0:def_10; ::_thesis: verum
end;
registration
cluster BCI_S-EXAMPLE -> being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 ;
coherence
( BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S ) by Lm8;
end;
registration
cluster non empty being_I strict with_condition_S being_SB-1 being_SB-2 being_SB-4 for BCIStr_1 ;
existence
ex b1 being non empty BCIStr_1 st
( b1 is strict & b1 is being_SB-1 & b1 is being_SB-2 & b1 is being_SB-4 & b1 is being_I & b1 is with_condition_S ) by Lm8;
end;
definition
mode semi-Brouwerian-algebra is non empty being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 BCIStr_1 ;
end;
theorem :: BCIALG_4:50
for X being non empty BCIStr_1 holds
( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra )
proof
let X be non empty BCIStr_1 ; ::_thesis: ( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra )
A1: ( X is semi-Brouwerian-algebra implies X is positive-implicative BCK-Algebra_with_Condition(S) )
proof
assume A2: X is semi-Brouwerian-algebra ; ::_thesis: X is positive-implicative BCK-Algebra_with_Condition(S)
A3: 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
A4: x \ y = 0. X and
A5: y \ x = 0. X ; ::_thesis: x = y
A6: x = x * x by A2, Def12
.= (x \ x) * x by A2, Def14
.= (0. X) * x by A2, BCIALG_1:def_5
.= y * x by A2, A5, Def14 ;
y = y * y by A2, Def12
.= (y \ y) * y by A2, Def14
.= y * (y \ y) by A2, Def13
.= y * (0. X) by A2, BCIALG_1:def_5
.= (x \ y) * y by A2, A4, Def13
.= x * y by A2, Def14 ;
hence x = y by A2, A6, Def13; ::_thesis: verum
end;
A7: for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
proof
let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ y
(x \ y) \ z = x \ (y * z) by A2, Def2
.= x \ (z * y) by A2, Def13 ;
hence (x \ y) \ z = (x \ z) \ y by A2, Def2; ::_thesis: verum
end;
A8: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
((x \ y) \ z) \ ((x \ z) \ y) = ((x \ y) \ z) \ ((x \ y) \ z) by A7;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A2, BCIALG_1:def_5; ::_thesis: verum
end;
A9: for x, y being Element of X holds x * y = x * (y \ x)
proof
let x, y be Element of X; ::_thesis: x * y = x * (y \ x)
x * (y \ x) = (y \ x) * x by A2, Def13
.= y * x by A2, Def14 ;
hence x * y = x * (y \ x) by A2, Def13; ::_thesis: verum
end;
A10: for x being Element of X holds x ` = 0. X
proof
let x be Element of X; ::_thesis: x ` = 0. X
(0. X) \ x = (x \ x) \ x by A2, BCIALG_1:def_5
.= x \ (x * x) by A2, Def2
.= x \ x by A2, Def12
.= 0. X by A2, BCIALG_1:def_5 ;
hence x ` = 0. X ; ::_thesis: verum
end;
for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
proof
let x, y, z be Element of X; ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
((x \ y) \ (z \ y)) \ (x \ z) = (x \ (y * (z \ y))) \ (x \ z) by A2, Def2
.= (x \ ((z \ y) * y)) \ (x \ z) by A2, Def13
.= (x \ (z * y)) \ (x \ z) by A2, Def14
.= ((x \ z) \ y) \ (x \ z) by A2, Def2
.= ((x \ z) \ (x \ z)) \ y by A7
.= y ` by A2, BCIALG_1:def_5 ;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A10; ::_thesis: verum
end;
hence X is positive-implicative BCK-Algebra_with_Condition(S) by A2, A10, A3, A8, A9, Th48, BCIALG_1:def_3, BCIALG_1:def_4, BCIALG_1:def_7, BCIALG_1:def_8; ::_thesis: verum
end;
( X is positive-implicative BCK-Algebra_with_Condition(S) implies X is semi-Brouwerian-algebra )
proof
assume A11: X is positive-implicative BCK-Algebra_with_Condition(S) ; ::_thesis: X is semi-Brouwerian-algebra
A12: 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
y * x = y * (x \ y) by A11, Th48;
then x * y = y * (x \ y) by A11, Th7;
hence (x \ y) * y = x * y by A11, Th7; ::_thesis: verum
end;
( ( for x being Element of X holds x * x = x ) & ( for x, y being Element of X holds x * y = y * x ) ) by A11, Th7, Th45;
hence X is semi-Brouwerian-algebra by A11, A12, Def12, Def13, Def14; ::_thesis: verum
end;
hence ( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra ) by A1; ::_thesis: verum
end;
definition
let IT be BCK-Algebra_with_Condition(S);
attrIT is implicative means :Def15: :: BCIALG_4:def 15
for x, y being Element of IT holds x \ (y \ x) = x;
end;
:: deftheorem Def15 defines implicative BCIALG_4:def_15_:_
for IT being BCK-Algebra_with_Condition(S) holds
( IT is implicative iff for x, y being Element of IT holds x \ (y \ x) = x );
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S implicative for BCIStr_1 ;
existence
ex b1 being BCK-Algebra_with_Condition(S) st b1 is implicative
proof
reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ;
IT is implicative
proof
let x, y be Element of IT; :: according to BCIALG_4:def_15 ::_thesis: x \ (y \ x) = x
thus x \ (y \ x) = x by STRUCT_0:def_10; ::_thesis: verum
end;
hence ex b1 being BCK-Algebra_with_Condition(S) st b1 is implicative ; ::_thesis: verum
end;
end;
theorem Th51: :: BCIALG_4:51
for X being BCK-Algebra_with_Condition(S) holds
( X is implicative iff ( X is commutative & X is positive-implicative ) )
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is implicative iff ( X is commutative & X is positive-implicative ) )
thus ( X is implicative implies ( X is commutative & X is positive-implicative ) ) ::_thesis: ( X is commutative & X is positive-implicative implies X is implicative )
proof
assume A1: X is implicative ; ::_thesis: ( X is commutative & X is positive-implicative )
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, Def15; ::_thesis: verum
end;
A3: 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 A4: (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 A4, BCIALG_1:def_7; ::_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, Def15;
hence x \ y = (x \ y) \ y by A1, Def15; ::_thesis: verum
end;
hence ( X is commutative & X is positive-implicative ) by A3, Def9, Def11; ::_thesis: verum
end;
assume that
A5: X is commutative and
A6: X is positive-implicative ; ::_thesis: X is 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
x \ (x \ (x \ (y \ x))) = x \ (y \ x) by BCIALG_1:8;
then A7: x \ (y \ x) = x \ ((y \ x) \ ((y \ x) \ x)) by A5, Def9;
(y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by A6, Def11
.= 0. X by BCIALG_1:def_5 ;
hence x \ (y \ x) = x by A7, BCIALG_1:2; ::_thesis: verum
end;
hence X is implicative by Def15; ::_thesis: verum
end;
theorem :: BCIALG_4:52
for X being BCK-Algebra_with_Condition(S) holds
( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )
proof
let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )
A1: ( X is implicative implies for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )
proof
assume A2: X is implicative ; ::_thesis: for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x))
then A3: X is positive-implicative by Th51;
let x, y, z be Element of X; ::_thesis: x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x))
A4: X is commutative by A2, Th51;
x = (x \ z) * (x \ (x \ z)) by A3, Th49;
then A5: x \ (y \ z) = ((x \ z) * (z \ (z \ x))) \ (y \ z) by A4, Def9;
(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 A6: ((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 A3, Def11
.= (((x \ z) \ z) \ (y \ z)) \ ((x \ z) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def_3 ;
then A7: (x \ y) \ z = (x \ z) \ (y \ z) by A6, BCIALG_1:def_7;
(z \ (z \ x)) \ (y \ z) = (z \ (y \ z)) \ (z \ x) by BCIALG_1:7
.= z \ (z \ x) by A2, Def15 ;
hence x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) by A3, A5, A7, Th47; ::_thesis: verum
end;
( ( for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) implies X is implicative )
proof
assume A8: for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ; ::_thesis: X is 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
x \ (y \ x) = ((x \ y) \ x) * (x \ (x \ x)) by A8
.= ((x \ y) \ x) * (x \ (0. X)) by BCIALG_1:def_5
.= ((x \ y) \ x) * x by BCIALG_1:2
.= ((x \ x) \ y) * x by BCIALG_1:7
.= (y `) * x by BCIALG_1:def_5
.= (0. X) * x by BCIALG_1:def_8 ;
hence x \ (y \ x) = x by Th9; ::_thesis: verum
end;
hence X is implicative by Def15; ::_thesis: verum
end;
hence ( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) by A1; ::_thesis: verum
end;