let j be Integer; :: thesis: for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
let G be Group; :: thesis: for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
let h be Element of G; :: thesis: h |^ (j + 1) = (h |^ j) * (h |^ 1)
A1: now :: thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
per cases ( j >= 0 or j < - 1 or j = - 1 ) by Lm15;
suppose A2: j >= 0 ; :: thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
then reconsider n = j as Element of NAT by INT_1:3;
A3: n + 1 = |.(j + 1).| by ABSVALUE:def 1;
n + 1 >= 0 ;
hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = (h |^ |.(j + 1).|) * ((h |^ (- 1)) * (h |^ (- j))) by Def8
.= (h |^ |.(j + 1).|) * ((h ") * (h |^ (- j))) by Th31
.= (h |^ |.(j + 1).|) * ((h ") * ((h |^ j) ")) by Lm12
.= (h |^ |.(j + 1).|) * ((h ") * ((h |^ |.j.|) ")) by A2, Def8
.= (h |^ |.(j + 1).|) * (((h |^ |.j.|) * h) ") by Th16
.= (h |^ |.(j + 1).|) * ((h |^ (|.j.| + 1)) ") by Lm6
.= (h |^ |.(j + 1).|) * ((h |^ |.(j + 1).|) ") by A3, ABSVALUE:def 1
.= 1_ G by Def5 ;
:: thesis: verum
end;
suppose j < - 1 ; :: thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
then A4: j + 1 < (- 1) + 1 by XREAL_1:6;
hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = ((h |^ |.(j + 1).|) ") * ((h |^ (- 1)) * (h |^ (- j))) by Def8
.= ((h |^ |.(j + 1).|) ") * ((h ") * (h |^ (- j))) by Th31
.= (((h |^ |.(j + 1).|) ") * (h ")) * (h |^ (- j)) by Def3
.= ((h * (h |^ |.(j + 1).|)) ") * (h |^ (- j)) by Th16
.= ((h |^ (|.(j + 1).| + 1)) ") * (h |^ (- j)) by Lm6
.= ((h |^ ((- (j + 1)) + 1)) ") * (h |^ (- j)) by A4, ABSVALUE:def 1
.= 1_ G by Def5 ;
:: thesis: verum
end;
suppose A5: j = - 1 ; :: thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = (1_ G) * ((h |^ (- 1)) * (h |^ (- j))) by Lm3
.= (h |^ (- 1)) * (h |^ (- j)) by Def4
.= (h ") * (h |^ (- j)) by Th31
.= (h ") * ((h |^ j) ") by Lm12
.= (h ") * ((h ") ") by A5, Th31
.= 1_ G by Def5 ;
:: thesis: verum
end;
end;
end;
(h |^ (j + 1)) * (h |^ (- (j + 1))) = (h |^ (j + 1)) * ((h |^ (j + 1)) ") by Lm12
.= 1_ G by Def5 ;
then A6: h |^ (- (j + 1)) = (h |^ (- 1)) * (h |^ (- j)) by A1, Th6;
thus h |^ (j + 1) = h |^ (- (- (j + 1)))
.= ((h |^ (- 1)) * (h |^ (- j))) " by A6, Lm12
.= ((h |^ (- j)) ") * ((h |^ (- 1)) ") by Th16
.= (h |^ (- (- j))) * ((h |^ (- 1)) ") by Lm12
.= (h |^ j) * (h |^ (- (- 1))) by Lm12
.= (h |^ j) * (h |^ 1) ; :: thesis: verum