let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)
let a be Element of AtomSet X; :: thesis: for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)
let i, j be Integer; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
per cases
( i > 0 or i = 0 or i < 0 )
;
suppose E1:
i < 0
;
:: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)then E2:
- i > 0
by XREAL_1:60;
reconsider m =
- i as
Element of
NAT by E1, INT_1:16;
per cases
( j >= 0 or j < 0 )
;
suppose E3:
j >= 0
;
:: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)set n =
- (i - j);
reconsider n =
- (i - j),
j =
j as
Element of
NAT by E1, E3, INT_1:16;
reconsider b =
a ` as
Element of
AtomSet X by BCIALG_1:34;
E9:
a |^ (i - j) =
(BCI-power X) . (a ` ),
(abs (i - j))
by Def2, E1
.=
(a ` ) |^ n
by E1, ABSVALUE:def 1
.=
b |^ (j + m)
.=
((a ` ) |^ m) \ (((a ` ) |^ j) ` )
by Th14
;
E11:
a |^ i =
(BCI-power X) . (a ` ),
(abs i)
by Def2, E1
.=
(a ` ) |^ m
by E1, ABSVALUE:def 1
;
((a ` ) |^ j) ` =
(b ` ) |^ j
by Th17
.=
a |^ j
by BCIALG_1:29
;
hence
(a |^ i) \ (a |^ j) = a |^ (i - j)
by E9, E11;
:: thesis: verum end; suppose E13:
j < 0
;
:: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)then E15:
- j > 0
by XREAL_1:60;
reconsider n =
- j as
Element of
NAT by E13, INT_1:16;
reconsider b =
a ` as
Element of
AtomSet X by BCIALG_1:34;
E17:
a |^ i =
(BCI-power X) . (a ` ),
(abs i)
by Def2, E1
.=
(a ` ) |^ m
by E1, ABSVALUE:def 1
;
a |^ j =
(BCI-power X) . (a ` ),
(abs j)
by Def2, E13
.=
(a ` ) |^ n
by E13, ABSVALUE:def 1
;
then E19:
(a |^ i) \ (a |^ j) = b |^ (m - n)
by Lm20, E15, E2, E17;
end; end;