:: BCIIDEAL semantic presentation begin theorem :: BCIIDEAL:1 for X being BCI-algebra for x, y, z, u being Element of X st x <= y holds u \ (z \ x) <= u \ (z \ y) proof let X be BCI-algebra; ::_thesis: for x, y, z, u being Element of X st x <= y holds u \ (z \ x) <= u \ (z \ y) let x, y, z, u be Element of X; ::_thesis: ( x <= y implies u \ (z \ x) <= u \ (z \ y) ) assume x <= y ; ::_thesis: u \ (z \ x) <= u \ (z \ y) then z \ y <= z \ x by BCIALG_1:5; hence u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; ::_thesis: verum end; theorem :: BCIIDEAL:2 for X being BCI-algebra for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u proof let X be BCI-algebra; ::_thesis: for x, y, z, u being Element of X holds (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u let x, y, z, u be Element of X; ::_thesis: (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u ((x \ (y \ z)) \ (x \ (y \ u))) \ ((y \ u) \ (y \ z)) = 0. X by BCIALG_1:1; then (x \ (y \ z)) \ (x \ (y \ u)) <= (y \ u) \ (y \ z) by BCIALG_1:def_11; then A1: ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= ((y \ u) \ (y \ z)) \ (z \ u) by BCIALG_1:5; ((y \ u) \ (y \ z)) \ (z \ u) = ((y \ u) \ (z \ u)) \ (y \ z) by BCIALG_1:7; then ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) <= 0. X by A1, BCIALG_1:def_3; then (((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u)) \ (0. X) = 0. X by BCIALG_1:def_11; then ((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u) = 0. X by BCIALG_1:2; hence (x \ (y \ z)) \ (x \ (y \ u)) <= z \ u by BCIALG_1:def_11; ::_thesis: verum end; theorem :: BCIIDEAL:3 for X being BCI-algebra for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u proof let X be BCI-algebra; ::_thesis: for x, y, z, u, v being Element of X holds (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u let x, y, z, u, v be Element of X; ::_thesis: (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((y \ (z \ v)) \ (y \ (z \ u))) = 0. X by BCIALG_1:1; then (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= (y \ (z \ v)) \ (y \ (z \ u)) by BCIALG_1:def_11; then A1: ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) <= ((y \ (z \ v)) \ (y \ (z \ u))) \ ((z \ u) \ (z \ v)) by BCIALG_1:5; ((y \ (z \ v)) \ (y \ (z \ u))) \ ((z \ u) \ (z \ v)) = ((y \ (z \ v)) \ ((z \ u) \ (z \ v))) \ (y \ (z \ u)) by BCIALG_1:7; then ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) <= 0. X by A1, BCIALG_1:def_3; then (((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v))) \ (0. X) = 0. X by BCIALG_1:def_11; then ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ ((z \ u) \ (z \ v)) = 0. X by BCIALG_1:2; then (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= (z \ u) \ (z \ v) by BCIALG_1:def_11; then A2: ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u) <= ((z \ u) \ (z \ v)) \ (v \ u) by BCIALG_1:5; ((z \ u) \ (z \ v)) \ (v \ u) = ((z \ u) \ (v \ u)) \ (z \ v) by BCIALG_1:7 .= 0. X by BCIALG_1:def_3 ; then (((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u)) \ (0. X) = 0. X by A2, BCIALG_1:def_11; then ((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u) = 0. X by BCIALG_1:2; hence (x \ (y \ (z \ u))) \ (x \ (y \ (z \ v))) <= v \ u by BCIALG_1:def_11; ::_thesis: verum end; theorem :: BCIIDEAL:4 for X being BCI-algebra for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X proof let X be BCI-algebra; ::_thesis: for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X let x, y be Element of X; ::_thesis: ((0. X) \ (x \ y)) \ (y \ x) = 0. X (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((0. X) \ x) \ (y \ x)) \ ((0. X) \ y) by BCIALG_1:7; then A1: (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) = (((y \ x) `) \ x) \ ((0. X) \ y) by BCIALG_1:7 .= (((y `) \ (x `)) \ x) \ ((0. X) \ y) by BCIALG_1:9 .= (((y `) \ x) \ (x `)) \ ((0. X) \ y) by BCIALG_1:7 .= (((y `) \ x) \ (y `)) \ (x `) by BCIALG_1:7 .= (((y `) \ (y `)) \ x) \ (x `) by BCIALG_1:7 .= (x `) \ (x `) by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_5 ; ((0. X) \ (x \ y)) \ (y \ x) = ((x \ y) `) \ (y \ x) .= ((x `) \ (y `)) \ (y \ x) by BCIALG_1:9 .= (((0. X) \ x) \ ((0. X) \ y)) \ (y \ x) ; hence ((0. X) \ (x \ y)) \ (y \ x) = 0. X by A1; ::_thesis: verum end; definition let X be BCI-algebra; let a be Element of X; func initial_section a -> set equals :: BCIIDEAL:def 1 { x where x is Element of X : x <= a } ; coherence { x where x is Element of X : x <= a } is set ; end; :: deftheorem defines initial_section BCIIDEAL:def_1_:_ for X being BCI-algebra for a being Element of X holds initial_section a = { x where x is Element of X : x <= a } ; theorem Th5: :: BCIIDEAL:5 for X being BCI-algebra for A being Ideal of X for x being Element of X for a being Element of A st x <= a holds x in A proof let X be BCI-algebra; ::_thesis: for A being Ideal of X for x being Element of X for a being Element of A st x <= a holds x in A let A be Ideal of X; ::_thesis: for x being Element of X for a being Element of A st x <= a holds x in A let x be Element of X; ::_thesis: for a being Element of A st x <= a holds x in A let a be Element of A; ::_thesis: ( x <= a implies x in A ) assume x <= a ; ::_thesis: x in A then x \ a = 0. X by BCIALG_1:def_11; then x \ a in A by BCIALG_1:def_18; hence x in A by BCIALG_1:def_18; ::_thesis: verum end; theorem :: BCIIDEAL:6 for X being BCI-algebra for x, a, b being Element of AtomSet X st x is Element of BranchV b holds a \ x = a \ b proof let X be BCI-algebra; ::_thesis: for x, a, b being Element of AtomSet X st x is Element of BranchV b holds a \ x = a \ b set P = AtomSet X; let x, a, b be Element of AtomSet X; ::_thesis: ( x is Element of BranchV b implies a \ x = a \ b ) set B = BranchV b; assume x is Element of BranchV b ; ::_thesis: a \ x = a \ b then x in BranchV b ; then ex x3 being Element of X st ( x = x3 & b <= x3 ) ; then A1: b \ x = 0. X by BCIALG_1:def_11; x in { x1 where x1 is Element of X : x1 is minimal } ; then ex x1 being Element of X st ( x = x1 & x1 is minimal ) ; hence a \ x = a \ b by A1, BCIALG_1:def_14; ::_thesis: verum end; theorem :: BCIIDEAL:7 for X being BCI-algebra for a being Element of X for x, b being Element of AtomSet X st x is Element of BranchV b holds a \ x = a \ b proof let X be BCI-algebra; ::_thesis: for a being Element of X for x, b being Element of AtomSet X st x is Element of BranchV b holds a \ x = a \ b set P = AtomSet X; let a be Element of X; ::_thesis: for x, b being Element of AtomSet X st x is Element of BranchV b holds a \ x = a \ b let x, b be Element of AtomSet X; ::_thesis: ( x is Element of BranchV b implies a \ x = a \ b ) set B = BranchV b; assume x is Element of BranchV b ; ::_thesis: a \ x = a \ b then x in BranchV b ; then ex x3 being Element of X st ( x = x3 & b <= x3 ) ; then A1: b \ x = 0. X by BCIALG_1:def_11; x in { x1 where x1 is Element of X : x1 is minimal } ; then ex x1 being Element of X st ( x = x1 & x1 is minimal ) ; hence a \ x = a \ b by A1, BCIALG_1:def_14; ::_thesis: verum end; theorem :: BCIIDEAL:8 for X being BCI-algebra for A being Ideal of X for a being Element of A holds initial_section a c= A proof let X be BCI-algebra; ::_thesis: for A being Ideal of X for a being Element of A holds initial_section a c= A let A be Ideal of X; ::_thesis: for a being Element of A holds initial_section a c= A let a be Element of A; ::_thesis: initial_section a c= A let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in initial_section a or b in A ) assume b in initial_section a ; ::_thesis: b in A then ex x1 being Element of X st ( b = x1 & x1 <= a ) ; hence b in A by Th5; ::_thesis: verum end; theorem :: BCIIDEAL:9 for X being BCI-algebra st AtomSet X is Ideal of X holds for x being Element of BCK-part X for a being Element of AtomSet X st x \ a in AtomSet X holds x = 0. X proof let X be BCI-algebra; ::_thesis: ( AtomSet X is Ideal of X implies for x being Element of BCK-part X for a being Element of AtomSet X st x \ a in AtomSet X holds x = 0. X ) set B = BCK-part X; set P = AtomSet X; A1: for x being Element of X holds ( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) ) proof let x be Element of X; ::_thesis: ( x in {(0. X)} iff x in (BCK-part X) /\ (AtomSet X) ) ( 0. X in BCK-part X & 0. X in AtomSet X ) by BCIALG_1:19; then 0. X in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def_4; hence ( x in {(0. X)} implies x in (BCK-part X) /\ (AtomSet X) ) by TARSKI:def_1; ::_thesis: ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} ) thus ( x in (BCK-part X) /\ (AtomSet X) implies x in {(0. X)} ) ::_thesis: verum proof assume A2: x in (BCK-part X) /\ (AtomSet X) ; ::_thesis: x in {(0. X)} then x in BCK-part X by XBOOLE_0:def_4; then ex x1 being Element of X st ( x = x1 & 0. X <= x1 ) ; then A3: (0. X) \ x = 0. X by BCIALG_1:def_11; x in { x2 where x2 is Element of X : x2 is minimal } by A2, XBOOLE_0:def_4; then ex x2 being Element of X st ( x = x2 & x2 is minimal ) ; then 0. X = x by A3, BCIALG_1:def_14; hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; end; assume A4: AtomSet X is Ideal of X ; ::_thesis: for x being Element of BCK-part X for a being Element of AtomSet X st x \ a in AtomSet X holds x = 0. X for x being Element of BCK-part X for a being Element of AtomSet X st x \ a in AtomSet X holds x = 0. X proof let x be Element of BCK-part X; ::_thesis: for a being Element of AtomSet X st x \ a in AtomSet X holds x = 0. X let a be Element of AtomSet X; ::_thesis: ( x \ a in AtomSet X implies x = 0. X ) assume x \ a in AtomSet X ; ::_thesis: x = 0. X then x in AtomSet X by A4, BCIALG_1:def_18; then x in (BCK-part X) /\ (AtomSet X) by XBOOLE_0:def_4; then x in {(0. X)} by A1; hence x = 0. X by TARSKI:def_1; ::_thesis: verum end; hence for x being Element of BCK-part X for a being Element of AtomSet X st x \ a in AtomSet X holds x = 0. X ; ::_thesis: verum end; theorem :: BCIIDEAL:10 for X being BCI-algebra st AtomSet X is Ideal of X holds AtomSet X is closed Ideal of X proof let X be BCI-algebra; ::_thesis: ( AtomSet X is Ideal of X implies AtomSet X is closed Ideal of X ) set P = AtomSet X; A1: for x being Element of AtomSet X holds x ` in AtomSet X proof let x be Element of AtomSet X; ::_thesis: x ` in AtomSet X x ` is minimal by BCIALG_2:30; hence x ` in AtomSet X ; ::_thesis: verum end; assume AtomSet X is Ideal of X ; ::_thesis: AtomSet X is closed Ideal of X hence AtomSet X is closed Ideal of X by A1, BCIALG_1:def_19; ::_thesis: verum end; definition let X be BCI-algebra; let I be Ideal of X; attrI is positive means :: BCIIDEAL:def 2 for x being Element of I holds x is positive ; end; :: deftheorem defines positive BCIIDEAL:def_2_:_ for X being BCI-algebra for I being Ideal of X holds ( I is positive iff for x being Element of I holds x is positive ); theorem :: BCIIDEAL:11 for X being BCK-algebra for A, I being Ideal of X holds ( A /\ I = {(0. X)} iff for x being Element of A for y being Element of I holds x \ y = x ) proof let X be BCK-algebra; ::_thesis: for A, I being Ideal of X holds ( A /\ I = {(0. X)} iff for x being Element of A for y being Element of I holds x \ y = x ) let A, I be Ideal of X; ::_thesis: ( A /\ I = {(0. X)} iff for x being Element of A for y being Element of I holds x \ y = x ) thus ( A /\ I = {(0. X)} implies for x being Element of A for y being Element of I holds x \ y = x ) ::_thesis: ( ( for x being Element of A for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} ) proof assume A1: A /\ I = {(0. X)} ; ::_thesis: for x being Element of A for y being Element of I holds x \ y = x let x be Element of A; ::_thesis: for y being Element of I holds x \ y = x let y be Element of I; ::_thesis: x \ y = x (x \ (x \ y)) \ y = 0. X by BCIALG_1:1; then x \ (x \ y) <= y by BCIALG_1:def_11; then A2: x \ (x \ y) in I by Th5; (x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7 .= (x \ y) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ (x \ y) <= x by BCIALG_1:def_11; then x \ (x \ y) in A by Th5; then x \ (x \ y) in {(0. X)} by A1, A2, XBOOLE_0:def_4; then A3: x \ (x \ y) = 0. X by TARSKI:def_1; (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ y = x by A3, BCIALG_1:def_7; ::_thesis: verum end; thus ( ( for x being Element of A for y being Element of I holds x \ y = x ) implies A /\ I = {(0. X)} ) ::_thesis: verum proof assume A4: for x being Element of A for y being Element of I holds x \ y = x ; ::_thesis: A /\ I = {(0. X)} thus A /\ I c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= A /\ I proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ I or x in {(0. X)} ) assume A5: x in A /\ I ; ::_thesis: x in {(0. X)} then reconsider xxx = x as Element of A by XBOOLE_0:def_4; reconsider xx = x as Element of I by A5, XBOOLE_0:def_4; xxx \ xx = xxx by A4; then x = 0. X by BCIALG_1:def_5; hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in A /\ I ) assume x in {(0. X)} ; ::_thesis: x in A /\ I then A6: x = 0. X by TARSKI:def_1; ( 0. X in A & 0. X in I ) by BCIALG_1:def_18; hence x in A /\ I by A6, XBOOLE_0:def_4; ::_thesis: verum end; end; theorem :: BCIIDEAL:12 for X being associative BCI-algebra for A being Ideal of X holds A is closed proof let X be associative BCI-algebra; ::_thesis: for A being Ideal of X holds A is closed let A be Ideal of X; ::_thesis: A is closed for x being Element of A holds x ` in A proof let x be Element of A; ::_thesis: x ` in A (0. X) \ x = x \ (0. X) by BCIALG_1:48 .= x by BCIALG_1:2 ; hence x ` in A ; ::_thesis: verum end; hence A is closed by BCIALG_1:def_19; ::_thesis: verum end; theorem :: BCIIDEAL:13 for X being BCI-algebra for A being Ideal of X st X is quasi-associative holds A is closed proof let X be BCI-algebra; ::_thesis: for A being Ideal of X st X is quasi-associative holds A is closed let A be Ideal of X; ::_thesis: ( X is quasi-associative implies A is closed ) assume A1: X is quasi-associative ; ::_thesis: A is closed for x being Element of A holds x ` in A proof let x be Element of A; ::_thesis: x ` in A x ` <= x by A1, BCIALG_1:71; hence x ` in A by Th5; ::_thesis: verum end; hence A is closed by BCIALG_1:def_19; ::_thesis: verum end; begin definition let X be BCI-algebra; let IT be Ideal of X; attrIT is associative means :Def3: :: BCIIDEAL:def 3 ( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds x in IT ) ); end; :: deftheorem Def3 defines associative BCIIDEAL:def_3_:_ for X being BCI-algebra for IT being Ideal of X holds ( IT is associative iff ( 0. X in IT & ( for x, y, z being Element of X st x \ (y \ z) in IT & y \ z in IT holds x in IT ) ) ); registration let X be BCI-algebra; cluster non empty associative for Ideal of X; existence ex b1 being Ideal of X st b1 is associative proof take Y = {(0. X)}; ::_thesis: ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative ) reconsider YY = Y as Ideal of X by BCIALG_1:43; A1: 0. X in YY by TARSKI:def_1; for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds x = 0. X proof let x, y, z be Element of X; ::_thesis: ( x \ (y \ z) in YY & y \ z in YY implies x = 0. X ) assume ( x \ (y \ z) in YY & y \ z in YY ) ; ::_thesis: x = 0. X then ( x \ (y \ z) = 0. X & y \ z = 0. X ) by TARSKI:def_1; hence x = 0. X by BCIALG_1:2; ::_thesis: verum end; then for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds x in YY by A1; hence ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative ) by A1, Def3; ::_thesis: verum end; end; definition let X be BCI-algebra; mode associative-ideal of X -> non empty Subset of X means :Def4: :: BCIIDEAL:def 4 ( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds x in it ) ); existence ex b1 being non empty Subset of X st ( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & y \ z in b1 holds x in b1 ) ) proof take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds x in X1 ) ) X1 c= the carrier of X ; hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds x in X1 ) ) ; ::_thesis: verum end; end; :: deftheorem Def4 defines associative-ideal BCIIDEAL:def_4_:_ for X being BCI-algebra for b2 being non empty Subset of X holds ( b2 is associative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds x in b2 ) ) ); theorem :: BCIIDEAL:14 for X being BCI-algebra for X1 being non empty Subset of X st X1 is associative-ideal of X holds X1 is Ideal of X proof let X be BCI-algebra; ::_thesis: for X1 being non empty Subset of X st X1 is associative-ideal of X holds X1 is Ideal of X let X1 be non empty Subset of X; ::_thesis: ( X1 is associative-ideal of X implies X1 is Ideal of X ) assume A1: X1 is associative-ideal of X ; ::_thesis: X1 is Ideal of X A2: for x, y being Element of X st x \ y in X1 & y in X1 holds x in X1 proof let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 ) assume ( x \ y in X1 & y in X1 ) ; ::_thesis: x in X1 then ( (x \ y) \ (0. X) in X1 & y \ (0. X) in X1 ) by BCIALG_1:2; hence x in X1 by A1, Def4; ::_thesis: verum end; 0. X in X1 by A1, Def4; hence X1 is Ideal of X by A2, BCIALG_1:def_18; ::_thesis: verum end; theorem Th15: :: BCIIDEAL:15 for X being BCI-algebra for I being Ideal of X holds ( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds x \ (y \ z) in I ) proof let X be BCI-algebra; ::_thesis: for I being Ideal of X holds ( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds x \ (y \ z) in I ) let I be Ideal of X; ::_thesis: ( I is associative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds x \ (y \ z) in I ) thus ( I is associative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I holds x \ (y \ z) in I ) ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds x \ (y \ z) in I ) implies I is associative-ideal of X ) proof assume A1: I is associative-ideal of X ; ::_thesis: for x, y, z being Element of X st (x \ y) \ z in I holds x \ (y \ z) in I let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I implies x \ (y \ z) in I ) assume A2: (x \ y) \ z in I ; ::_thesis: x \ (y \ z) in I (x \ (x \ y)) \ y = 0. X by BCIALG_1:1; then x \ (x \ y) <= y by BCIALG_1:def_11; then (x \ (x \ y)) \ (y \ z) <= y \ (y \ z) by BCIALG_1:5; then A3: ((x \ (x \ y)) \ (y \ z)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5; (y \ (y \ z)) \ z = 0. X by BCIALG_1:1; then (((x \ (x \ y)) \ (y \ z)) \ z) \ (0. X) = 0. X by A3, BCIALG_1:def_11; then ((x \ (x \ y)) \ (y \ z)) \ z = 0. X by BCIALG_1:2; then ((x \ (x \ y)) \ (y \ z)) \ z in I by A1, Def4; then ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:7; hence x \ (y \ z) in I by A1, A2, Def4; ::_thesis: verum end; assume A4: for x, y, z being Element of X st (x \ y) \ z in I holds x \ (y \ z) in I ; ::_thesis: I is associative-ideal of X A5: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x in I proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x in I ) assume that A6: (x \ y) \ z in I and A7: y \ z in I ; ::_thesis: x in I x \ (y \ z) in I by A4, A6; hence x in I by A7, BCIALG_1:def_18; ::_thesis: verum end; 0. X in I by BCIALG_1:def_18; hence I is associative-ideal of X by A5, Def4; ::_thesis: verum end; theorem :: BCIIDEAL:16 for X being BCI-algebra for I being Ideal of X st I is associative-ideal of X holds for x being Element of X holds x \ ((0. X) \ x) in I proof let X be BCI-algebra; ::_thesis: for I being Ideal of X st I is associative-ideal of X holds for x being Element of X holds x \ ((0. X) \ x) in I let I be Ideal of X; ::_thesis: ( I is associative-ideal of X implies for x being Element of X holds x \ ((0. X) \ x) in I ) assume A1: I is associative-ideal of X ; ::_thesis: for x being Element of X holds x \ ((0. X) \ x) in I let x be Element of X; ::_thesis: x \ ((0. X) \ x) in I x \ x = 0. X by BCIALG_1:def_5; then A2: (x \ (0. X)) \ x = 0. X by BCIALG_1:2; 0. X in I by A1, Def4; hence x \ ((0. X) \ x) in I by A1, A2, Th15; ::_thesis: verum end; theorem :: BCIIDEAL:17 for X being BCI-algebra for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds I is closed Ideal of X proof let X be BCI-algebra; ::_thesis: for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds I is closed Ideal of X let I be Ideal of X; ::_thesis: ( ( for x being Element of X holds x \ ((0. X) \ x) in I ) implies I is closed Ideal of X ) assume A1: for x being Element of X holds x \ ((0. X) \ x) in I ; ::_thesis: I is closed Ideal of X for x1 being Element of I holds x1 ` in I proof let x1 be Element of I; ::_thesis: x1 ` in I ((0. X) \ x1) \ x1 = ((0. X) \ ((0. X) \ ((0. X) \ x1))) \ x1 by BCIALG_1:8; then ((0. X) \ x1) \ x1 = ((0. X) \ x1) \ ((0. X) \ ((0. X) \ x1)) by BCIALG_1:7; then ((0. X) \ x1) \ x1 in I by A1; hence x1 ` in I by BCIALG_1:def_18; ::_thesis: verum end; hence I is closed Ideal of X by BCIALG_1:def_19; ::_thesis: verum end; definition let X be BCI-algebra; mode p-ideal of X -> non empty Subset of X means :Def5: :: BCIIDEAL:def 5 ( 0. X in it & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in it & y in it holds x in it ) ); existence ex b1 being non empty Subset of X st ( 0. X in b1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b1 & y in b1 holds x in b1 ) ) proof take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds x in X1 ) ) X1 c= X1 ; hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in X1 & y in X1 holds x in X1 ) ) ; ::_thesis: verum end; end; :: deftheorem Def5 defines p-ideal BCIIDEAL:def_5_:_ for X being BCI-algebra for b2 being non empty Subset of X holds ( b2 is p-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ z) \ (y \ z) in b2 & y in b2 holds x in b2 ) ) ); theorem :: BCIIDEAL:18 for X being BCI-algebra for X1 being non empty Subset of X st X1 is p-ideal of X holds X1 is Ideal of X proof let X be BCI-algebra; ::_thesis: for X1 being non empty Subset of X st X1 is p-ideal of X holds X1 is Ideal of X let X1 be non empty Subset of X; ::_thesis: ( X1 is p-ideal of X implies X1 is Ideal of X ) assume A1: X1 is p-ideal of X ; ::_thesis: X1 is Ideal of X A2: for x, y being Element of X st x \ y in X1 & y in X1 holds x in X1 proof let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 ) assume that A3: x \ y in X1 and A4: y in X1 ; ::_thesis: x in X1 (x \ (0. X)) \ y in X1 by A3, BCIALG_1:2; then (x \ (0. X)) \ (y \ (0. X)) in X1 by BCIALG_1:2; hence x in X1 by A1, A4, Def5; ::_thesis: verum end; 0. X in X1 by A1, Def5; hence X1 is Ideal of X by A2, BCIALG_1:def_18; ::_thesis: verum end; theorem Th19: :: BCIIDEAL:19 for X being BCI-algebra for I being Ideal of X st I is p-ideal of X holds BCK-part X c= I proof let X be BCI-algebra; ::_thesis: for I being Ideal of X st I is p-ideal of X holds BCK-part X c= I let I be Ideal of X; ::_thesis: ( I is p-ideal of X implies BCK-part X c= I ) assume A1: I is p-ideal of X ; ::_thesis: BCK-part X c= I let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BCK-part X or x in I ) assume A2: x in BCK-part X ; ::_thesis: x in I then A3: ex x1 being Element of X st ( x = x1 & 0. X <= x1 ) ; reconsider x = x as Element of X by A2; (0. X) \ x = 0. X by A3, BCIALG_1:def_11; then (0. X) \ ((0. X) \ x) = 0. X by BCIALG_1:2; then A4: (x \ x) \ ((0. X) \ x) = 0. X by BCIALG_1:def_5; 0. X in I by A1, Def5; hence x in I by A1, A4, Def5; ::_thesis: verum end; theorem :: BCIIDEAL:20 for X being BCI-algebra holds BCK-part X is p-ideal of X proof let X be BCI-algebra; ::_thesis: BCK-part X is p-ideal of X set A = BCK-part X; A1: now__::_thesis:_for_x,_y,_z_being_Element_of_X_st_(x_\_z)_\_(y_\_z)_in_BCK-part_X_&_y_in_BCK-part_X_holds_ x_in_BCK-part_X let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in BCK-part X & y in BCK-part X implies x in BCK-part X ) assume that A2: (x \ z) \ (y \ z) in BCK-part X and A3: y in BCK-part X ; ::_thesis: x in BCK-part X ex c being Element of X st ( (x \ z) \ (y \ z) = c & 0. X <= c ) by A2; then ((x \ z) \ (y \ z)) ` = 0. X by BCIALG_1:def_11; then ((x \ z) `) \ ((y \ z) `) = 0. X by BCIALG_1:9; then A4: ((x `) \ (z `)) \ ((y \ z) `) = 0. X by BCIALG_1:9; ex d being Element of X st ( y = d & 0. X <= d ) by A3; then y ` = 0. X by BCIALG_1:def_11; then (((x `) \ (z `)) \ ((0. X) \ (z `))) \ ((x `) \ (0. X)) = ((x `) \ (0. X)) ` by A4, BCIALG_1:9; then (((x `) \ (z `)) \ ((0. X) \ (z `))) \ ((x `) \ (0. X)) = (x `) ` by BCIALG_1:2; then 0. X = (0. X) \ ((0. X) \ x) by BCIALG_1:def_3; then (0. X) \ x = 0. X by BCIALG_1:1; then 0. X <= x by BCIALG_1:def_11; hence x in BCK-part X ; ::_thesis: verum end; (0. X) \ (0. X) = 0. X by BCIALG_1:def_5; then 0. X <= 0. X by BCIALG_1:def_11; then 0. X in BCK-part X ; hence BCK-part X is p-ideal of X by A1, Def5; ::_thesis: verum end; theorem Th21: :: BCIIDEAL:21 for X being BCI-algebra for I being Ideal of X holds ( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds y in I ) proof let X be BCI-algebra; ::_thesis: for I being Ideal of X holds ( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds y in I ) let I be Ideal of X; ::_thesis: ( I is p-ideal of X iff for x, y being Element of X st x in I & x <= y holds y in I ) thus ( I is p-ideal of X implies for x, y being Element of X st x in I & x <= y holds y in I ) ::_thesis: ( ( for x, y being Element of X st x in I & x <= y holds y in I ) implies I is p-ideal of X ) proof assume I is p-ideal of X ; ::_thesis: for x, y being Element of X st x in I & x <= y holds y in I then A1: BCK-part X c= I by Th19; let x, y be Element of X; ::_thesis: ( x in I & x <= y implies y in I ) assume that A2: x in I and A3: x <= y ; ::_thesis: y in I A4: x \ y = 0. X by A3, BCIALG_1:def_11; then (y \ x) ` = x \ y by BCIALG_1:6; then 0. X <= y \ x by A4, BCIALG_1:def_11; then y \ x in BCK-part X ; hence y in I by A2, A1, BCIALG_1:def_18; ::_thesis: verum end; assume A5: for x, y being Element of X st x in I & x <= y holds y in I ; ::_thesis: I is p-ideal of X A6: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds x in I proof let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I ) assume that A7: (x \ z) \ (y \ z) in I and A8: y in I ; ::_thesis: x in I ((x \ z) \ (y \ z)) \ (x \ y) = 0. X by BCIALG_1:def_3; then (x \ z) \ (y \ z) <= x \ y by BCIALG_1:def_11; then x \ y in I by A5, A7; hence x in I by A8, BCIALG_1:def_18; ::_thesis: verum end; 0. X in I by BCIALG_1:def_18; hence I is p-ideal of X by A6, Def5; ::_thesis: verum end; theorem :: BCIIDEAL:22 for X being BCI-algebra for I being Ideal of X holds ( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds x \ y in I ) proof let X be BCI-algebra; ::_thesis: for I being Ideal of X holds ( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds x \ y in I ) let I be Ideal of X; ::_thesis: ( I is p-ideal of X iff for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds x \ y in I ) thus ( I is p-ideal of X implies for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds x \ y in I ) ::_thesis: ( ( for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds x \ y in I ) implies I is p-ideal of X ) proof assume A1: I is p-ideal of X ; ::_thesis: for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds x \ y in I let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I implies x \ y in I ) assume A2: (x \ z) \ (y \ z) in I ; ::_thesis: x \ y in I ((x \ z) \ (y \ z)) \ (x \ y) = 0. X by BCIALG_1:def_3; then (x \ z) \ (y \ z) <= x \ y by BCIALG_1:def_11; hence x \ y in I by A1, A2, Th21; ::_thesis: verum end; assume A3: for x, y, z being Element of X st (x \ z) \ (y \ z) in I holds x \ y in I ; ::_thesis: I is p-ideal of X A4: for x, y, z being Element of X st (x \ z) \ (y \ z) in I & y in I holds x in I proof let x, y, z be Element of X; ::_thesis: ( (x \ z) \ (y \ z) in I & y in I implies x in I ) assume that A5: (x \ z) \ (y \ z) in I and A6: y in I ; ::_thesis: x in I x \ y in I by A3, A5; hence x in I by A6, BCIALG_1:def_18; ::_thesis: verum end; 0. X in I by BCIALG_1:def_18; hence I is p-ideal of X by A4, Def5; ::_thesis: verum end; begin definition let X be BCK-algebra; let IT be Ideal of X; attrIT is commutative means :Def6: :: BCIIDEAL:def 6 for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds x \ (y \ (y \ x)) in IT; end; :: deftheorem Def6 defines commutative BCIIDEAL:def_6_:_ for X being BCK-algebra for IT being Ideal of X holds ( IT is commutative iff for x, y, z being Element of X st (x \ y) \ z in IT & z in IT holds x \ (y \ (y \ x)) in IT ); registration let X be BCK-algebra; cluster non empty commutative for Ideal of X; existence ex b1 being Ideal of X st b1 is commutative proof set X1 = BCK-part X; take BCK-part X ; ::_thesis: ( BCK-part X is Ideal of X & BCK-part X is commutative ) A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds x in BCK-part X proof let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X ) assume that A2: x \ y in BCK-part X and A3: y in BCK-part X ; ::_thesis: x in BCK-part X ex x2 being Element of X st ( y = x2 & 0. X <= x2 ) by A3; then A4: y ` = 0. X by BCIALG_1:def_11; ex x1 being Element of X st ( x \ y = x1 & 0. X <= x1 ) by A2; then (x \ y) ` = 0. X by BCIALG_1:def_11; then (x `) \ (0. X) = 0. X by A4, BCIALG_1:9; then (0. X) \ x = 0. X by BCIALG_1:2; then 0. X <= x by BCIALG_1:def_11; hence x in BCK-part X ; ::_thesis: verum end; A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds x \ (y \ (y \ x)) in BCK-part X proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X ) assume that (x \ y) \ z in BCK-part X and z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X (0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) ` .= 0. X by BCIALG_1:def_8 ; then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11; hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum end; 0. X in BCK-part X by BCIALG_1:19; then BCK-part X is Ideal of X by A1, BCIALG_1:def_18; hence ( BCK-part X is Ideal of X & BCK-part X is commutative ) by A5, Def6; ::_thesis: verum end; end; theorem :: BCIIDEAL:23 for X being BCK-algebra holds BCK-part X is commutative Ideal of X proof let X be BCK-algebra; ::_thesis: BCK-part X is commutative Ideal of X set B = BCK-part X; A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds x in BCK-part X proof let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X ) assume that A2: x \ y in BCK-part X and A3: y in BCK-part X ; ::_thesis: x in BCK-part X ex x1 being Element of X st ( x \ y = x1 & 0. X <= x1 ) by A2; then (x \ y) ` = 0. X by BCIALG_1:def_11; then A4: (x `) \ (y `) = 0. X by BCIALG_1:9; ex x2 being Element of X st ( y = x2 & 0. X <= x2 ) by A3; then (x `) \ (0. X) = 0. X by A4, BCIALG_1:def_11; then (0. X) \ x = 0. X by BCIALG_1:2; then 0. X <= x by BCIALG_1:def_11; hence x in BCK-part X ; ::_thesis: verum end; A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds x \ (y \ (y \ x)) in BCK-part X proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X ) assume that (x \ y) \ z in BCK-part X and z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X (0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) ` .= 0. X by BCIALG_1:def_8 ; then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11; hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum end; 0. X in BCK-part X by BCIALG_1:19; hence BCK-part X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def_18; ::_thesis: verum end; theorem :: BCIIDEAL:24 for X being BCK-algebra st X is p-Semisimple BCI-algebra holds {(0. X)} is commutative Ideal of X proof let X be BCK-algebra; ::_thesis: ( X is p-Semisimple BCI-algebra implies {(0. X)} is commutative Ideal of X ) set X1 = {(0. X)}; A1: {(0. X)} c= the carrier of X proof let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in {(0. X)} or xx in the carrier of X ) assume xx in {(0. X)} ; ::_thesis: xx in the carrier of X then xx = 0. X by TARSKI:def_1; hence xx in the carrier of X ; ::_thesis: verum end; A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds x in {(0. X)} proof set X1 = {(0. X)}; let x, y be Element of X; ::_thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} ) assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; ::_thesis: x in {(0. X)} then ( x \ y = 0. X & y = 0. X ) by TARSKI:def_1; then x = 0. X by BCIALG_1:2; hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; 0. X in {(0. X)} by TARSKI:def_1; then reconsider X1 = {(0. X)} as Ideal of X by A1, A2, BCIALG_1:def_18; assume A3: X is p-Semisimple BCI-algebra ; ::_thesis: {(0. X)} is commutative Ideal of X for x, y, z being Element of X st (x \ y) \ z in X1 & z in X1 holds x \ (y \ (y \ x)) in X1 proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in X1 & z in X1 implies x \ (y \ (y \ x)) in X1 ) assume ( (x \ y) \ z in X1 & z in X1 ) ; ::_thesis: x \ (y \ (y \ x)) in X1 then ( (x \ y) \ z = 0. X & z = 0. X ) by TARSKI:def_1; then A4: x \ y = 0. X by BCIALG_1:2; y is atom by A3, BCIALG_1:52; then x = y by A4, BCIALG_1:def_14; then x \ (y \ (y \ x)) = x \ (x \ (0. X)) by BCIALG_1:def_5; then x \ (y \ (y \ x)) = x \ x by BCIALG_1:2; then x \ (y \ (y \ x)) = 0. X by BCIALG_1:def_5; hence x \ (y \ (y \ x)) in X1 by TARSKI:def_1; ::_thesis: verum end; hence {(0. X)} is commutative Ideal of X by Def6; ::_thesis: verum end; Lm1: for X being BCK-algebra holds the carrier of X c= BCK-part X proof let X be BCK-algebra; ::_thesis: the carrier of X c= BCK-part X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of X or x in BCK-part X ) assume x in the carrier of X ; ::_thesis: x in BCK-part X then consider x1 being Element of X such that A1: x = x1 ; x1 ` = 0. X by BCIALG_1:def_8; then 0. X <= x1 by BCIALG_1:def_11; hence x in BCK-part X by A1; ::_thesis: verum end; theorem Th25: :: BCIIDEAL:25 for X being BCK-algebra holds BCK-part X = the carrier of X proof let X be BCK-algebra; ::_thesis: BCK-part X = the carrier of X the carrier of X c= BCK-part X by Lm1; hence BCK-part X = the carrier of X by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: BCIIDEAL:26 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ y = x \ y ) holds the carrier of X = BCK-part X proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ y = x \ y ) implies the carrier of X = BCK-part X ) assume for X being BCI-algebra for x, y being Element of X holds (x \ y) \ y = x \ y ; ::_thesis: the carrier of X = BCK-part X then X is BCK-algebra by BCIALG_1:13; hence the carrier of X = BCK-part X by Th25; ::_thesis: verum end; theorem :: BCIIDEAL:27 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds x \ (y \ x) = x ) holds the carrier of X = BCK-part X proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds x \ (y \ x) = x ) implies the carrier of X = BCK-part X ) assume for X being BCI-algebra for x, y being Element of X holds x \ (y \ x) = x ; ::_thesis: the carrier of X = BCK-part X then X is BCK-algebra by BCIALG_1:14; hence the carrier of X = BCK-part X by Th25; ::_thesis: verum end; theorem :: BCIIDEAL:28 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds the carrier of X = BCK-part X proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) implies the carrier of X = BCK-part X ) assume for X being BCI-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ; ::_thesis: the carrier of X = BCK-part X then X is BCK-algebra by BCIALG_1:12; hence the carrier of X = BCK-part X by Th25; ::_thesis: verum end; theorem :: BCIIDEAL:29 for X being BCI-algebra st ( for X being BCI-algebra for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds the carrier of X = BCK-part X proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) implies the carrier of X = BCK-part X ) assume for X being BCI-algebra for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ; ::_thesis: the carrier of X = BCK-part X then X is BCK-algebra by BCIALG_1:15; hence the carrier of X = BCK-part X by Th25; ::_thesis: verum end; theorem :: BCIIDEAL:30 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds the carrier of X = BCK-part X proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) implies the carrier of X = BCK-part X ) assume for X being BCI-algebra for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ; ::_thesis: the carrier of X = BCK-part X then X is BCK-algebra by BCIALG_1:16; hence the carrier of X = BCK-part X by Th25; ::_thesis: verum end; theorem :: BCIIDEAL:31 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds the carrier of X = BCK-part X proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) implies the carrier of X = BCK-part X ) assume for X being BCI-algebra for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ; ::_thesis: the carrier of X = BCK-part X then X is BCK-algebra by BCIALG_1:17; hence the carrier of X = BCK-part X by Th25; ::_thesis: verum end; theorem :: BCIIDEAL:32 for X being BCK-algebra holds the carrier of X is commutative Ideal of X proof let X be BCK-algebra; ::_thesis: the carrier of X is commutative Ideal of X set B = BCK-part X; A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds x in BCK-part X proof let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X ) assume that A2: x \ y in BCK-part X and A3: y in BCK-part X ; ::_thesis: x in BCK-part X ex x1 being Element of X st ( x \ y = x1 & 0. X <= x1 ) by A2; then (x \ y) ` = 0. X by BCIALG_1:def_11; then A4: (x `) \ (y `) = 0. X by BCIALG_1:9; ex x2 being Element of X st ( y = x2 & 0. X <= x2 ) by A3; then (x `) \ (0. X) = 0. X by A4, BCIALG_1:def_11; then (0. X) \ x = 0. X by BCIALG_1:2; then 0. X <= x by BCIALG_1:def_11; hence x in BCK-part X ; ::_thesis: verum end; A5: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds x \ (y \ (y \ x)) in BCK-part X proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X ) assume that (x \ y) \ z in BCK-part X and z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X (0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) ` .= 0. X by BCIALG_1:def_8 ; then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11; hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum end; the carrier of X = BCK-part X by Th25; hence the carrier of X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def_18; ::_thesis: verum end; theorem Th33: :: BCIIDEAL:33 for X being BCK-algebra for I being Ideal of X holds ( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I ) proof let X be BCK-algebra; ::_thesis: for I being Ideal of X holds ( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I ) let I be Ideal of X; ::_thesis: ( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I ) thus ( I is commutative Ideal of X implies for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I ) ::_thesis: ( ( for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I ) implies I is commutative Ideal of X ) proof A1: 0. X in I by BCIALG_1:def_18; assume A2: I is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I let x, y be Element of X; ::_thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I ) assume x \ y in I ; ::_thesis: x \ (y \ (y \ x)) in I then (x \ y) \ (0. X) in I by BCIALG_1:2; hence x \ (y \ (y \ x)) in I by A2, A1, Def6; ::_thesis: verum end; assume A3: for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I ; ::_thesis: I is commutative Ideal of X for x, y, z being Element of X st (x \ y) \ z in I & z in I holds x \ (y \ (y \ x)) in I proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & z in I implies x \ (y \ (y \ x)) in I ) assume ( (x \ y) \ z in I & z in I ) ; ::_thesis: x \ (y \ (y \ x)) in I then x \ y in I by BCIALG_1:def_18; hence x \ (y \ (y \ x)) in I by A3; ::_thesis: verum end; hence I is commutative Ideal of X by Def6; ::_thesis: verum end; theorem Th34: :: BCIIDEAL:34 for X being BCK-algebra for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds A is commutative Ideal of X proof let X be BCK-algebra; ::_thesis: for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds A is commutative Ideal of X let I, A be Ideal of X; ::_thesis: ( I c= A & I is commutative Ideal of X implies A is commutative Ideal of X ) assume that A1: I c= A and A2: I is commutative Ideal of X ; ::_thesis: A is commutative Ideal of X for x, y being Element of X st x \ y in A holds x \ (y \ (y \ x)) in A proof let x, y be Element of X; ::_thesis: ( x \ y in A implies x \ (y \ (y \ x)) in A ) A3: for x, y, z, u being Element of X st x <= y holds u \ (z \ x) <= u \ (z \ y) proof let x, y, z, u be Element of X; ::_thesis: ( x <= y implies u \ (z \ x) <= u \ (z \ y) ) assume x <= y ; ::_thesis: u \ (z \ x) <= u \ (z \ y) then z \ y <= z \ x by BCIALG_1:5; hence u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; ::_thesis: verum end; (x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7 .= (x \ y) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ (x \ y) <= x by BCIALG_1:def_11; then y \ (y \ (x \ (x \ y))) <= y \ (y \ x) by A3; then A4: x \ (y \ (y \ x)) <= x \ (y \ (y \ (x \ (x \ y)))) by BCIALG_1:5; (x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then (x \ (x \ y)) \ y in I by BCIALG_1:def_18; then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in I by A2, Th33; then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in A by A1; then A5: (x \ (y \ (y \ (x \ (x \ y))))) \ (x \ y) in A by BCIALG_1:7; assume x \ y in A ; ::_thesis: x \ (y \ (y \ x)) in A then x \ (y \ (y \ (x \ (x \ y)))) in A by A5, BCIALG_1:def_18; hence x \ (y \ (y \ x)) in A by A4, Th5; ::_thesis: verum end; hence A is commutative Ideal of X by Th33; ::_thesis: verum end; theorem Th35: :: BCIIDEAL:35 for X being BCK-algebra holds ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X ) proof let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X ) thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X ) by BCIALG_1:43; ::_thesis: ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) thus ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: verum proof assume A1: {(0. X)} is commutative Ideal of X ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X let I be Ideal of X; ::_thesis: I is commutative Ideal of X for I being Ideal of X holds {(0. X)} c= I proof let I be Ideal of X; ::_thesis: {(0. X)} c= I let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in I ) assume x in {(0. X)} ; ::_thesis: x in I then x = 0. X by TARSKI:def_1; hence x in I by BCIALG_1:def_18; ::_thesis: verum end; hence I is commutative Ideal of X by A1, Th34; ::_thesis: verum end; end; theorem Th36: :: BCIIDEAL:36 for X being BCK-algebra holds ( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra ) proof let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra ) A1: ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) proof assume A2: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) let x, y be Element of X; ::_thesis: x \ y = x \ (y \ (y \ x)) x \ y = x \ (x \ (x \ y)) by BCIALG_1:8 .= x \ (y \ (y \ x)) by A2, BCIALG_3:def_1 ; hence x \ y = x \ (y \ (y \ x)) ; ::_thesis: verum end; thus ( {(0. X)} is commutative Ideal of X implies X is commutative BCK-algebra ) ::_thesis: ( X is commutative BCK-algebra implies {(0. X)} is commutative Ideal of X ) proof assume A3: {(0. X)} is commutative Ideal of X ; ::_thesis: X is commutative BCK-algebra for x, y being Element of X st x <= y holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) ) assume x <= y ; ::_thesis: x = y \ (y \ x) then x \ y = 0. X by BCIALG_1:def_11; then x \ y in {(0. X)} by TARSKI:def_1; then x \ (y \ (y \ x)) in {(0. X)} by A3, Th33; then ( (y \ (y \ x)) \ x = 0. X & x \ (y \ (y \ x)) = 0. X ) by BCIALG_1:1, TARSKI:def_1; hence x = y \ (y \ x) by BCIALG_1:def_7; ::_thesis: verum end; hence X is commutative BCK-algebra by BCIALG_3:5; ::_thesis: verum end; assume X is commutative BCK-algebra ; ::_thesis: {(0. X)} is commutative Ideal of X then for x, y being Element of X st x \ y in {(0. X)} holds x \ (y \ (y \ x)) in {(0. X)} by A1; hence {(0. X)} is commutative Ideal of X by Th33, BCIALG_1:43; ::_thesis: verum end; theorem Th37: :: BCIIDEAL:37 for X being BCK-algebra holds ( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X ) proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X ) thus ( X is commutative BCK-algebra implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies X is commutative BCK-algebra ) proof assume X is commutative BCK-algebra ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X then {(0. X)} is commutative Ideal of X by Th36; hence for I being Ideal of X holds I is commutative Ideal of X by Th35; ::_thesis: verum end; assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: X is commutative BCK-algebra then {(0. X)} is commutative Ideal of X by Th35; hence X is commutative BCK-algebra by Th36; ::_thesis: verum end; theorem :: BCIIDEAL:38 for X being BCK-algebra holds ( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X ) proof let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X ) thus ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X ) proof assume {(0. X)} is commutative Ideal of X ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X then X is commutative BCK-algebra by Th36; hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum end; assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: {(0. X)} is commutative Ideal of X then X is commutative BCK-algebra by Th37; hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum end; theorem :: BCIIDEAL:39 for X being BCK-algebra for I being Ideal of X for x, y being Element of X st x \ (x \ y) in I holds ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) proof let X be BCK-algebra; ::_thesis: for I being Ideal of X for x, y being Element of X st x \ (x \ y) in I holds ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) let I be Ideal of X; ::_thesis: for x, y being Element of X st x \ (x \ y) in I holds ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) let x, y be Element of X; ::_thesis: ( x \ (x \ y) in I implies ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) ) assume A1: x \ (x \ y) in I ; ::_thesis: ( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) (x \ y) \ ((x \ y) \ x) = (x \ y) \ ((x \ x) \ y) by BCIALG_1:7 .= (x \ ((x \ x) \ y)) \ y by BCIALG_1:7 .= (x \ (y `)) \ y by BCIALG_1:def_5 .= (x \ (0. X)) \ y by BCIALG_1:def_8 .= x \ y by BCIALG_1:2 ; hence x \ ((x \ y) \ ((x \ y) \ x)) in I by A1; ::_thesis: ( (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I ) ((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) = 0. X by BCIALG_1:1; then ((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) in I by BCIALG_1:def_18; then (y \ (y \ x)) \ (x \ (0. X)) in I by BCIALG_1:2; hence (y \ (y \ x)) \ x in I by BCIALG_1:2; ::_thesis: (y \ (y \ x)) \ (x \ y) in I ((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) = 0. X by BCIALG_1:1; then (y \ (0. X)) \ (y \ x) <= x \ (0. X) by BCIALG_1:def_11; then ((y \ (0. X)) \ (y \ x)) \ (x \ y) <= (x \ (0. X)) \ (x \ y) by BCIALG_1:5; then (y \ (y \ x)) \ (x \ y) <= (x \ (0. X)) \ (x \ y) by BCIALG_1:2; then (y \ (y \ x)) \ (x \ y) <= x \ (x \ y) by BCIALG_1:2; then ((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) = 0. X by BCIALG_1:def_11; then ((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) in I by BCIALG_1:def_18; hence (y \ (y \ x)) \ (x \ y) in I by A1, BCIALG_1:def_18; ::_thesis: verum end; theorem :: BCIIDEAL:40 for X being BCK-algebra holds ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies {(0. X)} is commutative Ideal of X ) proof assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) then X is commutative BCK-algebra by Th36; hence for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) by BCIALG_3:1; ::_thesis: verum end; assume for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: {(0. X)} is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:1; hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum end; theorem :: BCIIDEAL:41 for X being BCK-algebra holds ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) proof let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies {(0. X)} is commutative Ideal of X ) proof assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) then X is commutative BCK-algebra by Th36; hence for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) by BCIALG_3:3; ::_thesis: verum end; assume for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: {(0. X)} is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:3; hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum end; theorem :: BCIIDEAL:42 for X being BCK-algebra holds ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) proof let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies {(0. X)} is commutative Ideal of X ) proof assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) then X is commutative BCK-algebra by Th36; hence for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) by BCIALG_3:4; ::_thesis: verum end; assume for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: {(0. X)} is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:4; hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum end; theorem :: BCIIDEAL:43 for X being BCK-algebra holds ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds x = y \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X st x <= y holds x = y \ (y \ x) ) thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X st x <= y holds x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds x = y \ (y \ x) ) implies {(0. X)} is commutative Ideal of X ) proof assume {(0. X)} is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x <= y holds x = y \ (y \ x) then X is commutative BCK-algebra by Th36; hence for x, y being Element of X st x <= y holds x = y \ (y \ x) by BCIALG_3:5; ::_thesis: verum end; assume for x, y being Element of X st x <= y holds x = y \ (y \ x) ; ::_thesis: {(0. X)} is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:5; hence {(0. X)} is commutative Ideal of X by Th36; ::_thesis: verum end; theorem :: BCIIDEAL:44 for X being BCK-algebra st {(0. X)} is commutative Ideal of X holds ( ( for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) proof let X be BCK-algebra; ::_thesis: ( {(0. X)} is commutative Ideal of X implies ( ( for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) ) assume {(0. X)} is commutative Ideal of X ; ::_thesis: ( ( for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) then A1: X is commutative BCK-algebra by Th36; hence for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) by BCIALG_3:9; ::_thesis: ( ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) thus for x, y being Element of X st x \ y = x holds y \ x = y by A1, BCIALG_3:7; ::_thesis: ( ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) thus for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x by A1, BCIALG_3:8; ::_thesis: ( ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) thus for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A1, BCIALG_3:10; ::_thesis: for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) thus for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by A1, BCIALG_3:11; ::_thesis: verum end; theorem :: BCIIDEAL:45 for X being BCK-algebra holds ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies for I being Ideal of X holds I is commutative Ideal of X ) proof assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) then X is commutative BCK-algebra by Th37; hence for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) by BCIALG_3:1; ::_thesis: verum end; assume for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:1; hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum end; theorem :: BCIIDEAL:46 for X being BCK-algebra holds ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) proof let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies for I being Ideal of X holds I is commutative Ideal of X ) proof assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) then X is commutative BCK-algebra by Th37; hence for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) by BCIALG_3:3; ::_thesis: verum end; assume for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:3; hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum end; theorem :: BCIIDEAL:47 for X being BCK-algebra holds ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) proof let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies for I being Ideal of X holds I is commutative Ideal of X ) proof assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) then X is commutative BCK-algebra by Th37; hence for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) by BCIALG_3:4; ::_thesis: verum end; assume for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:4; hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum end; theorem :: BCIIDEAL:48 for X being BCK-algebra holds ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X st x <= y holds x = y \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff for x, y being Element of X st x <= y holds x = y \ (y \ x) ) thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies for x, y being Element of X st x <= y holds x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds x = y \ (y \ x) ) implies for I being Ideal of X holds I is commutative Ideal of X ) proof assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: for x, y being Element of X st x <= y holds x = y \ (y \ x) then X is commutative BCK-algebra by Th37; hence for x, y being Element of X st x <= y holds x = y \ (y \ x) by BCIALG_3:5; ::_thesis: verum end; assume for x, y being Element of X st x <= y holds x = y \ (y \ x) ; ::_thesis: for I being Ideal of X holds I is commutative Ideal of X then X is commutative BCK-algebra by BCIALG_3:5; hence for I being Ideal of X holds I is commutative Ideal of X by Th37; ::_thesis: verum end; theorem :: BCIIDEAL:49 for X being BCK-algebra st ( for I being Ideal of X holds I is commutative Ideal of X ) holds ( ( for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) proof let X be BCK-algebra; ::_thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies ( ( for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) ) assume for I being Ideal of X holds I is commutative Ideal of X ; ::_thesis: ( ( for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) then A1: X is commutative BCK-algebra by Th37; hence for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) by BCIALG_3:9; ::_thesis: ( ( for x, y being Element of X st x \ y = x holds y \ x = y ) & ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) thus for x, y being Element of X st x \ y = x holds y \ x = y by A1, BCIALG_3:7; ::_thesis: ( ( for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) thus for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x by A1, BCIALG_3:8; ::_thesis: ( ( for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) ) thus for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A1, BCIALG_3:10; ::_thesis: for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) thus for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by A1, BCIALG_3:11; ::_thesis: verum end; begin definition let X be BCK-algebra; mode implicative-ideal of X -> non empty Subset of X means :Def7: :: BCIIDEAL:def 7 ( 0. X in it & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in it & z in it holds x in it ) ); existence ex b1 being non empty Subset of X st ( 0. X in b1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b1 & z in b1 holds x in b1 ) ) proof take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in X1 & z in X1 holds x in X1 ) ) X1 c= the carrier of X ; hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in X1 & z in X1 holds x in X1 ) ) ; ::_thesis: verum end; end; :: deftheorem Def7 defines implicative-ideal BCIIDEAL:def_7_:_ for X being BCK-algebra for b2 being non empty Subset of X holds ( b2 is implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b2 & z in b2 holds x in b2 ) ) ); theorem Th50: :: BCIIDEAL:50 for X being BCK-algebra for I being Ideal of X holds ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds x in I ) proof let X be BCK-algebra; ::_thesis: for I being Ideal of X holds ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds x in I ) let I be Ideal of X; ::_thesis: ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds x in I ) A1: ( ( for x, y being Element of X st x \ (y \ x) in I holds x in I ) implies I is implicative-ideal of X ) proof assume A2: for x, y being Element of X st x \ (y \ x) in I holds x in I ; ::_thesis: I is implicative-ideal of X A3: for x, y, z being Element of X st (x \ (y \ x)) \ z in I & z in I holds x in I proof let x, y, z be Element of X; ::_thesis: ( (x \ (y \ x)) \ z in I & z in I implies x in I ) assume ( (x \ (y \ x)) \ z in I & z in I ) ; ::_thesis: x in I then x \ (y \ x) in I by BCIALG_1:def_18; hence x in I by A2; ::_thesis: verum end; 0. X in I by BCIALG_1:def_18; hence I is implicative-ideal of X by A3, Def7; ::_thesis: verum end; ( I is implicative-ideal of X implies for x, y being Element of X st x \ (y \ x) in I holds x in I ) proof assume A4: I is implicative-ideal of X ; ::_thesis: for x, y being Element of X st x \ (y \ x) in I holds x in I let x, y be Element of X; ::_thesis: ( x \ (y \ x) in I implies x in I ) assume x \ (y \ x) in I ; ::_thesis: x in I then A5: (x \ (y \ x)) \ (0. X) in I by BCIALG_1:2; thus x in I by A4, A5, Def7; ::_thesis: verum end; hence ( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds x in I ) by A1; ::_thesis: verum end; definition let X be BCK-algebra; mode positive-implicative-ideal of X -> non empty Subset of X means :Def8: :: BCIIDEAL:def 8 ( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & y \ z in it holds x \ z in it ) ); existence ex b1 being non empty Subset of X st ( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & y \ z in b1 holds x \ z in b1 ) ) proof take X1 = the carrier of X; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds x \ z in X1 ) ) X1 c= the carrier of X ; hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y, z being Element of X st (x \ y) \ z in X1 & y \ z in X1 holds x \ z in X1 ) ) ; ::_thesis: verum end; end; :: deftheorem Def8 defines positive-implicative-ideal BCIIDEAL:def_8_:_ for X being BCK-algebra for b2 being non empty Subset of X holds ( b2 is positive-implicative-ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & y \ z in b2 holds x \ z in b2 ) ) ); theorem Th51: :: BCIIDEAL:51 for X being BCK-algebra for I being Ideal of X holds ( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds x \ y in I ) proof let X be BCK-algebra; ::_thesis: for I being Ideal of X holds ( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds x \ y in I ) let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y being Element of X st (x \ y) \ y in I holds x \ y in I ) thus ( I is positive-implicative-ideal of X implies for x, y being Element of X st (x \ y) \ y in I holds x \ y in I ) ::_thesis: ( ( for x, y being Element of X st (x \ y) \ y in I holds x \ y in I ) implies I is positive-implicative-ideal of X ) proof assume A1: I is positive-implicative-ideal of X ; ::_thesis: for x, y being Element of X st (x \ y) \ y in I holds x \ y in I let x, y be Element of X; ::_thesis: ( (x \ y) \ y in I implies x \ y in I ) y \ y = 0. X by BCIALG_1:def_5; then A2: y \ y in I by A1, Def8; assume (x \ y) \ y in I ; ::_thesis: x \ y in I hence x \ y in I by A1, A2, Def8; ::_thesis: verum end; thus ( ( for x, y being Element of X st (x \ y) \ y in I holds x \ y in I ) implies I is positive-implicative-ideal of X ) ::_thesis: verum proof assume A3: for x, y being Element of X st (x \ y) \ y in I holds x \ y in I ; ::_thesis: I is positive-implicative-ideal of X A4: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I ) assume that A5: (x \ y) \ z in I and A6: y \ z in I ; ::_thesis: x \ z in I (((x \ z) \ z) \ ((x \ y) \ z)) \ ((x \ z) \ (x \ y)) = 0. X by BCIALG_1:def_3; then ((x \ z) \ z) \ ((x \ y) \ z) <= (x \ z) \ (x \ y) by BCIALG_1:def_11; then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= ((x \ z) \ (x \ y)) \ (y \ z) by BCIALG_1:5; then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) <= 0. X by BCIALG_1:1; then ((((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X by BCIALG_1:def_11; then (((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z) = 0. X by BCIALG_1:2; then ((x \ z) \ z) \ ((x \ y) \ z) <= y \ z by BCIALG_1:def_11; then ((x \ z) \ z) \ ((x \ y) \ z) in I by A6, Th5; then (x \ z) \ z in I by A5, BCIALG_1:def_18; hence x \ z in I by A3; ::_thesis: verum end; 0. X in I by BCIALG_1:def_18; hence I is positive-implicative-ideal of X by A4, Def8; ::_thesis: verum end; end; theorem Th52: :: BCIIDEAL:52 for X being BCK-algebra for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) holds for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I proof let X be BCK-algebra; ::_thesis: for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) holds for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I let I be Ideal of X; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) implies for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) assume A1: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ; ::_thesis: for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I implies (x \ z) \ (y \ z) in I ) ((x \ (y \ z)) \ (x \ y)) \ (y \ (y \ z)) = 0. X by BCIALG_1:1; then (x \ (y \ z)) \ (x \ y) <= y \ (y \ z) by BCIALG_1:def_11; then A2: ((x \ (y \ z)) \ (x \ y)) \ z <= (y \ (y \ z)) \ z by BCIALG_1:5; (y \ (y \ z)) \ z = (y \ z) \ (y \ z) by BCIALG_1:7; then ((x \ (y \ z)) \ (x \ y)) \ z <= 0. X by A2, BCIALG_1:def_5; then (((x \ (y \ z)) \ (x \ y)) \ z) \ (0. X) = 0. X by BCIALG_1:def_11; then ((x \ (y \ z)) \ (x \ y)) \ z = 0. X by BCIALG_1:2; then A3: ((x \ (y \ z)) \ (x \ y)) \ z in I by BCIALG_1:def_18; assume (x \ y) \ z in I ; ::_thesis: (x \ z) \ (y \ z) in I then (x \ (y \ z)) \ z in I by A1, A3; hence (x \ z) \ (y \ z) in I by BCIALG_1:7; ::_thesis: verum end; theorem Th53: :: BCIIDEAL:53 for X being BCK-algebra for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) holds I is positive-implicative-ideal of X proof let X be BCK-algebra; ::_thesis: for I being Ideal of X st ( for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) holds I is positive-implicative-ideal of X let I be Ideal of X; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) implies I is positive-implicative-ideal of X ) assume A1: for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ; ::_thesis: I is positive-implicative-ideal of X A2: for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in I & y \ z in I implies x \ z in I ) assume that A3: (x \ y) \ z in I and A4: y \ z in I ; ::_thesis: x \ z in I (x \ z) \ (y \ z) in I by A1, A3; hence x \ z in I by A4, BCIALG_1:def_18; ::_thesis: verum end; 0. X in I by BCIALG_1:def_18; hence I is positive-implicative-ideal of X by A2, Def8; ::_thesis: verum end; theorem :: BCIIDEAL:54 for X being BCK-algebra for I being Ideal of X holds ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) proof let X be BCK-algebra; ::_thesis: for I being Ideal of X holds ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) A1: 0. X in I by BCIALG_1:def_18; thus ( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) by Def8; ::_thesis: ( ( for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) implies I is positive-implicative-ideal of X ) assume for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ; ::_thesis: I is positive-implicative-ideal of X hence I is positive-implicative-ideal of X by A1, Def8; ::_thesis: verum end; theorem :: BCIIDEAL:55 for X being BCK-algebra for I being Ideal of X holds ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) proof let X be BCK-algebra; ::_thesis: for I being Ideal of X holds ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) let I be Ideal of X; ::_thesis: ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) ( I is positive-implicative-ideal of X implies for x, y, z being Element of X st (x \ y) \ z in I & y \ z in I holds x \ z in I ) by Def8; hence ( I is positive-implicative-ideal of X iff for x, y, z being Element of X st (x \ y) \ z in I holds (x \ z) \ (y \ z) in I ) by Th52, Th53; ::_thesis: verum end; theorem :: BCIIDEAL:56 for X being BCK-algebra for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds A is positive-implicative-ideal of X proof let X be BCK-algebra; ::_thesis: for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds A is positive-implicative-ideal of X let I, A be Ideal of X; ::_thesis: ( I c= A & I is positive-implicative-ideal of X implies A is positive-implicative-ideal of X ) assume that A1: I c= A and A2: I is positive-implicative-ideal of X ; ::_thesis: A is positive-implicative-ideal of X for x, y being Element of X st (x \ y) \ y in A holds x \ y in A proof let x, y be Element of X; ::_thesis: ( (x \ y) \ y in A implies x \ y in A ) ((x \ ((x \ y) \ y)) \ y) \ y = ((x \ y) \ ((x \ y) \ y)) \ y by BCIALG_1:7 .= ((x \ y) \ y) \ ((x \ y) \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then ((x \ ((x \ y) \ y)) \ y) \ y in I by BCIALG_1:def_18; then (x \ ((x \ y) \ y)) \ y in I by A2, Th51; then A3: (x \ y) \ ((x \ y) \ y) in I by BCIALG_1:7; assume (x \ y) \ y in A ; ::_thesis: x \ y in A hence x \ y in A by A1, A3, BCIALG_1:def_18; ::_thesis: verum end; hence A is positive-implicative-ideal of X by Th51; ::_thesis: verum end; theorem :: BCIIDEAL:57 for X being BCK-algebra for I being Ideal of X st I is implicative-ideal of X holds ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) proof let X be BCK-algebra; ::_thesis: for I being Ideal of X st I is implicative-ideal of X holds ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) let I be Ideal of X; ::_thesis: ( I is implicative-ideal of X implies ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) ) assume A1: I is implicative-ideal of X ; ::_thesis: ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) A2: for x, y being Element of X st x \ y in I holds x \ (y \ (y \ x)) in I proof let x, y be Element of X; ::_thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I ) (x \ (y \ (y \ x))) \ x = (x \ x) \ (y \ (y \ x)) by BCIALG_1:7 .= (y \ (y \ x)) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ (y \ (y \ x)) <= x by BCIALG_1:def_11; then y \ x <= y \ (x \ (y \ (y \ x))) by BCIALG_1:5; then (x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) <= (x \ (y \ (y \ x))) \ (y \ x) by BCIALG_1:5; then A3: ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= ((x \ (y \ (y \ x))) \ (y \ x)) \ (x \ y) by BCIALG_1:5; (x \ (y \ (y \ x))) \ (y \ x) = (x \ (y \ x)) \ (y \ (y \ x)) by BCIALG_1:7; then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= 0. X by A3, BCIALG_1:def_3; then (((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (0. X) = 0. X by BCIALG_1:def_11; then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) = 0. X by BCIALG_1:2; then A4: (x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) <= x \ y by BCIALG_1:def_11; assume x \ y in I ; ::_thesis: x \ (y \ (y \ x)) in I hence x \ (y \ (y \ x)) in I by A1, A4, Th5, Th50; ::_thesis: verum end; for x, y being Element of X st (x \ y) \ y in I holds x \ y in I proof let x, y be Element of X; ::_thesis: ( (x \ y) \ y in I implies x \ y in I ) ((x \ y) \ (x \ (x \ y))) \ ((x \ y) \ y) = 0. X by BCIALG_1:1; then A5: (x \ y) \ (x \ (x \ y)) <= (x \ y) \ y by BCIALG_1:def_11; assume (x \ y) \ y in I ; ::_thesis: x \ y in I hence x \ y in I by A1, A5, Th5, Th50; ::_thesis: verum end; hence ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) by A2, Th33, Th51; ::_thesis: verum end;