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 * (h |^ (- j))) = 1_ G
per cases ( j >= 1 or j < 0 or j = 0 ) by Lm13;
suppose A2: j >= 1 ; :: thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
then j >= 1 + 0 ;
then A3: j - 1 >= 0 by XREAL_1:19;
then A4: |.(j - 1).| + 1 = (j - 1) + 1 by ABSVALUE:def 1
.= j ;
A5: |.j.| = j by A2, ABSVALUE:def 1;
A6: |.j.| = |.(- j).| by COMPLEX1:52;
thus (h |^ (j - 1)) * (h * (h |^ (- j))) = ((h |^ (j - 1)) * h) * (h |^ (- j)) by Def3
.= ((h |^ |.(j - 1).|) * h) * (h |^ (- j)) by A3, Def8
.= ((h |^ |.(j - 1).|) * h) * ((h |^ |.(- j).|) ") by A2, Th29
.= (h |^ (|.(j - 1).| + 1)) * ((h |^ |.(- j).|) ") by Lm6
.= 1_ G by A4, A5, A6, Def5 ; :: thesis: verum
end;
suppose A7: j < 0 ; :: thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
A8: 1 - j = - (j - 1) ;
thus (h |^ (j - 1)) * (h * (h |^ (- j))) = ((h |^ |.(j - 1).|) ") * (h * (h |^ (- j))) by A7, Def8
.= ((h |^ |.(j - 1).|) ") * (h * (h |^ |.(- j).|)) by A7, Def8
.= ((h |^ |.(j - 1).|) ") * (h |^ (1 + |.(- j).|)) by Lm6
.= ((h |^ |.(j - 1).|) ") * (h |^ (1 + (- j))) by A7, ABSVALUE:def 1
.= ((h |^ |.(j - 1).|) ") * (h |^ |.(j - 1).|) by A7, A8, ABSVALUE:def 1
.= 1_ G by Def5 ; :: thesis: verum
end;
suppose A9: j = 0 ; :: thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
hence (h |^ (j - 1)) * (h * (h |^ (- j))) = (h ") * (h * (h |^ (- j))) by Th31
.= ((h ") * h) * (h |^ (- j)) by Def3
.= (1_ G) * (h |^ (- j)) by Def5
.= h |^ 0 by A9, Def4
.= 1_ G by Def7 ;
:: thesis: verum
end;
end;
end;
(h |^ (j - 1)) * (h |^ (1 - j)) = (h |^ (j - 1)) * (h |^ (- (j - 1)))
.= (h |^ (j - 1)) * ((h |^ (j - 1)) ") by Lm12
.= 1_ G by Def5 ;
then h * (h |^ (- j)) = h |^ (1 - j) by A1, Th6;
then (h |^ (1 - j)) " = ((h |^ (- j)) ") * (h ") by Th16
.= (h |^ (- (- j))) * (h ") by Lm12
.= (h |^ j) * (h |^ (- 1)) by Th31 ;
then (h |^ j) * (h |^ (- 1)) = h |^ (- (1 - j)) by Lm12;
hence h |^ (j - 1) = (h |^ j) * (h |^ (- 1)) ; :: thesis: verum