let X be BCI-algebra; for m, n being Nat st X is BCI-algebra of n, 0 ,m,m holds
X is BCI-commutative BCI-algebra
let m, n be Nat; ( 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;
( x \ y = 0. X implies (y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1 )
defpred S1[
Nat]
means ( $1
<= m implies (
y,
(y \ x))
to_power ($1 + 1) <= (
y,
(y \ x))
to_power 1 );
assume A2:
x \ y = 0. X
;
(y,(y \ x)) to_power (m + 1) <= (y,(y \ x)) to_power 1
now for k being 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
Nat;
( ( 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 )
;
( 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
;
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
;
(y,(y \ x)) to_power ((k + 1) + 1) <= (y,(y \ x)) to_power 1hence
(
y,
(y \ x))
to_power ((k + 1) + 1) <= (
y,
(y \ x))
to_power 1
by A4, A5, Th1, NAT_1:13;
verum end;
then A6:
for
k being
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
Nat holds
S1[
m]
from NAT_1:sch 2(A7, A6);
hence
(
y,
(y \ x))
to_power (m + 1) <= (
y,
(y \ x))
to_power 1
;
verum
end;
assume A8:
X is BCI-algebra of n, 0 ,m,m
; 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;
( x \ y = 0. X implies x = y \ (y \ x) )
assume A9:
x \ y = 0. X
;
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
;
hence
x = y \ (y \ x)
by A10, Th2;
verum
end;
hence
X is BCI-commutative BCI-algebra
by BCIALG_3:def 4; verum