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 B1:
X is p-Semisimple BCI-algebra
; :: thesis: X is BCI-algebra of n + j,n,m,(m + j) + 1
B2:
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
A1a:
Polynom 0 ,
0 ,
x,
y =
x \ (x \ y)
by Th1
.=
y
by B1, BCIALG_1:def 26
;
defpred S1[
Element of
NAT ]
means ( $1
<= n implies
Polynom $1,$1,
x,
y = y );
A1:
S1[
0 ]
by A1a;
A2:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
now 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;
assume A4:
k + 1
<= n
;
:: thesis: Polynom (k + 1),(k + 1),x,y = y Polynom (k + 1),
(k + 1),
x,
y =
(Polynom k,(k + 1),x,y) \ (x \ y)
by Th1b
.=
((Polynom k,k,x,y) \ (y \ x)) \ (x \ y)
by Th1c
;
then
Polynom (k + 1),
(k + 1),
x,
y = x \ (x \ y)
by B1, A3, A4, BCIALG_1:def 26, NAT_1:13;
hence
Polynom (k + 1),
(k + 1),
x,
y = y
by B1, BCIALG_1:def 26;
:: thesis: verum end;
hence
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
;
:: thesis: verum
end;
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A1, A2);
hence
Polynom n,
n,
x,
y = y
;
:: thesis: verum
end;
B3:
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
A1a:
Polynom 0 ,1,
x,
y =
(Polynom 0 ,0 ,x,y) \ (y \ x)
by Th1c
.=
(x \ (x \ y)) \ (y \ x)
by Th1
.=
y \ (y \ x)
by B1, BCIALG_1:def 26
.=
x
by B1, BCIALG_1:def 26
;
defpred S1[
Element of
NAT ]
means ( $1
<= m implies
Polynom $1,
($1 + 1),
x,
y = x );
A1:
S1[
0 ]
by A1a;
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 Polynom k,(k + 1),x,y = x ) & k + 1 <= m implies Polynom (k + 1),((k + 1) + 1),x,y = x )assume A3:
(
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;
assume A4:
k + 1
<= m
;
:: thesis: Polynom (k + 1),((k + 1) + 1),x,y = x Polynom (k + 1),
((k + 1) + 1),
x,
y =
(Polynom k,((k + 1) + 1),x,y) \ (x \ y)
by Th1b
.=
((Polynom k,(k + 1),x,y) \ (y \ x)) \ (x \ y)
by Th1c
;
then Polynom (k + 1),
((k + 1) + 1),
x,
y =
(x \ (x \ y)) \ (y \ x)
by A3, A4, BCIALG_1:7, NAT_1:13
.=
y \ (y \ x)
by B1, BCIALG_1:def 26
;
hence
Polynom (k + 1),
((k + 1) + 1),
x,
y = x
by B1, BCIALG_1:def 26;
:: 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
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
A1a:
Polynom (n + 0 ),
n,
x,
y =
y
by B2
.=
Polynom m,
((m + 0 ) + 1),
y,
x
by B3
;
defpred S1[
Element of
NAT ]
means ( $1
<= j implies
Polynom (n + $1),
n,
x,
y = Polynom m,
((m + $1) + 1),
y,
x );
A1:
S1[
0 ]
by A1a;
A2:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
now 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 A3:
(
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,xthen Polynom (n + (k + 1)),
n,
x,
y =
(Polynom m,((m + k) + 1),y,x) \ (x \ y)
by A3, Th1b, NAT_1:13
.=
Polynom m,
(((m + k) + 1) + 1),
y,
x
by Th1c
;
hence
Polynom (n + (k + 1)),
n,
x,
y = Polynom m,
((m + (k + 1)) + 1),
y,
x
;
:: thesis: verum end;
hence
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
;
:: thesis: verum
end;
for
j being
Element of
NAT holds
S1[
j]
from NAT_1:sch 1(A1, A2);
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 Def2; :: thesis: verum