let X be BCI-algebra; :: thesis:
let x, y be Element of X; :: thesis:
let a, b be Element of AtomSet X; :: thesis:
assume that
A1: a \ b is finite-period and
A2: x is finite-period and
A3: y is finite-period and
A4: a is finite-period and
A5: b is finite-period and
A6: x in BranchV a and
A7: y in BranchV b ; :: thesis:
ord y divides (ord x) lcm (ord y) by NAT_D:def 4;
then consider yx being Nat such that
A8: (ord x) lcm (ord y) = (ord y) * yx by NAT_D:def 3;
reconsider na = ord a as Element of NAT ;
reconsider xly = (ord x) lcm (ord y) as Element of NAT ;
ord x divides (ord x) lcm (ord y) by NAT_D:def 4;
then consider xy being Nat such that
A9: (ord x) lcm (ord y) = (ord x) * xy by NAT_D:def 3;
(a \ b) |^ xly = (a |^ ((ord x) * xy)) \ (b |^ ((ord y) * yx)) by A9, A8, Th15
.= ((a |^ (ord x)) |^ xy) \ (b |^ ((ord y) * yx)) by Th23
.= ((a |^ (ord x)) |^ xy) \ ((b |^ (ord y)) |^ yx) by Th23
.= ((a |^ na) |^ xy) \ ((b |^ (ord y)) |^ yx) by A2, A4, A6, Th28
.= ((0. X) |^ xy) \ ((b |^ (ord y)) |^ yx) by A4, Th26
.= ((0. X) |^ xy) \ ((b |^ (ord b)) |^ yx) by A3, A5, A7, Th28
.= ((0. X) |^ xy) \ ((0. X) |^ yx) by A5, Th26
.= ((0. X) |^ yx) ` by Th7
.= (0. X) ` by Th7
.= 0. X by BCIALG_1:def 5 ;
then ((a \ b) |^ xly) ` = 0. X by BCIALG_1:def 5;
then 0. X <= (a \ b) |^ xly ;
then (a \ b) |^ xly in BCK-part X ;
hence ord (a \ b) divides (ord x) lcm (ord y) by A1, Th29; :: thesis: