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 )
assume A1:
X is BCI-algebra of n, 0 ,m,m
; :: thesis: X is BCI-commutative BCI-algebra
C1:
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 )
assume B1:
x \ y = 0. X
;
:: thesis: 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 );
then A1:
S1[
0 ]
;
A2:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
now 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 A3:
(
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 )set m1 =
k + 1;
assume A4:
k + 1
<= m
;
:: thesis: 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 B2:
((0. X) \ y) \ ((0. X) \ x) = 0. X
by B1, BCIALG_1:2;
(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
(0. X) \ (y \ x) = ((0. X) \ y) \ ((0. X),x to_power 1)
by BCIALG_2:2;
then
(0. X) \ (y \ x) = 0. X
by B2, 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
y,
(y \ x) to_power ((k + 1) + 1) <= y,
(y \ x) to_power (k + 1)
by BCIALG_2:10;
hence
y,
(y \ x) to_power ((k + 1) + 1) <= y,
(y \ x) to_power 1
by A4, Th01, A3, NAT_1:13;
:: thesis: verum end;
hence
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
;
:: thesis: verum
end;
for
m being
Element of
NAT holds
S1[
m]
from NAT_1:sch 1(A1, A2);
hence
y,
(y \ x) to_power (m + 1) <= y,
(y \ x) to_power 1
;
:: thesis: verum
end;
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)
proof
let x,
y be
Element of
X;
:: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume D1:
x \ y = 0. X
;
:: thesis: x = y \ (y \ x)
Polynom n,
0 ,
x,
y = Polynom m,
m,
y,
x
by A1, Def2;
then
x,
(y \ x) to_power 0 = (y,(y \ x) to_power (m + 1)),
(0. X) to_power m
by D1, 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 C1, D1;
then D2:
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 D2, Th02;
:: thesis: verum
end;
hence
X is BCI-commutative BCI-algebra
by BCIALG_3:def 4; :: thesis: verum