:: BCIALG_5 semantic presentation begin definition let X be BCI-algebra; let x, y be Element of X; let m, n be Element of NAT ; func Polynom (m,n,x,y) -> Element of X equals :: BCIALG_5:def 1 (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n; coherence (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n is Element of X ; end; :: deftheorem defines Polynom BCIALG_5:def_1_:_ for X being BCI-algebra for x, y being Element of X for m, n being Element of NAT holds Polynom (m,n,x,y) = (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n; theorem Th1: :: BCIALG_5:1 for X being BCI-algebra for x, y, z being Element of X st x <= y & y <= z holds x <= z proof let X be BCI-algebra; ::_thesis: for x, y, z being Element of X st x <= y & y <= z holds x <= z let x, y, z be Element of X; ::_thesis: ( x <= y & y <= z implies x <= z ) assume ( x <= y & y <= z ) ; ::_thesis: x <= z then ( x \ y = 0. X & y \ z = 0. X ) by BCIALG_1:def_11; hence x \ z = 0. X by BCIALG_1:3; :: according to BCIALG_1:def_11 ::_thesis: verum end; theorem Th2: :: BCIALG_5:2 for X being BCI-algebra for x, y being Element of X st x <= y & y <= x holds x = y proof let X be BCI-algebra; ::_thesis: for x, y being Element of X st x <= y & y <= x holds x = y let x, y be Element of X; ::_thesis: ( x <= y & y <= x implies x = y ) assume ( x <= y & y <= x ) ; ::_thesis: x = y then ( x \ y = 0. X & y \ x = 0. X ) by BCIALG_1:def_11; hence x = y by BCIALG_1:def_7; ::_thesis: verum end; theorem Th3: :: BCIALG_5:3 for n being Element of NAT for X being BCK-algebra for x, y being Element of X holds ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n ) proof let n be Element of NAT ; ::_thesis: for X being BCK-algebra for x, y being Element of X holds ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n ) let X be BCK-algebra; ::_thesis: for x, y being Element of X holds ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n ) let x, y be Element of X; ::_thesis: ( x \ y <= x & (x,y) to_power (n + 1) <= (x,y) to_power n ) (((x,y) to_power n) \ y) \ ((x,y) to_power n) = (((x,y) to_power n) \ ((x,y) to_power n)) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then A1: ((x,y) to_power n) \ y <= (x,y) to_power n by BCIALG_1:def_11; (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 & (x,y) to_power (n + 1) <= (x,y) to_power n ) by A1, BCIALG_1:def_11, BCIALG_2:4; ::_thesis: verum end; theorem Th4: :: BCIALG_5:4 for n being Element of NAT for X being BCK-algebra for x being Element of X holds ((0. X),x) to_power n = 0. X proof let n be Element of NAT ; ::_thesis: for X being BCK-algebra for x being Element of X holds ((0. X),x) to_power n = 0. X let X be BCK-algebra; ::_thesis: for x being Element of X holds ((0. X),x) to_power n = 0. X let x be Element of X; ::_thesis: ((0. X),x) to_power n = 0. X defpred S1[ Element of NAT ] means ( \$1 <= n implies ((0. X),x) to_power \$1 = 0. X ); now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_((0._X),x)_to_power_k_=_0._X_)_&_k_+_1_<=_n_holds_ ((0._X),x)_to_power_(k_+_1)_=_0._X let k be Element of NAT ; ::_thesis: ( ( k <= n implies ((0. X),x) to_power k = 0. X ) & k + 1 <= n implies ((0. X),x) to_power (k + 1) = 0. X ) assume A1: ( k <= n implies ((0. X),x) to_power k = 0. X ) ; ::_thesis: ( k + 1 <= n implies ((0. X),x) to_power (k + 1) = 0. X ) set m = k + 1; assume k + 1 <= n ; ::_thesis: ((0. X),x) to_power (k + 1) = 0. X then ((0. X),x) to_power (k + 1) = x ` by A1, BCIALG_2:4, NAT_1:13 .= 0. X by BCIALG_1:def_8 ; hence ((0. X),x) to_power (k + 1) = 0. X ; ::_thesis: verum end; then A2: for k being Element of NAT st S1[k] holds S1[k + 1] ; A3: S1[ 0 ] by BCIALG_2:1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence ((0. X),x) to_power n = 0. X ; ::_thesis: verum end; theorem Th5: :: BCIALG_5:5 for m, n being Element of NAT for X being BCK-algebra for x, y being Element of X st m >= n holds (x,y) to_power m <= (x,y) to_power n proof let m, n be Element of NAT ; ::_thesis: for X being BCK-algebra for x, y being Element of X st m >= n holds (x,y) to_power m <= (x,y) to_power n let X be BCK-algebra; ::_thesis: for x, y being Element of X st m >= n holds (x,y) to_power m <= (x,y) to_power n let x, y be Element of X; ::_thesis: ( m >= n implies (x,y) to_power m <= (x,y) to_power n ) assume m >= n ; ::_thesis: (x,y) to_power m <= (x,y) to_power n then m - n is Element of NAT by NAT_1:21; then consider k being Element of NAT such that A1: k = m - n ; ((x,y) to_power k) \ x = ((x \ x),y) to_power k by BCIALG_2:7 .= ((0. X),y) to_power k by BCIALG_1:def_5 .= 0. X by Th4 ; then (x,y) to_power k <= x by BCIALG_1:def_11; then (((x,y) to_power k),y) to_power n <= (x,y) to_power n by BCIALG_2:19; then (x,y) to_power (k + n) <= (x,y) to_power n by BCIALG_2:10; hence (x,y) to_power m <= (x,y) to_power n by A1; ::_thesis: verum end; theorem Th6: :: BCIALG_5:6 for m, n being Element of NAT for X being BCK-algebra for x, y being Element of X st m > n & (x,y) to_power n = (x,y) to_power m holds for k being Element of NAT st k >= n holds (x,y) to_power n = (x,y) to_power k proof let m, n be Element of NAT ; ::_thesis: for X being BCK-algebra for x, y being Element of X st m > n & (x,y) to_power n = (x,y) to_power m holds for k being Element of NAT st k >= n holds (x,y) to_power n = (x,y) to_power k let X be BCK-algebra; ::_thesis: for x, y being Element of X st m > n & (x,y) to_power n = (x,y) to_power m holds for k being Element of NAT st k >= n holds (x,y) to_power n = (x,y) to_power k let x, y be Element of X; ::_thesis: ( m > n & (x,y) to_power n = (x,y) to_power m implies for k being Element of NAT st k >= n holds (x,y) to_power n = (x,y) to_power k ) assume that A1: m > n and A2: (x,y) to_power n = (x,y) to_power m ; ::_thesis: for k being Element of NAT st k >= n holds (x,y) to_power n = (x,y) to_power k ( m - n is Element of NAT & m - n > n - n ) by A1, NAT_1:21, XREAL_1:9; then m - n >= 1 by NAT_1:14; then (m - n) + n >= 1 + n by XREAL_1:6; then A3: (x,y) to_power n <= (x,y) to_power (n + 1) by A2, Th5; A4: (x,y) to_power (n + 1) <= (x,y) to_power n by Th3; for k being Element of NAT st k >= n holds (x,y) to_power n = (x,y) to_power k proof let k be Element of NAT ; ::_thesis: ( k >= n implies (x,y) to_power n = (x,y) to_power k ) assume k >= n ; ::_thesis: (x,y) to_power n = (x,y) to_power k then k - n is Element of NAT by NAT_1:21; then consider k1 being Element of NAT such that A5: k1 = k - n ; (x,y) to_power n = (((x,y) to_power n),y) to_power k1 proof defpred S1[ Element of NAT ] means ( \$1 <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power \$1 ); now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_k1_implies_(x,y)_to_power_n_=_(((x,y)_to_power_n),y)_to_power_k_)_&_k_+_1_<=_k1_holds_ (x,y)_to_power_n_=_(((x,y)_to_power_n),y)_to_power_(k_+_1) let k be Element of NAT ; ::_thesis: ( ( k <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power k ) & k + 1 <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1) ) assume A6: ( k <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power k ) ; ::_thesis: ( k + 1 <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1) ) set m = k + 1; A7: (((x,y) to_power n),y) to_power (k + 1) = ((((x,y) to_power n),y) to_power k) \ y by BCIALG_2:4 .= ((((x,y) to_power n) \ y),y) to_power k by BCIALG_2:7 .= (((x,y) to_power (n + 1)),y) to_power k by BCIALG_2:4 .= (((x,y) to_power n),y) to_power k by A4, A3, Th2 ; assume k + 1 <= k1 ; ::_thesis: (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1) hence (x,y) to_power n = (((x,y) to_power n),y) to_power (k + 1) by A6, A7, NAT_1:13; ::_thesis: verum end; then A8: for k being Element of NAT st S1[k] holds S1[k + 1] ; A9: S1[ 0 ] by BCIALG_2:1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A8); hence (x,y) to_power n = (((x,y) to_power n),y) to_power k1 ; ::_thesis: verum end; then (x,y) to_power n = (x,y) to_power (n + k1) by BCIALG_2:10; hence (x,y) to_power n = (x,y) to_power k by A5; ::_thesis: verum end; hence for k being Element of NAT st k >= n holds (x,y) to_power n = (x,y) to_power k ; ::_thesis: verum end; theorem Th7: :: BCIALG_5:7 for X being BCI-algebra for x, y being Element of X holds Polynom (0,0,x,y) = x \ (x \ y) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X holds Polynom (0,0,x,y) = x \ (x \ y) let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) = x \ (x \ y) Polynom (0,0,x,y) = (x,(x \ y)) to_power (0 + 1) by BCIALG_2:1 .= x \ (x \ y) by BCIALG_2:2 ; hence Polynom (0,0,x,y) = x \ (x \ y) ; ::_thesis: verum end; theorem :: BCIALG_5:8 for X being BCI-algebra for x, y being Element of X for m, n being Element of NAT holds Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n proof let X be BCI-algebra; ::_thesis: for x, y being Element of X for m, n being Element of NAT holds Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n let x, y be Element of X; ::_thesis: for m, n being Element of NAT holds Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n let m, n be Element of NAT ; ::_thesis: Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n ((Polynom (0,0,x,y)),(x \ y)) to_power m = ((x \ (x \ y)),(x \ y)) to_power m by Th7 .= ((x,(x \ y)) to_power m) \ (x \ y) by BCIALG_2:7 .= (x,(x \ y)) to_power (m + 1) by BCIALG_2:4 ; hence Polynom (m,n,x,y) = ((((Polynom (0,0,x,y)),(x \ y)) to_power m),(y \ x)) to_power n ; ::_thesis: verum end; theorem Th9: :: BCIALG_5:9 for X being BCI-algebra for x, y being Element of X for m, n being Element of NAT holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X for m, n being Element of NAT holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y) let x, y be Element of X; ::_thesis: for m, n being Element of NAT holds Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y) let m, n be Element of NAT ; ::_thesis: Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y) Polynom ((m + 1),n,x,y) = (((x,(y \ x)) to_power n),(x \ y)) to_power ((m + 1) + 1) by BCIALG_2:11 .= ((((x,(y \ x)) to_power n),(x \ y)) to_power (m + 1)) \ (x \ y) by BCIALG_2:4 .= ((((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n) \ (x \ y) by BCIALG_2:11 ; hence Polynom ((m + 1),n,x,y) = (Polynom (m,n,x,y)) \ (x \ y) ; ::_thesis: verum end; theorem Th10: :: BCIALG_5:10 for X being BCI-algebra for x, y being Element of X for m, n being Element of NAT holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X for m, n being Element of NAT holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) let x, y be Element of X; ::_thesis: for m, n being Element of NAT holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) let m, n be Element of NAT ; ::_thesis: Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) consider f being Function of NAT, the carrier of X such that A1: (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power (n + 1) = f . (n + 1) and A2: f . 0 = (x,(x \ y)) to_power (m + 1) and A3: for k being Element of NAT st k < n + 1 holds f . (k + 1) = (f . k) \ (y \ x) by BCIALG_2:def_1; consider g being Function of NAT, the carrier of X such that A4: (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n = g . n and A5: g . 0 = (x,(x \ y)) to_power (m + 1) and A6: for k being Element of NAT st k < n holds g . (k + 1) = (g . k) \ (y \ x) by BCIALG_2:def_1; defpred S1[ Element of NAT ] means ( \$1 <= n implies f . \$1 = g . \$1 ); now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_f_._k_=_g_._k_)_&_k_+_1_<=_n_holds_ f_._(k_+_1)_=_g_._(k_+_1) let k be Element of NAT ; ::_thesis: ( ( k <= n implies f . k = g . k ) & k + 1 <= n implies f . (k + 1) = g . (k + 1) ) assume A7: ( k <= n implies f . k = g . k ) ; ::_thesis: ( k + 1 <= n implies f . (k + 1) = g . (k + 1) ) set m = k + 1; assume A8: k + 1 <= n ; ::_thesis: f . (k + 1) = g . (k + 1) then k + 1 <= n + 1 by NAT_1:13; then k < n + 1 by NAT_1:13; then A9: f . (k + 1) = (f . k) \ (y \ x) by A3; k < n by A8, NAT_1:13; hence f . (k + 1) = g . (k + 1) by A6, A7, A9; ::_thesis: verum end; then A10: for k being Element of NAT st S1[k] holds S1[k + 1] ; A11: S1[ 0 ] by A2, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A11, A10); then f . n = g . n ; hence Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) by A1, A3, A4, XREAL_1:29; ::_thesis: verum end; theorem :: BCIALG_5:11 for X being BCI-algebra for y, x being Element of X for n being Element of NAT holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y) proof let X be BCI-algebra; ::_thesis: for y, x being Element of X for n being Element of NAT holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y) let y, x be Element of X; ::_thesis: for n being Element of NAT holds Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y) let n be Element of NAT ; ::_thesis: Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y) (y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5; then (y \ (y \ x)) \ x = 0. X by BCIALG_1:7; then y \ (y \ x) <= x by BCIALG_1:def_11; then ((y \ (y \ x)),(x \ y)) to_power (n + 1) <= (x,(x \ y)) to_power (n + 1) by BCIALG_2:19; then ((((y \ (y \ x)),(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:19; then ((((y \ (y \ x)),(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:11; then (((((y,(y \ x)) to_power 1),(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:2; hence Polynom ((n + 1),(n + 1),y,x) <= Polynom (n,(n + 1),x,y) by BCIALG_2:10; ::_thesis: verum end; theorem :: BCIALG_5:12 for X being BCI-algebra for x, y being Element of X for n being Element of NAT holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X for n being Element of NAT holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x) let x, y be Element of X; ::_thesis: for n being Element of NAT holds Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x) let n be Element of NAT ; ::_thesis: Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x) (x \ y) \ (x \ y) = 0. X by BCIALG_1:def_5; then (x \ (x \ y)) \ y = 0. X by BCIALG_1:7; then x \ (x \ y) <= y by BCIALG_1:def_11; then ((x \ (x \ y)),(x \ y)) to_power n <= (y,(x \ y)) to_power n by BCIALG_2:19; then ((((x \ (x \ y)),(x \ y)) to_power n),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power n),(y \ x)) to_power (n + 1) by BCIALG_2:19; then (((((x,(x \ y)) to_power 1),(x \ y)) to_power n),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power n),(y \ x)) to_power (n + 1) by BCIALG_2:2; then (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power n),(y \ x)) to_power (n + 1) by BCIALG_2:10; hence Polynom (n,(n + 1),x,y) <= Polynom (n,n,y,x) by BCIALG_2:11; ::_thesis: verum end; definition let X be BCI-algebra; attrX is quasi-commutative means :Def2: :: BCIALG_5:def 2 ex i, j, m, n being Element of NAT st for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (m,n,y,x); end; :: deftheorem Def2 defines quasi-commutative BCIALG_5:def_2_:_ for X being BCI-algebra holds ( X is quasi-commutative iff ex i, j, m, n being Element of NAT st for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (m,n,y,x) ); registration cluster BCI-EXAMPLE -> quasi-commutative ; coherence BCI-EXAMPLE is quasi-commutative proof for x, y being Element of BCI-EXAMPLE holds Polynom (0,0,x,y) = Polynom (0,0,y,x) by STRUCT_0:def_10; hence BCI-EXAMPLE is quasi-commutative by Def2; ::_thesis: verum end; end; registration cluster non empty being_B being_C being_I being_BCI-4 quasi-commutative for BCIStr_0 ; existence ex b1 being BCI-algebra st b1 is quasi-commutative proof take BCI-EXAMPLE ; ::_thesis: BCI-EXAMPLE is quasi-commutative thus BCI-EXAMPLE is quasi-commutative ; ::_thesis: verum end; end; definition let i, j, m, n be Element of NAT ; mode BCI-algebra of i,j,m,n -> BCI-algebra means :Def3: :: BCIALG_5:def 3 for x, y being Element of it holds Polynom (i,j,x,y) = Polynom (m,n,y,x); existence ex b1 being BCI-algebra st for x, y being Element of b1 holds Polynom (i,j,x,y) = Polynom (m,n,y,x) proof for x, y being Element of BCI-EXAMPLE holds Polynom (i,j,x,y) = Polynom (m,n,y,x) by STRUCT_0:def_10; hence ex b1 being BCI-algebra st for x, y being Element of b1 holds Polynom (i,j,x,y) = Polynom (m,n,y,x) ; ::_thesis: verum end; end; :: deftheorem Def3 defines BCI-algebra BCIALG_5:def_3_:_ for i, j, m, n being Element of NAT for b5 being BCI-algebra holds ( b5 is BCI-algebra of i,j,m,n iff for x, y being Element of b5 holds Polynom (i,j,x,y) = Polynom (m,n,y,x) ); theorem Th13: :: BCIALG_5:13 for X being BCI-algebra for i, j, m, n being Element of NAT holds ( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j ) proof let X be BCI-algebra; ::_thesis: for i, j, m, n being Element of NAT holds ( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j ) let i, j, m, n be Element of NAT ; ::_thesis: ( X is BCI-algebra of i,j,m,n iff X is BCI-algebra of m,n,i,j ) thus ( X is BCI-algebra of i,j,m,n implies X is BCI-algebra of m,n,i,j ) ::_thesis: ( X is BCI-algebra of m,n,i,j implies X is BCI-algebra of i,j,m,n ) proof assume X is BCI-algebra of i,j,m,n ; ::_thesis: X is BCI-algebra of m,n,i,j then for x, y being Element of X holds Polynom (m,n,x,y) = Polynom (i,j,y,x) by Def3; hence X is BCI-algebra of m,n,i,j by Def3; ::_thesis: verum end; assume X is BCI-algebra of m,n,i,j ; ::_thesis: X is BCI-algebra of i,j,m,n then for x, y being Element of X holds Polynom (m,n,y,x) = Polynom (i,j,x,y) by Def3; hence X is BCI-algebra of i,j,m,n by Def3; ::_thesis: verum end; theorem Th14: :: BCIALG_5:14 for i, j, m, n being Element of NAT for X being BCI-algebra of i,j,m,n for k being Element of NAT holds X is BCI-algebra of i + k,j,m,n + k proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCI-algebra of i,j,m,n for k being Element of NAT holds X is BCI-algebra of i + k,j,m,n + k let X be BCI-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCI-algebra of i + k,j,m,n + k let k be Element of NAT ; ::_thesis: X is BCI-algebra of i + k,j,m,n + k for x, y being Element of X holds Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) proof let x, y be Element of X; ::_thesis: Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) A1: ((Polynom (m,n,y,x)),(x \ y)) to_power k = Polynom (m,(n + k),y,x) by BCIALG_2:10; ((Polynom (i,j,x,y)),(x \ y)) to_power k = (((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power k),(y \ x)) to_power j by BCIALG_2:11 .= (((x,(x \ y)) to_power ((i + 1) + k)),(y \ x)) to_power j by BCIALG_2:10 .= Polynom ((i + k),j,x,y) ; hence Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) by A1, Def3; ::_thesis: verum end; hence X is BCI-algebra of i + k,j,m,n + k by Def3; ::_thesis: verum end; theorem :: BCIALG_5:15 for i, j, m, n being Element of NAT for X being BCI-algebra of i,j,m,n for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCI-algebra of i,j,m,n for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n let X be BCI-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCI-algebra of i,j + k,m + k,n let k be Element of NAT ; ::_thesis: X is BCI-algebra of i,j + k,m + k,n for x, y being Element of X holds Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) proof let x, y be Element of X; ::_thesis: Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) A1: ((Polynom (m,n,y,x)),(y \ x)) to_power k = (((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power k),(x \ y)) to_power n by BCIALG_2:11 .= (((y,(y \ x)) to_power ((m + 1) + k)),(x \ y)) to_power n by BCIALG_2:10 .= Polynom ((m + k),n,y,x) ; ((Polynom (i,j,x,y)),(y \ x)) to_power k = Polynom (i,(j + k),x,y) by BCIALG_2:10; hence Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) by A1, Def3; ::_thesis: verum end; hence X is BCI-algebra of i,j + k,m + k,n by Def3; ::_thesis: verum end; registration cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 quasi-commutative for BCIStr_0 ; existence ex b1 being BCK-algebra st b1 is quasi-commutative proof take BCI-EXAMPLE ; ::_thesis: BCI-EXAMPLE is quasi-commutative thus BCI-EXAMPLE is quasi-commutative ; ::_thesis: verum end; end; registration let i, j, m, n be Element of NAT ; cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 for BCI-algebra of i,j,m,n; existence ex b1 being BCI-algebra of i,j,m,n st b1 is being_BCK-5 proof for x, y being Element of BCI-EXAMPLE holds Polynom (i,j,x,y) = Polynom (m,n,y,x) by STRUCT_0:def_10; then reconsider B = BCI-EXAMPLE as BCI-algebra of i,j,m,n by Def3; take B ; ::_thesis: B is being_BCK-5 thus B is being_BCK-5 ; ::_thesis: verum end; end; definition let i, j, m, n be Element of NAT ; mode BCK-algebra of i,j,m,n is being_BCK-5 BCI-algebra of i,j,m,n; end; theorem :: BCIALG_5:16 for X being BCI-algebra for i, j, m, n being Element of NAT holds ( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j ) proof let X be BCI-algebra; ::_thesis: for i, j, m, n being Element of NAT holds ( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j ) let i, j, m, n be Element of NAT ; ::_thesis: ( X is BCK-algebra of i,j,m,n iff X is BCK-algebra of m,n,i,j ) thus ( X is BCK-algebra of i,j,m,n implies X is BCK-algebra of m,n,i,j ) ::_thesis: ( X is BCK-algebra of m,n,i,j implies X is BCK-algebra of i,j,m,n ) proof assume A1: X is BCK-algebra of i,j,m,n ; ::_thesis: X is BCK-algebra of m,n,i,j then for x, y being Element of X holds Polynom (m,n,x,y) = Polynom (i,j,y,x) by Def3; hence X is BCK-algebra of m,n,i,j by A1, Def3; ::_thesis: verum end; assume A2: X is BCK-algebra of m,n,i,j ; ::_thesis: X is BCK-algebra of i,j,m,n then for x, y being Element of X holds Polynom (m,n,y,x) = Polynom (i,j,x,y) by Def3; hence X is BCK-algebra of i,j,m,n by A2, Def3; ::_thesis: verum end; theorem Th17: :: BCIALG_5:17 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k let X be BCK-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCK-algebra of i + k,j,m,n + k let k be Element of NAT ; ::_thesis: X is BCK-algebra of i + k,j,m,n + k for x, y being Element of X holds Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) proof let x, y be Element of X; ::_thesis: Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) A1: ((Polynom (m,n,y,x)),(x \ y)) to_power k = Polynom (m,(n + k),y,x) by BCIALG_2:10; ((Polynom (i,j,x,y)),(x \ y)) to_power k = (((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power k),(y \ x)) to_power j by BCIALG_2:11 .= (((x,(x \ y)) to_power ((i + 1) + k)),(y \ x)) to_power j by BCIALG_2:10 .= Polynom ((i + k),j,x,y) ; hence Polynom ((i + k),j,x,y) = Polynom (m,(n + k),y,x) by A1, Def3; ::_thesis: verum end; hence X is BCK-algebra of i + k,j,m,n + k by Def3; ::_thesis: verum end; theorem Th18: :: BCIALG_5:18 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n for k being Element of NAT holds X is BCK-algebra of i,j + k,m + k,n proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n for k being Element of NAT holds X is BCK-algebra of i,j + k,m + k,n let X be BCK-algebra of i,j,m,n; ::_thesis: for k being Element of NAT holds X is BCK-algebra of i,j + k,m + k,n let k be Element of NAT ; ::_thesis: X is BCK-algebra of i,j + k,m + k,n for x, y being Element of X holds Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) proof let x, y be Element of X; ::_thesis: Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) A1: ((Polynom (m,n,y,x)),(y \ x)) to_power k = (((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power k),(x \ y)) to_power n by BCIALG_2:11 .= (((y,(y \ x)) to_power ((m + 1) + k)),(x \ y)) to_power n by BCIALG_2:10 .= Polynom ((m + k),n,y,x) ; ((Polynom (i,j,x,y)),(y \ x)) to_power k = Polynom (i,(j + k),x,y) by BCIALG_2:10; hence Polynom (i,(j + k),x,y) = Polynom ((m + k),n,y,x) by A1, Def3; ::_thesis: verum end; hence X is BCK-algebra of i,j + k,m + k,n by Def3; ::_thesis: verum end; theorem Th19: :: BCIALG_5:19 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1) proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1) let X be BCK-algebra of i,j,m,n; ::_thesis: for x, y being Element of X holds (x,y) to_power (i + 1) = (x,y) to_power (n + 1) let x, y be Element of X; ::_thesis: (x,y) to_power (i + 1) = (x,y) to_power (n + 1) A1: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then A2: Polynom ((m + 1),n,(x \ y),x) = ((x \ y),(x \ (x \ y))) to_power n by BCIALG_2:5 .= ((x \ (x \ (x \ y))),(x \ (x \ y))) to_power n by BCIALG_1:8 .= (((x,(x \ (x \ y))) to_power 1),(x \ (x \ y))) to_power n by BCIALG_2:2 .= (x,(x \ (x \ y))) to_power (n + 1) by BCIALG_2:10 .= (x,y) to_power (n + 1) by BCIALG_2:8 ; X is BCI-algebra of m,n,i,j by Th13; then A3: X is BCI-algebra of m + 1,n,i,j + 1 by Th14; Polynom (i,(j + 1),x,(x \ y)) = (x,(x \ (x \ y))) to_power (i + 1) by A1, BCIALG_2:5 .= (x,y) to_power (i + 1) by BCIALG_2:8 ; hence (x,y) to_power (i + 1) = (x,y) to_power (n + 1) by A2, A3, Def3; ::_thesis: verum end; theorem Th20: :: BCIALG_5:20 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n for x, y being Element of X holds (x,y) to_power (j + 1) = (x,y) to_power (m + 1) proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n for x, y being Element of X holds (x,y) to_power (j + 1) = (x,y) to_power (m + 1) let X be BCK-algebra of i,j,m,n; ::_thesis: for x, y being Element of X holds (x,y) to_power (j + 1) = (x,y) to_power (m + 1) let x, y be Element of X; ::_thesis: (x,y) to_power (j + 1) = (x,y) to_power (m + 1) A1: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then A2: Polynom ((i + 1),j,(x \ y),x) = ((x \ y),(x \ (x \ y))) to_power j by BCIALG_2:5 .= ((x \ (x \ (x \ y))),(x \ (x \ y))) to_power j by BCIALG_1:8 .= (((x,(x \ (x \ y))) to_power 1),(x \ (x \ y))) to_power j by BCIALG_2:2 .= (x,(x \ (x \ y))) to_power (j + 1) by BCIALG_2:10 .= (x,y) to_power (j + 1) by BCIALG_2:8 ; A3: X is BCI-algebra of i + 1,j,m,n + 1 by Th14; Polynom (m,(n + 1),x,(x \ y)) = (x,(x \ (x \ y))) to_power (m + 1) by A1, BCIALG_2:5 .= (x,y) to_power (m + 1) by BCIALG_2:8 ; hence (x,y) to_power (j + 1) = (x,y) to_power (m + 1) by A2, A3, Def3; ::_thesis: verum end; theorem Th21: :: BCIALG_5:21 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j,j,n proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j,j,n let X be BCK-algebra of i,j,m,n; ::_thesis: X is BCK-algebra of i,j,j,n for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (j,n,y,x) proof let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) = Polynom (j,n,y,x) Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3; hence Polynom (i,j,x,y) = Polynom (j,n,y,x) by Th20; ::_thesis: verum end; hence X is BCK-algebra of i,j,j,n by Def3; ::_thesis: verum end; theorem Th22: :: BCIALG_5:22 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of n,j,m,n let X be BCK-algebra of i,j,m,n; ::_thesis: X is BCK-algebra of n,j,m,n for x, y being Element of X holds Polynom (n,j,x,y) = Polynom (m,n,y,x) proof let x, y be Element of X; ::_thesis: Polynom (n,j,x,y) = Polynom (m,n,y,x) Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3; hence Polynom (n,j,x,y) = Polynom (m,n,y,x) by Th19; ::_thesis: verum end; hence X is BCK-algebra of n,j,m,n by Def3; ::_thesis: verum end; definition let i, j, m, n be Element of NAT ; func min (i,j,m,n) -> ext-real number equals :: BCIALG_5:def 4 min ((min (i,j)),(min (m,n))); correctness coherence min ((min (i,j)),(min (m,n))) is ext-real number ; ; func max (i,j,m,n) -> ext-real number equals :: BCIALG_5:def 5 max ((max (i,j)),(max (m,n))); correctness coherence max ((max (i,j)),(max (m,n))) is ext-real number ; ; end; :: deftheorem defines min BCIALG_5:def_4_:_ for i, j, m, n being Element of NAT holds min (i,j,m,n) = min ((min (i,j)),(min (m,n))); :: deftheorem defines max BCIALG_5:def_5_:_ for i, j, m, n being Element of NAT holds max (i,j,m,n) = max ((max (i,j)),(max (m,n))); theorem :: BCIALG_5:23 for i, j, m, n being Element of NAT holds ( min (i,j,m,n) = i or min (i,j,m,n) = j or min (i,j,m,n) = m or min (i,j,m,n) = n ) proof let i, j, m, n be Element of NAT ; ::_thesis: ( min (i,j,m,n) = i or min (i,j,m,n) = j or min (i,j,m,n) = m or min (i,j,m,n) = n ) A1: ( min (m,n) = m or min (m,n) = n ) by XXREAL_0:15; ( min (i,j) = i or min (i,j) = j ) by XXREAL_0:15; hence ( min (i,j,m,n) = i or min (i,j,m,n) = j or min (i,j,m,n) = m or min (i,j,m,n) = n ) by A1, XXREAL_0:15; ::_thesis: verum end; theorem :: BCIALG_5:24 for i, j, m, n being Element of NAT holds ( max (i,j,m,n) = i or max (i,j,m,n) = j or max (i,j,m,n) = m or max (i,j,m,n) = n ) proof let i, j, m, n be Element of NAT ; ::_thesis: ( max (i,j,m,n) = i or max (i,j,m,n) = j or max (i,j,m,n) = m or max (i,j,m,n) = n ) A1: ( max (m,n) = m or max (m,n) = n ) by XXREAL_0:16; ( max (i,j) = i or max (i,j) = j ) by XXREAL_0:16; hence ( max (i,j,m,n) = i or max (i,j,m,n) = j or max (i,j,m,n) = m or max (i,j,m,n) = n ) by A1, XXREAL_0:16; ::_thesis: verum end; theorem Th25: :: BCIALG_5:25 for i, j, m, n being Element of NAT st i = min (i,j,m,n) holds ( i <= j & i <= m & i <= n ) proof let i, j, m, n be Element of NAT ; ::_thesis: ( i = min (i,j,m,n) implies ( i <= j & i <= m & i <= n ) ) A1: min (m,n) <= n by XXREAL_0:17; assume i = min (i,j,m,n) ; ::_thesis: ( i <= j & i <= m & i <= n ) then A2: ( i <= min (i,j) & i <= min (m,n) ) by XXREAL_0:17; ( min (i,j) <= j & min (m,n) <= m ) by XXREAL_0:17; hence ( i <= j & i <= m & i <= n ) by A2, A1, XXREAL_0:2; ::_thesis: verum end; theorem Th26: :: BCIALG_5:26 for i, j, m, n being Element of NAT holds ( max (i,j,m,n) >= i & max (i,j,m,n) >= j & max (i,j,m,n) >= m & max (i,j,m,n) >= n ) proof let i, j, m, n be Element of NAT ; ::_thesis: ( max (i,j,m,n) >= i & max (i,j,m,n) >= j & max (i,j,m,n) >= m & max (i,j,m,n) >= n ) A1: ( max (m,n) >= m & max (m,n) >= n ) by XXREAL_0:25; A2: ( max (i,j,m,n) >= max (i,j) & max (i,j,m,n) >= max (m,n) ) by XXREAL_0:25; ( max (i,j) >= i & max (i,j) >= j ) by XXREAL_0:25; hence ( max (i,j,m,n) >= i & max (i,j,m,n) >= j & max (i,j,m,n) >= m & max (i,j,m,n) >= n ) by A1, A2, XXREAL_0:2; ::_thesis: verum end; theorem Th27: :: BCIALG_5:27 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = j holds X is BCK-algebra of i,i,i,i proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = j holds X is BCK-algebra of i,i,i,i let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = min (i,j,m,n) & i = j implies X is BCK-algebra of i,i,i,i ) assume A1: i = min (i,j,m,n) ; ::_thesis: ( not i = j or X is BCK-algebra of i,i,i,i ) assume A2: i = j ; ::_thesis: X is BCK-algebra of i,i,i,i A3: for x, y being Element of X holds Polynom (i,i,x,y) <= Polynom (i,i,y,x) proof let x, y be Element of X; ::_thesis: Polynom (i,i,x,y) <= Polynom (i,i,y,x) i <= n by A1, Th25; then A4: (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power i by Th5; i <= m by A1, Th25; then i + 1 <= m + 1 by XREAL_1:6; then A5: (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n by Th5, BCIALG_2:19; Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3; hence Polynom (i,i,x,y) <= Polynom (i,i,y,x) by A2, A5, A4, Th1; ::_thesis: verum end; for x, y being Element of X holds Polynom (i,i,y,x) = Polynom (i,i,x,y) proof let x, y be Element of X; ::_thesis: Polynom (i,i,y,x) = Polynom (i,i,x,y) Polynom (i,i,x,y) <= Polynom (i,i,y,x) by A3; then A6: (Polynom (i,i,x,y)) \ (Polynom (i,i,y,x)) = 0. X by BCIALG_1:def_11; Polynom (i,i,y,x) <= Polynom (i,i,x,y) by A3; then (Polynom (i,i,y,x)) \ (Polynom (i,i,x,y)) = 0. X by BCIALG_1:def_11; hence Polynom (i,i,y,x) = Polynom (i,i,x,y) by A6, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-algebra of i,i,i,i by Def3; ::_thesis: verum end; theorem :: BCIALG_5:28 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i < j & i < n holds X is BCK-algebra of i,i + 1,i,i + 1 proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i < j & i < n holds X is BCK-algebra of i,i + 1,i,i + 1 let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = min (i,j,m,n) & i < j & i < n implies X is BCK-algebra of i,i + 1,i,i + 1 ) assume A1: i = min (i,j,m,n) ; ::_thesis: ( not i < j or not i < n or X is BCK-algebra of i,i + 1,i,i + 1 ) assume that A2: i < j and A3: i < n ; ::_thesis: X is BCK-algebra of i,i + 1,i,i + 1 for x, y being Element of X holds Polynom (i,(i + 1),x,y) = Polynom (i,(i + 1),y,x) proof ( n - i is Element of NAT & n - i > i - i ) by A3, NAT_1:21, XREAL_1:9; then n - i >= 1 by NAT_1:14; then A4: (n - i) + i >= 1 + i by XREAL_1:6; m >= i by A1, Th25; then A5: m + 1 >= i + 1 by XREAL_1:6; ( j - i is Element of NAT & j - i > i - i ) by A2, NAT_1:21, XREAL_1:9; then j - i >= 1 by NAT_1:14; then A6: (j - i) + i >= 1 + i by XREAL_1:6; let x, y be Element of X; ::_thesis: Polynom (i,(i + 1),x,y) = Polynom (i,(i + 1),y,x) A7: i + 1 < n + 1 by A3, XREAL_1:6; (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (n + 1) by Th19; then A8: (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (m + 1) by A7, A5, Th6; A9: ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power (n + 1) ) by Def3, Th19; (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (i + 1) = (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (n + 1) by Th19; then (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (i + 1) = (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j by A7, A6, Th6; hence Polynom (i,(i + 1),x,y) = Polynom (i,(i + 1),y,x) by A7, A8, A9, A4, Th6; ::_thesis: verum end; hence X is BCK-algebra of i,i + 1,i,i + 1 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:29 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = n & i = m holds X is BCK-algebra of i,i,i,i proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = n & i = m holds X is BCK-algebra of i,i,i,i let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = min (i,j,m,n) & i = n & i = m implies X is BCK-algebra of i,i,i,i ) assume A1: i = min (i,j,m,n) ; ::_thesis: ( not i = n or not i = m or X is BCK-algebra of i,i,i,i ) assume A2: ( i = n & i = m ) ; ::_thesis: X is BCK-algebra of i,i,i,i then for x, y being Element of X holds Polynom (i,i,x,y) = Polynom (i,j,y,x) by Def3; then A3: X is BCK-algebra of i,i,i,j by Def3; i = min (i,i,i,j) by A1, A2; hence X is BCK-algebra of i,i,i,i by A3, Th27; ::_thesis: verum end; theorem :: BCIALG_5:30 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i = n & m < j holds X is BCK-algebra of i,m + 1,m,i proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = n & m < j holds X is BCK-algebra of i,m + 1,m,i let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = n & m < j implies X is BCK-algebra of i,m + 1,m,i ) assume that A1: i = n and A2: m < j ; ::_thesis: X is BCK-algebra of i,m + 1,m,i for x, y being Element of X holds Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x) proof ( j - m is Element of NAT & j - m > m - m ) by A2, NAT_1:21, XREAL_1:9; then j - m >= 1 by NAT_1:14; then A3: (j - m) + m >= 1 + m by XREAL_1:6; let x, y be Element of X; ::_thesis: Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x) A4: m + 1 < j + 1 by A2, XREAL_1:6; ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + 1) = (((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (m + 1) ) by Def3, Th20; hence Polynom (i,(m + 1),x,y) = Polynom (m,i,y,x) by A1, A4, A3, Th6; ::_thesis: verum end; hence X is BCK-algebra of i,m + 1,m,i by Def3; ::_thesis: verum end; theorem :: BCIALG_5:31 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i = n holds X is BCK-algebra of i,j,j,i proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = n holds X is BCK-algebra of i,j,j,i let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = n implies X is BCK-algebra of i,j,j,i ) assume i = n ; ::_thesis: X is BCK-algebra of i,j,j,i then reconsider X = X as BCK-algebra of i,j,m,i ; for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (j,i,y,x) proof let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) = Polynom (j,i,y,x) Polynom (i,j,x,y) = Polynom (m,i,y,x) by Def3; hence Polynom (i,j,x,y) = Polynom (j,i,y,x) by Th20; ::_thesis: verum end; hence X is BCK-algebra of i,j,j,i by Def3; ::_thesis: verum end; theorem :: BCIALG_5:32 for i, j, m, n, l, k being Element of NAT for X being BCK-algebra of i,j,m,n st l >= j & k >= n holds X is BCK-algebra of k,l,l,k proof let i, j, m, n, l, k be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st l >= j & k >= n holds X is BCK-algebra of k,l,l,k let X be BCK-algebra of i,j,m,n; ::_thesis: ( l >= j & k >= n implies X is BCK-algebra of k,l,l,k ) assume that A1: l >= j and A2: k >= n ; ::_thesis: X is BCK-algebra of k,l,l,k l - j is Element of NAT by A1, NAT_1:21; then consider t being Element of NAT such that A3: t = l - j ; k - n is Element of NAT by A2, NAT_1:21; then consider t1 being Element of NAT such that A4: t1 = k - n ; X is BCK-algebra of n,j,m,n by Th22; then X is BCK-algebra of n,j,j,n by Th21; then X is BCK-algebra of n + t1,j,j,n + t1 by Th17; then X is BCK-algebra of k,j + t,j + t,k by A4, Th18; hence X is BCK-algebra of k,l,l,k by A3; ::_thesis: verum end; theorem :: BCIALG_5:33 for i, j, m, n, k being Element of NAT for X being BCK-algebra of i,j,m,n st k >= max (i,j,m,n) holds X is BCK-algebra of k,k,k,k proof let i, j, m, n, k be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st k >= max (i,j,m,n) holds X is BCK-algebra of k,k,k,k let X be BCK-algebra of i,j,m,n; ::_thesis: ( k >= max (i,j,m,n) implies X is BCK-algebra of k,k,k,k ) assume A1: k >= max (i,j,m,n) ; ::_thesis: X is BCK-algebra of k,k,k,k max (i,j,m,n) >= n by Th26; then k - n is Element of NAT by A1, NAT_1:21, XXREAL_0:2; then consider t1 being Element of NAT such that A2: t1 = k - n ; max (i,j,m,n) >= j by Th26; then k - j is Element of NAT by A1, NAT_1:21, XXREAL_0:2; then consider t being Element of NAT such that A3: t = k - j ; X is BCK-algebra of n,j,m,n by Th22; then X is BCK-algebra of n,j,j,n by Th21; then X is BCK-algebra of n + t1,j,j,n + t1 by Th17; then X is BCK-algebra of k,j + t,j + t,k by A2, Th18; hence X is BCK-algebra of k,k,k,k by A3; ::_thesis: verum end; theorem :: BCIALG_5:34 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i <= m & j <= n holds X is BCK-algebra of i,j,i,j proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i <= m & j <= n holds X is BCK-algebra of i,j,i,j let X be BCK-algebra of i,j,m,n; ::_thesis: ( i <= m & j <= n implies X is BCK-algebra of i,j,i,j ) assume that A1: i <= m and A2: j <= n ; ::_thesis: X is BCK-algebra of i,j,i,j A3: for x, y being Element of X holds Polynom (i,j,x,y) <= Polynom (i,j,y,x) proof let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) <= Polynom (i,j,y,x) i + 1 <= m + 1 by A1, XREAL_1:6; then A4: (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n by Th5, BCIALG_2:19; ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power j ) by A2, Def3, Th5; hence Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A4, Th1; ::_thesis: verum end; for x, y being Element of X holds Polynom (i,j,y,x) = Polynom (i,j,x,y) proof let x, y be Element of X; ::_thesis: Polynom (i,j,y,x) = Polynom (i,j,x,y) Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A3; then A5: (Polynom (i,j,x,y)) \ (Polynom (i,j,y,x)) = 0. X by BCIALG_1:def_11; Polynom (i,j,y,x) <= Polynom (i,j,x,y) by A3; then (Polynom (i,j,y,x)) \ (Polynom (i,j,x,y)) = 0. X by BCIALG_1:def_11; hence Polynom (i,j,y,x) = Polynom (i,j,x,y) by A5, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-algebra of i,j,i,j by Def3; ::_thesis: verum end; theorem :: BCIALG_5:35 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i <= m & i < n holds X is BCK-algebra of i,j,i,i + 1 proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i <= m & i < n holds X is BCK-algebra of i,j,i,i + 1 let X be BCK-algebra of i,j,m,n; ::_thesis: ( i <= m & i < n implies X is BCK-algebra of i,j,i,i + 1 ) assume that A1: i <= m and A2: i < n ; ::_thesis: X is BCK-algebra of i,j,i,i + 1 for x, y being Element of X holds Polynom (i,j,x,y) = Polynom (i,(i + 1),y,x) proof ( n - i is Element of NAT & n - i > i - i ) by A2, NAT_1:21, XREAL_1:9; then n - i >= 1 by NAT_1:14; then A3: (n - i) + i >= 1 + i by XREAL_1:6; let x, y be Element of X; ::_thesis: Polynom (i,j,x,y) = Polynom (i,(i + 1),y,x) A4: i + 1 < n + 1 by A2, XREAL_1:6; A5: ( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (n + 1) ) by Def3, Th19; ( (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (n + 1) & m + 1 >= i + 1 ) by A1, Th19, XREAL_1:6; then (y,(y \ x)) to_power (i + 1) = (y,(y \ x)) to_power (m + 1) by A4, Th6; hence Polynom (i,j,x,y) = Polynom (i,(i + 1),y,x) by A4, A5, A3, Th6; ::_thesis: verum end; hence X is BCK-algebra of i,j,i,i + 1 by Def3; ::_thesis: verum end; theorem Th36: :: BCIALG_5:36 for X being BCI-algebra for i, j, k being Element of NAT st X is BCI-algebra of i,j,j + k,i + k holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: for i, j, k being Element of NAT st X is BCI-algebra of i,j,j + k,i + k holds X is BCK-algebra let i, j, k be Element of NAT ; ::_thesis: ( X is BCI-algebra of i,j,j + k,i + k implies X is BCK-algebra ) assume A1: X is BCI-algebra of i,j,j + k,i + k ; ::_thesis: X is BCK-algebra for y being Element of X holds (0. X) \ y = 0. X proof let y be Element of X; ::_thesis: (0. X) \ y = 0. X A2: (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) = ((((y,y) to_power (j + k)) \ y),((0. X) \ y)) to_power (i + k) by BCIALG_2:4 .= ((((y \ y),y) to_power (j + k)),((0. X) \ y)) to_power (i + k) by BCIALG_2:7 .= ((((0. X),y) to_power (j + k)),((0. X) \ y)) to_power (i + k) by BCIALG_1:def_5 .= ((((0. X),((0. X) \ y)) to_power (i + k)),y) to_power (j + k) by BCIALG_2:11 .= (((((0. X),(0. X)) to_power (i + k)) \ (((0. X),y) to_power (i + k))),y) to_power (j + k) by BCIALG_2:18 .= (((0. X) \ (((0. X),y) to_power (i + k))),y) to_power (j + k) by BCIALG_2:6 .= (((0. X),y) to_power (j + k)) \ (((0. X),y) to_power (i + k)) by BCIALG_2:7 .= (((((0. X),y) to_power j),y) to_power k) \ (((0. X),y) to_power (i + k)) by BCIALG_2:10 .= (((((0. X),y) to_power j),y) to_power k) \ (((((0. X),y) to_power i),y) to_power k) by BCIALG_2:10 ; A3: (((((0. X),y) to_power j),y) to_power k) \ (((((0. X),y) to_power i),y) to_power k) <= (((0. X),y) to_power j) \ (((0. X),y) to_power i) by BCIALG_2:21; Polynom (i,j,(0. X),y) = Polynom ((j + k),(i + k),y,(0. X)) by A1, Def3; then ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j = (((y,(y \ (0. X))) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_1:2; then ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j = (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_1:2; then A4: ((((0. X),y) to_power j),((0. X) \ y)) to_power (i + 1) = (((y,y) to_power ((j + k) + 1)),((0. X) \ y)) to_power (i + k) by BCIALG_2:11; ((((0. X),y) to_power j),((0. X) \ y)) to_power (i + 1) = ((((0. X),((0. X) \ y)) to_power (i + 1)),y) to_power j by BCIALG_2:11 .= (((((0. X),(0. X)) to_power (i + 1)) \ (((0. X),y) to_power (i + 1))),y) to_power j by BCIALG_2:18 .= (((0. X) \ (((0. X),y) to_power (i + 1))),y) to_power j by BCIALG_2:6 .= (((0. X),y) to_power j) \ (((0. X),y) to_power (i + 1)) by BCIALG_2:7 ; then ((((0. X),y) to_power j) \ (((0. X),y) to_power (i + 1))) \ ((((0. X),y) to_power j) \ (((0. X),y) to_power i)) = 0. X by A4, A2, A3, BCIALG_1:def_11; then (0. X) \ ((((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1))) = 0. X by BCIALG_1:11; then A5: 0. X <= (((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) by BCIALG_1:def_11; (((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) = (((0. X),y) to_power i) \ ((((0. X),y) to_power i) \ y) by BCIALG_2:4 .= (((0. X),y) to_power i) \ ((((0. X) \ y),y) to_power i) by BCIALG_2:7 ; then (((0. X),y) to_power i) \ (((0. X),y) to_power (i + 1)) <= (0. X) \ ((0. X) \ y) by BCIALG_2:21; then 0. X <= (0. X) \ ((0. X) \ y) by A5, Th1; then (0. X) \ ((0. X) \ ((0. X) \ y)) = 0. X by BCIALG_1:def_11; hence (0. X) \ y = 0. X by BCIALG_1:8; ::_thesis: verum end; then for x being Element of X holds x ` = 0. X ; hence X is BCK-algebra by BCIALG_1:def_8; ::_thesis: verum end; theorem Th37: :: BCIALG_5:37 for X being BCI-algebra holds ( X is BCI-algebra of 0 , 0 , 0 , 0 iff X is BCK-algebra of 0 , 0 , 0 , 0 ) proof let X be BCI-algebra; ::_thesis: ( X is BCI-algebra of 0 , 0 , 0 , 0 iff X is BCK-algebra of 0 , 0 , 0 , 0 ) thus ( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 ) ::_thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 ) proof assume A1: X is BCI-algebra of 0 , 0 , 0 , 0 ; ::_thesis: X is BCK-algebra of 0 , 0 , 0 , 0 then X is BCI-algebra of 0 , 0 ,0 + 0,0 + 0 ; then reconsider X = X as BCK-algebra by Th36; for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,0,y,x) by A1, Def3; hence X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum end; thus ( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 ) ; ::_thesis: verum end; theorem Th38: :: BCIALG_5:38 for X being BCI-algebra holds ( X is commutative BCK-algebra iff X is BCI-algebra of 0 , 0 , 0 , 0 ) proof let X be BCI-algebra; ::_thesis: ( X is commutative BCK-algebra iff X is BCI-algebra of 0 , 0 , 0 , 0 ) thus ( X is commutative BCK-algebra implies X is BCI-algebra of 0 , 0 , 0 , 0 ) ::_thesis: ( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is commutative BCK-algebra ) proof assume A1: X is commutative BCK-algebra ; ::_thesis: X is BCI-algebra of 0 , 0 , 0 , 0 for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) = Polynom (0,0,y,x) A2: x \ (x \ y) = y \ (y \ x) by A1, BCIALG_3:def_1; (((x,(x \ y)) to_power 1),(y \ x)) to_power 0 = (x,(x \ y)) to_power 1 by BCIALG_2:1 .= y \ (y \ x) by A2, BCIALG_2:2 .= (y,(y \ x)) to_power 1 by BCIALG_2:2 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ; hence Polynom (0,0,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum end; hence X is BCI-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum end; assume A3: X is BCI-algebra of 0 , 0 , 0 , 0 ; ::_thesis: X is commutative BCK-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x) A4: Polynom (0,0,x,y) = Polynom (0,0,y,x) by A3, Def3; x \ (x \ y) = (x,(x \ y)) to_power 1 by BCIALG_2:2 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by A4, BCIALG_2:1 .= (y,(y \ x)) to_power 1 by BCIALG_2:1 .= y \ (y \ x) by BCIALG_2:2 ; hence x \ (x \ y) = y \ (y \ x) ; ::_thesis: verum end; hence X is commutative BCK-algebra by A3, Th37, BCIALG_3:def_1; ::_thesis: verum end; notation let X be BCI-algebra; synonym p-Semisimple-part X for AtomSet X; end; theorem :: BCIALG_5:39 for X being BCI-algebra for B, P being non empty Subset of X for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds B /\ P = {(0. X)} proof let X be BCI-algebra; ::_thesis: for B, P being non empty Subset of X for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds B /\ P = {(0. X)} let B, P be non empty Subset of X; ::_thesis: for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds B /\ P = {(0. X)} let X be BCI-algebra; ::_thesis: ( B = BCK-part X & P = p-Semisimple-part X implies B /\ P = {(0. X)} ) assume that A1: B = BCK-part X and A2: P = p-Semisimple-part X ; ::_thesis: B /\ P = {(0. X)} thus B /\ P c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= B /\ P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B /\ P or x in {(0. X)} ) assume A3: x in B /\ P ; ::_thesis: x in {(0. X)} then A4: x in P by XBOOLE_0:def_4; A5: x in B by A3, XBOOLE_0:def_4; then A6: ex x1 being Element of X st ( x = x1 & 0. X <= x1 ) by A1; reconsider x = x as Element of X by A1, A5; A7: (0. X) \ x = 0. X by A6, BCIALG_1:def_11; ex x2 being Element of X st ( x = x2 & x2 is minimal ) by A2, A4; then x = 0. X by A7, BCIALG_1:def_14; hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; ( 0. X in BCK-part X & 0. X in p-Semisimple-part X ) by BCIALG_1:19; then 0. X in B /\ P by A1, A2, XBOOLE_0:def_4; then for x being set st x in {(0. X)} holds x in B /\ P by TARSKI:def_1; hence {(0. X)} c= B /\ P by TARSKI:def_3; ::_thesis: verum end; theorem :: BCIALG_5:40 for X being BCI-algebra for P being non empty Subset of X for X being BCI-algebra st P = p-Semisimple-part X holds ( X is BCK-algebra iff P = {(0. X)} ) proof let X be BCI-algebra; ::_thesis: for P being non empty Subset of X for X being BCI-algebra st P = p-Semisimple-part X holds ( X is BCK-algebra iff P = {(0. X)} ) let P be non empty Subset of X; ::_thesis: for X being BCI-algebra st P = p-Semisimple-part X holds ( X is BCK-algebra iff P = {(0. X)} ) let X be BCI-algebra; ::_thesis: ( P = p-Semisimple-part X implies ( X is BCK-algebra iff P = {(0. X)} ) ) assume A1: P = p-Semisimple-part X ; ::_thesis: ( X is BCK-algebra iff P = {(0. X)} ) thus ( X is BCK-algebra implies P = {(0. X)} ) ::_thesis: ( P = {(0. X)} implies X is BCK-algebra ) proof assume A2: X is BCK-algebra ; ::_thesis: P = {(0. X)} thus P c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in {(0. X)} ) assume A3: x in P ; ::_thesis: x in {(0. X)} then A4: ex x1 being Element of X st ( x = x1 & x1 is minimal ) by A1; reconsider x = x as Element of X by A1, A3; (0. X) \ x = x ` .= 0. X by A2, BCIALG_1:def_8 ; then x = 0. X by A4, BCIALG_1:def_14; hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; 0. X in P by A1; then for x being set st x in {(0. X)} holds x in P by TARSKI:def_1; hence {(0. X)} c= P by TARSKI:def_3; ::_thesis: verum end; assume A5: P = {(0. X)} ; ::_thesis: X is BCK-algebra 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 in P by A5, TARSKI:def_1; then (0. X) \ x in P by A1, BCIALG_1:33; hence (0. X) \ x = 0. X by A5, TARSKI:def_1; ::_thesis: verum end; then for x being Element of X holds x ` = 0. X ; hence X is BCK-algebra by BCIALG_1:def_8; ::_thesis: verum end; theorem :: BCIALG_5:41 for X being BCI-algebra for B being non empty Subset of X for X being BCI-algebra st B = BCK-part X holds ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) proof let X be BCI-algebra; ::_thesis: for B being non empty Subset of X for X being BCI-algebra st B = BCK-part X holds ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) let B be non empty Subset of X; ::_thesis: for X being BCI-algebra st B = BCK-part X holds ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) let X be BCI-algebra; ::_thesis: ( B = BCK-part X implies ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) ) assume A1: B = BCK-part X ; ::_thesis: ( X is p-Semisimple BCI-algebra iff B = {(0. X)} ) thus ( X is p-Semisimple BCI-algebra implies B = {(0. X)} ) ::_thesis: ( B = {(0. X)} implies X is p-Semisimple BCI-algebra ) proof assume A2: X is p-Semisimple BCI-algebra ; ::_thesis: B = {(0. X)} thus B c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in {(0. X)} ) assume A3: x in B ; ::_thesis: x in {(0. X)} then A4: ex x1 being Element of X st ( x = x1 & 0. X <= x1 ) by A1; reconsider x = x as Element of X by A1, A3; (x `) ` = x by A2, BCIALG_1:def_26; then (0. X) ` = x by A4, BCIALG_1:def_11; 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 B ) assume A5: x in {(0. X)} ; ::_thesis: x in B then reconsider x = x as Element of X by TARSKI:def_1; x = 0. X by A5, TARSKI:def_1; then x ` = 0. X by BCIALG_1:def_5; then 0. X <= x by BCIALG_1:def_11; hence x in B by A1; ::_thesis: verum end; assume A6: B = {(0. X)} ; ::_thesis: X is p-Semisimple BCI-algebra for x being Element of X holds (x `) ` = x proof let x be Element of X; ::_thesis: (x `) ` = x (0. X) \ (x \ ((0. X) \ ((0. X) \ x))) = ((0. X),(x \ ((0. X) \ ((0. X) \ x)))) to_power 1 by BCIALG_2:2 .= (((0. X),x) to_power 1) \ (((0. X),((0. X) \ ((0. X) \ x))) to_power 1) by BCIALG_2:18 .= (((0. X),x) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:8 .= 0. X by BCIALG_1:def_5 ; then 0. X <= x \ ((0. X) \ ((0. X) \ x)) by BCIALG_1:def_11; then x \ ((0. X) \ ((0. X) \ x)) in B by A1; then A7: x \ ((0. X) \ ((0. X) \ x)) = 0. X by A6, TARSKI:def_1; ((0. X) \ ((0. X) \ x)) \ x = ((0. X) \ x) \ ((0. X) \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; hence (x `) ` = x by A7, BCIALG_1:def_7; ::_thesis: verum end; hence X is p-Semisimple BCI-algebra by BCIALG_1:54; ::_thesis: verum end; theorem Th42: :: BCIALG_5:42 for X being BCI-algebra st X is p-Semisimple BCI-algebra holds X is BCI-algebra of 0 ,1, 0 , 0 proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple BCI-algebra implies X is BCI-algebra of 0 ,1, 0 , 0 ) assume A1: X is p-Semisimple BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1, 0 , 0 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,0,y,x) (((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x \ (x \ y)),(y \ x)) to_power 1 by BCIALG_2:2 .= (y,(y \ x)) to_power 1 by A1, BCIALG_1:def_26 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ; hence Polynom (0,1,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum end; hence X is BCI-algebra of 0 ,1, 0 , 0 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:43 for X being BCI-algebra for n, j, m being Element of NAT st X is p-Semisimple BCI-algebra holds X is BCI-algebra of n + j,n,m,(m + j) + 1 proof let X be BCI-algebra; ::_thesis: for n, j, m being Element of NAT st X is p-Semisimple BCI-algebra holds X is BCI-algebra of n + j,n,m,(m + j) + 1 let n, j, m be Element of NAT ; ::_thesis: ( X is p-Semisimple BCI-algebra implies X is BCI-algebra of n + j,n,m,(m + j) + 1 ) assume A1: X is p-Semisimple BCI-algebra ; ::_thesis: X is BCI-algebra of n + j,n,m,(m + j) + 1 A2: for x, y being Element of X holds Polynom (n,n,x,y) = y proof let x, y be Element of X; ::_thesis: Polynom (n,n,x,y) = y defpred S1[ Element of NAT ] means ( \$1 <= n implies Polynom (\$1,\$1,x,y) = y ); now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_Polynom_(k,k,x,y)_=_y_)_&_k_+_1_<=_n_holds_ Polynom_((k_+_1),(k_+_1),x,y)_=_y let k be Element of NAT ; ::_thesis: ( ( k <= n implies Polynom (k,k,x,y) = y ) & k + 1 <= n implies Polynom ((k + 1),(k + 1),x,y) = y ) assume A3: ( k <= n implies Polynom (k,k,x,y) = y ) ; ::_thesis: ( k + 1 <= n implies Polynom ((k + 1),(k + 1),x,y) = y ) set m = k + 1; A4: Polynom ((k + 1),(k + 1),x,y) = (Polynom (k,(k + 1),x,y)) \ (x \ y) by Th9 .= ((Polynom (k,k,x,y)) \ (y \ x)) \ (x \ y) by Th10 ; assume k + 1 <= n ; ::_thesis: Polynom ((k + 1),(k + 1),x,y) = y then Polynom ((k + 1),(k + 1),x,y) = x \ (x \ y) by A1, A3, A4, BCIALG_1:def_26, NAT_1:13; hence Polynom ((k + 1),(k + 1),x,y) = y by A1, BCIALG_1:def_26; ::_thesis: verum end; then A5: for k being Element of NAT st S1[k] holds S1[k + 1] ; Polynom (0,0,x,y) = x \ (x \ y) by Th7 .= y by A1, BCIALG_1:def_26 ; then A6: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5); hence Polynom (n,n,x,y) = y ; ::_thesis: verum end; A7: for x, y being Element of X holds Polynom (m,(m + 1),x,y) = x proof let x, y be Element of X; ::_thesis: Polynom (m,(m + 1),x,y) = x defpred S1[ Element of NAT ] means ( \$1 <= m implies Polynom (\$1,(\$1 + 1),x,y) = x ); now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_m_implies_Polynom_(k,(k_+_1),x,y)_=_x_)_&_k_+_1_<=_m_holds_ Polynom_((k_+_1),((k_+_1)_+_1),x,y)_=_x let k be Element of NAT ; ::_thesis: ( ( k <= m implies Polynom (k,(k + 1),x,y) = x ) & k + 1 <= m implies Polynom ((k + 1),((k + 1) + 1),x,y) = x ) assume A8: ( k <= m implies Polynom (k,(k + 1),x,y) = x ) ; ::_thesis: ( k + 1 <= m implies Polynom ((k + 1),((k + 1) + 1),x,y) = x ) set l = k + 1; A9: Polynom ((k + 1),((k + 1) + 1),x,y) = (Polynom (k,((k + 1) + 1),x,y)) \ (x \ y) by Th9 .= ((Polynom (k,(k + 1),x,y)) \ (y \ x)) \ (x \ y) by Th10 ; assume k + 1 <= m ; ::_thesis: Polynom ((k + 1),((k + 1) + 1),x,y) = x then Polynom ((k + 1),((k + 1) + 1),x,y) = (x \ (x \ y)) \ (y \ x) by A8, A9, BCIALG_1:7, NAT_1:13 .= y \ (y \ x) by A1, BCIALG_1:def_26 ; hence Polynom ((k + 1),((k + 1) + 1),x,y) = x by A1, BCIALG_1:def_26; ::_thesis: verum end; then A10: for k being Element of NAT st S1[k] holds S1[k + 1] ; Polynom (0,1,x,y) = (Polynom (0,0,x,y)) \ (y \ x) by Th10 .= (x \ (x \ y)) \ (y \ x) by Th7 .= y \ (y \ x) by A1, BCIALG_1:def_26 .= x by A1, BCIALG_1:def_26 ; then A11: S1[ 0 ] ; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A11, A10); hence Polynom (m,(m + 1),x,y) = x ; ::_thesis: verum end; for x, y being Element of X holds Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x) proof let x, y be Element of X; ::_thesis: Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x) defpred S1[ Element of NAT ] means ( \$1 <= j implies Polynom ((n + \$1),n,x,y) = Polynom (m,((m + \$1) + 1),y,x) ); now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_j_implies_Polynom_((n_+_k),n,x,y)_=_Polynom_(m,((m_+_k)_+_1),y,x)_)_&_k_+_1_<=_j_holds_ Polynom_((n_+_(k_+_1)),n,x,y)_=_Polynom_(m,((m_+_(k_+_1))_+_1),y,x) let k be Element of NAT ; ::_thesis: ( ( k <= j implies Polynom ((n + k),n,x,y) = Polynom (m,((m + k) + 1),y,x) ) & k + 1 <= j implies Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) ) assume A12: ( k <= j implies Polynom ((n + k),n,x,y) = Polynom (m,((m + k) + 1),y,x) ) ; ::_thesis: ( k + 1 <= j implies Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) ) set l = k + 1; assume k + 1 <= j ; ::_thesis: Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) then Polynom ((n + (k + 1)),n,x,y) = (Polynom (m,((m + k) + 1),y,x)) \ (x \ y) by A12, Th9, NAT_1:13 .= Polynom (m,(((m + k) + 1) + 1),y,x) by Th10 ; hence Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) ; ::_thesis: verum end; then A13: for k being Element of NAT st S1[k] holds S1[k + 1] ; Polynom ((n + 0),n,x,y) = y by A2 .= Polynom (m,((m + 0) + 1),y,x) by A7 ; then A14: S1[ 0 ] ; for j being Element of NAT holds S1[j] from NAT_1:sch_1(A14, A13); hence Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x) ; ::_thesis: verum end; hence X is BCI-algebra of n + j,n,m,(m + j) + 1 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:44 for X being BCI-algebra st X is associative BCI-algebra holds ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) proof let X be BCI-algebra; ::_thesis: ( X is associative BCI-algebra implies ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) ) assume A1: X is associative BCI-algebra ; ::_thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) for x being Element of X holds (x `) ` = x proof let x be Element of X; ::_thesis: (x `) ` = x x ` = x by A1, BCIALG_1:47; hence (x `) ` = x ; ::_thesis: verum end; then A2: X is p-Semisimple by BCIALG_1:54; for x, y being Element of X holds Polynom (1,0,x,y) = Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (1,0,x,y) = Polynom (0,0,y,x) x \ (x \ y) = y by A2, BCIALG_1:def_26; then A3: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_1:48; (((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 = (x,(x \ y)) to_power 2 by BCIALG_2:1 .= (x \ (x \ y)) \ (x \ y) by BCIALG_2:3 .= (y,(y \ x)) to_power 1 by A3, BCIALG_2:2 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ; hence Polynom (1,0,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum end; hence ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) by A2, Def3, Th42; ::_thesis: verum end; theorem :: BCIALG_5:45 for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds X is BCI-algebra of 0 ,1,1,1 proof let X be BCI-algebra; ::_thesis: ( X is weakly-positive-implicative BCI-algebra implies X is BCI-algebra of 0 ,1,1,1 ) assume A1: X is weakly-positive-implicative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1,1,1 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (1,1,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (1,1,y,x) A2: (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by A1, BCIALG_1:85; (((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2 .= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2 .= (((y \ (y \ x)) \ (y \ x)),(x \ y)) to_power 1 by A2, BCIALG_2:2 .= (((y,(y \ x)) to_power 2),(x \ y)) to_power 1 by BCIALG_2:3 ; hence Polynom (0,1,x,y) = Polynom (1,1,y,x) ; ::_thesis: verum end; hence X is BCI-algebra of 0 ,1,1,1 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:46 for X being BCI-algebra st X is positive-implicative BCI-algebra holds X is BCI-algebra of 0 ,1,1,1 proof let X be BCI-algebra; ::_thesis: ( X is positive-implicative BCI-algebra implies X is BCI-algebra of 0 ,1,1,1 ) assume A1: X is positive-implicative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1,1,1 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (1,1,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (1,1,y,x) A2: (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by A1, BCIALG_1:85; (((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2 .= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2 .= (((y \ (y \ x)) \ (y \ x)),(x \ y)) to_power 1 by A2, BCIALG_2:2 .= (((y,(y \ x)) to_power 2),(x \ y)) to_power 1 by BCIALG_2:3 ; hence Polynom (0,1,x,y) = Polynom (1,1,y,x) ; ::_thesis: verum end; hence X is BCI-algebra of 0 ,1,1,1 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:47 for X being BCI-algebra st X is implicative BCI-algebra holds X is BCI-algebra of 0 ,1, 0 , 0 proof let X be BCI-algebra; ::_thesis: ( X is implicative BCI-algebra implies X is BCI-algebra of 0 ,1, 0 , 0 ) assume A1: X is implicative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1, 0 , 0 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,0,y,x) A2: (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by A1, BCIALG_1:def_24; (((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x \ (x \ y)),(y \ x)) to_power 1 by BCIALG_2:2 .= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2 .= (y,(y \ x)) to_power 1 by A2, BCIALG_2:2 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ; hence Polynom (0,1,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum end; hence X is BCI-algebra of 0 ,1, 0 , 0 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:48 for X being BCI-algebra st X is alternative BCI-algebra holds X is BCI-algebra of 0 ,1, 0 , 0 proof let X be BCI-algebra; ::_thesis: ( X is alternative BCI-algebra implies X is BCI-algebra of 0 ,1, 0 , 0 ) assume A1: X is alternative BCI-algebra ; ::_thesis: X is BCI-algebra of 0 ,1, 0 , 0 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,0,y,x) A2: (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by A1, BCIALG_1:76; (((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x \ (x \ y)),(y \ x)) to_power 1 by BCIALG_2:2 .= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2 .= (y,(y \ x)) to_power 1 by A2, BCIALG_2:2 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ; hence Polynom (0,1,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum end; hence X is BCI-algebra of 0 ,1, 0 , 0 by Def3; ::_thesis: verum end; theorem Th49: :: BCIALG_5:49 for X being BCI-algebra holds ( X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0 ,1, 0 ,1 ) proof let X be BCI-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff X is BCK-algebra of 0 ,1, 0 ,1 ) thus ( X is BCK-positive-implicative BCK-algebra implies X is BCK-algebra of 0 ,1, 0 ,1 ) ::_thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 implies X is BCK-positive-implicative BCK-algebra ) proof assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x) (x \ y) \ (x \ y) = 0. X by BCIALG_1:def_5; then (x \ (x \ y)) \ y = 0. X by BCIALG_1:7; then A2: x \ (x \ y) <= y by BCIALG_1:def_11; x \ (x \ y) = (x \ (x \ y)) \ (x \ y) by A1, BCIALG_3:28; then x \ (x \ y) <= y \ (x \ y) by A2, BCIALG_1:5; then (x \ (x \ y)) \ (y \ x) <= (y \ (x \ y)) \ (y \ x) by BCIALG_1:5; then A3: (x \ (x \ y)) \ (y \ x) <= (y \ (y \ x)) \ (x \ y) by BCIALG_1:7; (y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5; then (y \ (y \ x)) \ x = 0. X by BCIALG_1:7; then y \ (y \ x) <= x by BCIALG_1:def_11; then A4: (y \ (y \ x)) \ (y \ x) <= x \ (y \ x) by BCIALG_1:5; y \ (y \ x) = (y \ (y \ x)) \ (y \ x) by A1, BCIALG_3:28; then (y \ (y \ x)) \ (x \ y) <= (x \ (y \ x)) \ (x \ y) by A4, BCIALG_1:5; then (y \ (y \ x)) \ (x \ y) <= (x \ (x \ y)) \ (y \ x) by BCIALG_1:7; then A5: (x \ (x \ y)) \ (y \ x) = (y \ (y \ x)) \ (x \ y) by A3, Th2; (((x,(x \ y)) to_power 1),(y \ x)) to_power 1 = ((x,(x \ y)) to_power 1) \ (y \ x) by BCIALG_2:2 .= (x \ (x \ y)) \ (y \ x) by BCIALG_2:2 .= ((y \ (y \ x)),(x \ y)) to_power 1 by A5, BCIALG_2:2 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 1 by BCIALG_2:2 ; hence Polynom (0,1,x,y) = Polynom (0,1,y,x) ; ::_thesis: verum end; hence X is BCK-algebra of 0 ,1, 0 ,1 by A1, Def3; ::_thesis: verum end; assume A6: X is BCK-algebra of 0 ,1, 0 ,1 ; ::_thesis: X is BCK-positive-implicative BCK-algebra for x, y being Element of X holds x \ y = (x \ y) \ y proof let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y A7: Polynom (0,1,x,(x \ y)) = Polynom (0,1,(x \ y),x) by A6, Def3; A8: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by A6, BCIALG_1:def_8 ; then A9: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:2 .= (x \ (x \ (x \ y))) \ y by BCIALG_1:7 .= (x \ y) \ y by BCIALG_1:8 ; A10: (x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x \ y) \ ((x \ y) \ x) by BCIALG_1:8 .= x \ y by A8, BCIALG_1:2 ; (x \ (x \ (x \ y))) \ ((x \ y) \ x) = ((x,(x \ (x \ y))) to_power 1) \ ((x \ y) \ x) by BCIALG_2:2 .= ((((x \ y),((x \ y) \ x)) to_power 1),(x \ (x \ y))) to_power 1 by A7, BCIALG_2:2 .= (((x \ y) \ ((x \ y) \ x)),(x \ (x \ y))) to_power 1 by BCIALG_2:2 .= ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by BCIALG_2:2 ; hence x \ y = (x \ y) \ y by A10, A9; ::_thesis: verum end; hence X is BCK-positive-implicative BCK-algebra by A6, BCIALG_3:28; ::_thesis: verum end; theorem Th50: :: BCIALG_5:50 for X being BCI-algebra holds ( X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1, 0 , 0 , 0 ) proof let X be BCI-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1, 0 , 0 , 0 ) thus ( X is BCK-implicative BCK-algebra implies X is BCK-algebra of 1, 0 , 0 , 0 ) ::_thesis: ( X is BCK-algebra of 1, 0 , 0 , 0 implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: X is BCK-algebra of 1, 0 , 0 , 0 for x, y being Element of X holds Polynom (1,0,x,y) = Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (1,0,x,y) = Polynom (0,0,y,x) A2: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_3:35; (((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 = (x,(x \ y)) to_power 2 by BCIALG_2:1 .= (x \ (x \ y)) \ (x \ y) by BCIALG_2:3 .= (y,(y \ x)) to_power 1 by A2, BCIALG_2:2 .= (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:1 ; hence Polynom (1,0,x,y) = Polynom (0,0,y,x) ; ::_thesis: verum end; hence X is BCK-algebra of 1, 0 , 0 , 0 by A1, Def3; ::_thesis: verum end; assume A3: X is BCK-algebra of 1, 0 , 0 , 0 ; ::_thesis: X is BCK-implicative BCK-algebra for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) A4: Polynom (1,0,x,y) = Polynom (0,0,y,x) by A3, Def3; (x \ (x \ y)) \ (x \ y) = (x,(x \ y)) to_power 2 by BCIALG_2:3 .= (((x,(x \ y)) to_power (1 + 1)),(y \ x)) to_power 0 by BCIALG_2:1 .= (y,(y \ x)) to_power 1 by A4, BCIALG_2:1 .= y \ (y \ x) by BCIALG_2:2 ; hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ; ::_thesis: verum end; hence X is BCK-implicative BCK-algebra by A3, BCIALG_3:35; ::_thesis: verum end; registration cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative -> commutative for BCIStr_0 ; coherence for b1 being BCK-algebra st b1 is BCK-implicative holds b1 is commutative by BCIALG_3:34; cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative -> BCK-positive-implicative for BCIStr_0 ; coherence for b1 being BCK-algebra st b1 is BCK-implicative holds b1 is BCK-positive-implicative by BCIALG_3:34; end; theorem :: BCIALG_5:51 for X being BCI-algebra holds ( X is BCK-algebra of 1, 0 , 0 , 0 iff ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) ) proof let X be BCI-algebra; ::_thesis: ( X is BCK-algebra of 1, 0 , 0 , 0 iff ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) ) thus ( X is BCK-algebra of 1, 0 , 0 , 0 implies ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) ) ::_thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 implies X is BCK-algebra of 1, 0 , 0 , 0 ) proof assume X is BCK-algebra of 1, 0 , 0 , 0 ; ::_thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) then X is BCK-implicative BCK-algebra by Th50; hence ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) by Th38, Th49; ::_thesis: verum end; assume ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) ; ::_thesis: X is BCK-algebra of 1, 0 , 0 , 0 then ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) by Th38, Th49; then X is BCK-implicative BCK-algebra by BCIALG_3:34; hence X is BCK-algebra of 1, 0 , 0 , 0 by Th50; ::_thesis: verum end; theorem :: BCIALG_5:52 for X being quasi-commutative BCK-algebra holds ( X is BCK-algebra of 0 ,1, 0 ,1 iff for x, y being Element of X holds x \ y = (x \ y) \ y ) proof let X be quasi-commutative BCK-algebra; ::_thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 iff for x, y being Element of X holds x \ y = (x \ y) \ y ) thus ( X is BCK-algebra of 0 ,1, 0 ,1 implies for x, y being Element of X holds x \ y = (x \ y) \ y ) ::_thesis: ( ( for x, y being Element of X holds x \ y = (x \ y) \ y ) implies X is BCK-algebra of 0 ,1, 0 ,1 ) proof assume A1: X is BCK-algebra of 0 ,1, 0 ,1 ; ::_thesis: for x, y being Element of X holds x \ y = (x \ y) \ y 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 A2: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then A3: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:2 .= (x \ (x \ (x \ y))) \ y by BCIALG_1:7 .= (x \ y) \ y by BCIALG_1:8 ; A4: (x \ (x \ (x \ y))) \ ((x \ y) \ x) = (x \ y) \ ((x \ y) \ x) by BCIALG_1:8 .= x \ y by A2, BCIALG_1:2 ; A5: Polynom (0,1,x,(x \ y)) = Polynom (0,1,(x \ y),x) by A1, Def3; (x \ (x \ (x \ y))) \ ((x \ y) \ x) = ((x,(x \ (x \ y))) to_power 1) \ ((x \ y) \ x) by BCIALG_2:2 .= ((((x \ y),((x \ y) \ x)) to_power 1),(x \ (x \ y))) to_power 1 by A5, BCIALG_2:2 .= (((x \ y) \ ((x \ y) \ x)),(x \ (x \ y))) to_power 1 by BCIALG_2:2 .= ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by BCIALG_2:2 ; hence x \ y = (x \ y) \ y by A4, A3; ::_thesis: verum end; hence for x, y being Element of X holds x \ y = (x \ y) \ y ; ::_thesis: verum end; assume for x, y being Element of X holds x \ y = (x \ y) \ y ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1 then X is BCK-positive-implicative BCK-algebra by BCIALG_3:28; hence X is BCK-algebra of 0 ,1, 0 ,1 by Th49; ::_thesis: verum end; theorem :: BCIALG_5:53 for n being Element of NAT for X being quasi-commutative BCK-algebra holds ( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) proof let n be Element of NAT ; ::_thesis: for X being quasi-commutative BCK-algebra holds ( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) let X be quasi-commutative BCK-algebra; ::_thesis: ( X is BCK-algebra of n,n + 1,n,n + 1 iff for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) thus ( X is BCK-algebra of n,n + 1,n,n + 1 implies for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) ::_thesis: ( ( for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ) implies X is BCK-algebra of n,n + 1,n,n + 1 ) proof assume A1: X is BCK-algebra of n,n + 1,n,n + 1 ; ::_thesis: for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) proof let x, y be Element of X; ::_thesis: (x,y) to_power (n + 1) = (x,y) to_power (n + 2) A2: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then A3: (((x,(x \ (x \ y))) to_power (n + 1)),((x \ y) \ x)) to_power (n + 1) = (((x,y) to_power (n + 1)),(0. X)) to_power (n + 1) by BCIALG_2:8 .= (x,y) to_power (n + 1) by BCIALG_2:5 ; A4: ((((x \ y),((x \ y) \ x)) to_power (n + 1)),(x \ (x \ y))) to_power (n + 1) = ((x \ y),(x \ (x \ y))) to_power (n + 1) by A2, BCIALG_2:5 .= ((x,(x \ (x \ y))) to_power (n + 1)) \ y by BCIALG_2:7 .= ((x,y) to_power (n + 1)) \ y by BCIALG_2:8 .= (x,y) to_power ((n + 1) + 1) by BCIALG_2:4 ; Polynom (n,(n + 1),x,(x \ y)) = Polynom (n,(n + 1),(x \ y),x) by A1, Def3; hence (x,y) to_power (n + 1) = (x,y) to_power (n + 2) by A3, A4; ::_thesis: verum end; hence for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ; ::_thesis: verum end; assume A5: for x, y being Element of X holds (x,y) to_power (n + 1) = (x,y) to_power (n + 2) ; ::_thesis: X is BCK-algebra of n,n + 1,n,n + 1 for x, y being Element of X holds Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x) proof let x, y be Element of X; ::_thesis: Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x) (x \ y) \ (x \ y) = 0. X by BCIALG_1:def_5; then (x \ (x \ y)) \ y = 0. X by BCIALG_1:7; then x \ (x \ y) <= y by BCIALG_1:def_11; then ((x \ (x \ y)),(x \ y)) to_power (n + 1) <= (y,(x \ y)) to_power (n + 1) by BCIALG_2:19; then (((x,(x \ y)) to_power 1),(x \ y)) to_power (n + 1) <= (y,(x \ y)) to_power (n + 1) by BCIALG_2:2; then A6: (x,(x \ y)) to_power (1 + (n + 1)) <= (y,(x \ y)) to_power (n + 1) by BCIALG_2:10; (y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5; then (y \ (y \ x)) \ x = 0. X by BCIALG_1:7; then y \ (y \ x) <= x by BCIALG_1:def_11; then ((y \ (y \ x)),(y \ x)) to_power (n + 1) <= (x,(y \ x)) to_power (n + 1) by BCIALG_2:19; then (((y,(y \ x)) to_power 1),(y \ x)) to_power (n + 1) <= (x,(y \ x)) to_power (n + 1) by BCIALG_2:2; then A7: (y,(y \ x)) to_power (1 + (n + 1)) <= (x,(y \ x)) to_power (n + 1) by BCIALG_2:10; (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (n + 2) by A5; then (((y,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) by A7, BCIALG_2:19; then A8: (((y,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) <= (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by BCIALG_2:11; (x,(x \ y)) to_power (n + 1) = (x,(x \ y)) to_power (n + 2) by A5; then (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((y,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) by A6, BCIALG_2:19; then (((x,(x \ y)) to_power (n + 1)),(y \ x)) to_power (n + 1) <= (((y,(y \ x)) to_power (n + 1)),(x \ y)) to_power (n + 1) by BCIALG_2:11; hence Polynom (n,(n + 1),x,y) = Polynom (n,(n + 1),y,x) by A8, Th2; ::_thesis: verum end; hence X is BCK-algebra of n,n + 1,n,n + 1 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:54 for X being BCI-algebra st X is BCI-algebra of 0 ,1, 0 , 0 holds X is BCI-commutative BCI-algebra proof let X be BCI-algebra; ::_thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 implies X is BCI-commutative BCI-algebra ) assume A1: X is BCI-algebra of 0 ,1, 0 , 0 ; ::_thesis: X is BCI-commutative BCI-algebra for x, y being Element of X st y \ x = 0. X holds y = x \ (x \ y) proof let x, y be Element of X; ::_thesis: ( y \ x = 0. X implies y = x \ (x \ y) ) Polynom (0,1,x,y) = Polynom (0,0,y,x) by A1, Def3; then ((x,(x \ y)) to_power 1) \ (y \ x) = (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:2; then (x \ (x \ y)) \ (y \ x) = (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:2; then A2: (x \ (x \ y)) \ (y \ x) = (y,(y \ x)) to_power 1 by BCIALG_2:1; assume y \ x = 0. X ; ::_thesis: y = x \ (x \ y) then (x \ (x \ y)) \ (0. X) = y \ (0. X) by A2, BCIALG_2:2; then y = (x \ (x \ y)) \ (0. X) by BCIALG_1:2; hence y = x \ (x \ y) by BCIALG_1:2; ::_thesis: verum end; then for x, y being Element of X st x \ y = 0. X holds x = y \ (y \ x) ; hence X is BCI-commutative BCI-algebra by BCIALG_3:def_4; ::_thesis: verum end; theorem :: BCIALG_5:55 for X being BCI-algebra for n, m being Element of NAT st X is BCI-algebra of n, 0 ,m,m holds X is BCI-commutative BCI-algebra proof let X be BCI-algebra; ::_thesis: for n, m being Element of NAT st X is BCI-algebra of n, 0 ,m,m holds X is BCI-commutative BCI-algebra let n, m be Element of NAT ; ::_thesis: ( X is BCI-algebra of n, 0 ,m,m implies X is BCI-commutative BCI-algebra ) A1: for x, y being Element of X st x \ y = 0. X holds (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1 proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1 ) defpred S1[ Element of NAT ] means ( \$1 <= m implies (y,(y \ x)) to_power (\$1 + 1) <= (y,(y \ x)) to_power 1 ); assume A2: x \ y = 0. X ; ::_thesis: (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1 now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_m_implies_(y,(y_\_x))_to_power_(k_+_1)_<=_(y,(y_\_x))_to_power_1_)_&_k_+_1_<=_m_holds_ (y,(y_\_x))_to_power_((k_+_1)_+_1)_<=_(y,(y_\_x))_to_power_1 ((0. X),(y \ x)) to_power 1 = (((0. X),y) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:18; then (0. X) \ (y \ x) = (((0. X),y) to_power 1) \ (((0. X),x) to_power 1) by BCIALG_2:2; then A3: (0. X) \ (y \ x) = ((0. X) \ y) \ (((0. X),x) to_power 1) by BCIALG_2:2; let k be Element of NAT ; ::_thesis: ( ( k <= m implies (y,(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power 1 ) & k + 1 <= m implies (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1 ) assume A4: ( k <= m implies (y,(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power 1 ) ; ::_thesis: ( k + 1 <= m implies (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1 ) (((0. X) \ y) \ ((0. X) \ x)) \ (x \ y) = 0. X by BCIALG_1:1; then ((0. X) \ y) \ ((0. X) \ x) = 0. X by A2, BCIALG_1:2; then (0. X) \ (y \ x) = 0. X by A3, BCIALG_2:2; then (y \ y) \ (y \ x) = 0. X by BCIALG_1:def_5; then (y \ (y \ x)) \ y = 0. X by BCIALG_1:7; then y \ (y \ x) <= y by BCIALG_1:def_11; then ((y \ (y \ x)),(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power (k + 1) by BCIALG_2:19; then (((y,(y \ x)) to_power 1),(y \ x)) to_power (k + 1) <= (y,(y \ x)) to_power (k + 1) by BCIALG_2:2; then A5: (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power (k + 1) by BCIALG_2:10; set m1 = k + 1; assume k + 1 <= m ; ::_thesis: (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1 hence (y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1 by A4, A5, Th1, NAT_1:13; ::_thesis: verum end; then A6: for k being Element of NAT st S1[k] holds S1[k + 1] ; ((y,(y \ x)) to_power (0 + 1)) \ ((y,(y \ x)) to_power 1) = 0. X by BCIALG_1:def_5; then A7: S1[ 0 ] by BCIALG_1:def_11; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A7, A6); hence (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1 ; ::_thesis: verum end; assume A8: X is BCI-algebra of n, 0 ,m,m ; ::_thesis: X is BCI-commutative BCI-algebra for x, y being Element of X st x \ y = 0. X holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) ) assume A9: x \ y = 0. X ; ::_thesis: x = y \ (y \ x) Polynom (n,0,x,y) = Polynom (m,m,y,x) by A8, Def3; then (x,(y \ x)) to_power 0 = (((y,(y \ x)) to_power (m + 1)),(0. X)) to_power m by A9, BCIALG_2:5; then (x,(y \ x)) to_power 0 = ((((y,(y \ x)) to_power (m + 1)),(0. X)) to_power m) \ (0. X) by BCIALG_1:2; then (x,(y \ x)) to_power 0 = (((y,(y \ x)) to_power (m + 1)),(0. X)) to_power (m + 1) by BCIALG_2:4; then (x,(y \ x)) to_power 0 = (y,(y \ x)) to_power (m + 1) by BCIALG_2:5; then x = (y,(y \ x)) to_power (m + 1) by BCIALG_2:1; then x <= (y,(y \ x)) to_power 1 by A1, A9; then A10: x <= y \ (y \ x) by BCIALG_2:2; (y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7; then (y \ (y \ x)) \ x = 0. X by BCIALG_1:def_5; then y \ (y \ x) <= x by BCIALG_1:def_11; hence x = y \ (y \ x) by A10, Th2; ::_thesis: verum end; hence X is BCI-commutative BCI-algebra by BCIALG_3:def_4; ::_thesis: verum end; theorem :: BCIALG_5:56 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st j = 0 & m > 0 holds X is BCK-algebra of 0 , 0 , 0 , 0 proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st j = 0 & m > 0 holds X is BCK-algebra of 0 , 0 , 0 , 0 let X be BCK-algebra of i,j,m,n; ::_thesis: ( j = 0 & m > 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 ) assume that A1: j = 0 and A2: m > 0 ; ::_thesis: X is BCK-algebra of 0 , 0 , 0 , 0 for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,n,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) = Polynom (0,n,y,x) A3: Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3; A4: i + 1 >= j + 1 by A1, XREAL_1:6; ( (x,(x \ y)) to_power (j + 1) = (x,(x \ y)) to_power (m + 1) & j + 1 < m + 1 ) by A1, A2, Th20, XREAL_1:6; then (x,(x \ y)) to_power (i + 1) = (x,(x \ y)) to_power (0 + 1) by A1, A4, Th6; hence Polynom (0,0,x,y) = Polynom (0,n,y,x) by A1, A3, Th20; ::_thesis: verum end; then reconsider X = X as BCK-algebra of 0 , 0 , 0 ,n by Def3; A5: for x, y being Element of X holds Polynom (0,0,x,y) <= Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,0,x,y) <= Polynom (0,0,y,x) Polynom (0,0,x,y) = Polynom (0,n,y,x) by Def3; hence Polynom (0,0,x,y) <= Polynom (0,0,y,x) by Th5; ::_thesis: verum end; for x, y being Element of X holds Polynom (0,0,y,x) = Polynom (0,0,x,y) proof let x, y be Element of X; ::_thesis: Polynom (0,0,y,x) = Polynom (0,0,x,y) Polynom (0,0,x,y) <= Polynom (0,0,y,x) by A5; then A6: (Polynom (0,0,x,y)) \ (Polynom (0,0,y,x)) = 0. X by BCIALG_1:def_11; Polynom (0,0,y,x) <= Polynom (0,0,x,y) by A5; then (Polynom (0,0,y,x)) \ (Polynom (0,0,x,y)) = 0. X by BCIALG_1:def_11; hence Polynom (0,0,y,x) = Polynom (0,0,x,y) by A6, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:57 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st m = 0 & j > 0 holds X is BCK-algebra of 0 ,1, 0 ,1 proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st m = 0 & j > 0 holds X is BCK-algebra of 0 ,1, 0 ,1 let X be BCK-algebra of i,j,m,n; ::_thesis: ( m = 0 & j > 0 implies X is BCK-algebra of 0 ,1, 0 ,1 ) reconsider X = X as BCK-algebra of i + 1,j,m,n + 1 by Th17; assume that A1: m = 0 and A2: j > 0 ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x) A3: (i + 1) + 1 > (m + 1) + 0 by A1, XREAL_1:8; A4: (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (m + 1) by Th20; A5: j + 1 > m + 1 by A1, A2, XREAL_1:6; ( n + 1 >= m + 1 & (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (j + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (m + 1) ) by A1, Th20, XREAL_1:6; then A6: (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (0 + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by A1, A5, Th6; ( Polynom ((i + 1),j,x,y) = Polynom (m,(n + 1),y,x) & (x,(x \ y)) to_power (j + 1) = (x,(x \ y)) to_power (m + 1) ) by Def3, Th20; then (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power j = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by A1, A5, A3, Th6; hence Polynom (0,1,x,y) = Polynom (0,1,y,x) by A1, A5, A6, A4, Th6, NAT_1:14; ::_thesis: verum end; hence X is BCK-algebra of 0 ,1, 0 ,1 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:58 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st n = 0 & i <> 0 holds X is BCK-algebra of 0 , 0 , 0 , 0 proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st n = 0 & i <> 0 holds X is BCK-algebra of 0 , 0 , 0 , 0 let X be BCK-algebra of i,j,m,n; ::_thesis: ( n = 0 & i <> 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 ) assume that A1: n = 0 and A2: i <> 0 ; ::_thesis: X is BCK-algebra of 0 , 0 , 0 , 0 for x, y being Element of X holds Polynom (0,j,x,y) = Polynom (0,0,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,j,x,y) = Polynom (0,0,y,x) A3: Polynom (i,j,x,y) = Polynom (m,n,y,x) by Def3; A4: m + 1 >= n + 1 by A1, XREAL_1:6; ( (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (i + 1) & n + 1 < i + 1 ) by A1, A2, Th19, XREAL_1:6; then (y,(y \ x)) to_power (m + 1) = (y,(y \ x)) to_power (0 + 1) by A1, A4, Th6; hence Polynom (0,j,x,y) = Polynom (0,0,y,x) by A1, A3, Th19; ::_thesis: verum end; then reconsider X = X as BCK-algebra of 0 ,j, 0 , 0 by Def3; A5: for x, y being Element of X holds Polynom (0,0,y,x) <= Polynom (0,0,x,y) proof let x, y be Element of X; ::_thesis: Polynom (0,0,y,x) <= Polynom (0,0,x,y) Polynom (0,j,x,y) = Polynom (0,0,y,x) by Def3; hence Polynom (0,0,y,x) <= Polynom (0,0,x,y) by Th5; ::_thesis: verum end; for x, y being Element of X holds Polynom (0,0,y,x) = Polynom (0,0,x,y) proof let x, y be Element of X; ::_thesis: Polynom (0,0,y,x) = Polynom (0,0,x,y) Polynom (0,0,x,y) <= Polynom (0,0,y,x) by A5; then A6: (Polynom (0,0,x,y)) \ (Polynom (0,0,y,x)) = 0. X by BCIALG_1:def_11; Polynom (0,0,y,x) <= Polynom (0,0,x,y) by A5; then (Polynom (0,0,y,x)) \ (Polynom (0,0,x,y)) = 0. X by BCIALG_1:def_11; hence Polynom (0,0,y,x) = Polynom (0,0,x,y) by A6, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; ::_thesis: verum end; theorem :: BCIALG_5:59 for i, j, m, n being Element of NAT for X being BCK-algebra of i,j,m,n st i = 0 & n <> 0 holds X is BCK-algebra of 0 ,1, 0 ,1 proof let i, j, m, n be Element of NAT ; ::_thesis: for X being BCK-algebra of i,j,m,n st i = 0 & n <> 0 holds X is BCK-algebra of 0 ,1, 0 ,1 let X be BCK-algebra of i,j,m,n; ::_thesis: ( i = 0 & n <> 0 implies X is BCK-algebra of 0 ,1, 0 ,1 ) reconsider X = X as BCK-algebra of i,j + 1,m + 1,n by Th18; assume that A1: i = 0 and A2: n <> 0 ; ::_thesis: X is BCK-algebra of 0 ,1, 0 ,1 for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (0,1,y,x) proof let x, y be Element of X; ::_thesis: Polynom (0,1,x,y) = Polynom (0,1,y,x) A3: (m + 1) + 1 > (i + 1) + 0 by A1, XREAL_1:8; A4: (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (i + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) by Th19; A5: n + 1 > i + 1 by A1, A2, XREAL_1:6; ( j + 1 >= i + 1 & (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (n + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (i + 1) ) by A1, Th19, XREAL_1:6; then A6: (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (0 + 1) = (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) by A1, A5, Th6; ( Polynom (i,(j + 1),x,y) = Polynom ((m + 1),n,y,x) & (y,(y \ x)) to_power (n + 1) = (y,(y \ x)) to_power (i + 1) ) by Def3, Th19; then (((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) = (((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power n by A1, A5, A3, Th6; hence Polynom (0,1,x,y) = Polynom (0,1,y,x) by A1, A5, A6, A4, Th6, NAT_1:14; ::_thesis: verum end; hence X is BCK-algebra of 0 ,1, 0 ,1 by Def3; ::_thesis: verum end;